|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object fmrisc.Proving.Instantiating
public final class Instantiating
Extending a proof state by instantiating quantified formulas.
Constructor Summary | |
---|---|
Instantiating()
|
Method Summary | |
---|---|
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 |
---|
public Instantiating()
Method Detail |
---|
public static ProofState instantiate(ProofState state)
state
- an open proof state.
public static ProofState instantiate(Formula formula)
formula
- a formula
public static ProofState instantiate(Formula[] formulas)
formulas
- a sequence of formulas in the same state
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |