fmrisc.ProofNavigator.Proving

Class Instantiating

java.lang.Object

fmrisc.ProofNavigator.Proving.Instantiating

public final class Instantiating
extends java.lang.Object

Extending a proof state by instantiating quantified formulas.

Constructor Summary

Constructors

Constructor and Description
Instantiating()

Method Summary

Modifier and Type	Method and Description
static ProofState	instantiate(Formula formula) Extend proof state by instantiations of given formula
static ProofState	instantiate(Formula[] formulas) Extend proof state by instantiations of given formulas
static ProofState	instantiate(ProofState state) Extend given proof state by instantiations of quantified formulas.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Instantiating

public Instantiating()

Method Detail

instantiate

public static ProofState instantiate(ProofState state)

Extend given proof state by instantiations of quantified formulas.

Parameters:

state - an open proof state.

Returns:

null or a proof state whose parent is the given state and that is equivalent to the given state but with instantiated versions of quantified formulas added such that it is more likely that the state can be closed by a validity checker.

instantiate

public static ProofState instantiate(Formula formula)

Extend proof state by instantiations of given formula

Parameters:

formula - a formula

Returns:

null or a proof state whose parent is the state of the formula and that is equivalent to the given state but with instantiated versions of the given formula added such that it is more likely that the state can be closed by a validity checker.

instantiate

public static ProofState instantiate(Formula[] formulas)

Extend proof state by instantiations of given formulas

Parameters:

formulas - a sequence of formulas in the same state

Returns:

null or a proof state whose parent is the state of the formulas and that is equivalent to the given state but with instantiated versions of the given formulas added such that it is more likely that the state can be closed by a validity checker.