|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object fmrisc.Proving.Proof
public final class Proof
Method Summary | |
---|---|
void |
close(ProofState state)
Inform proof that state was closed. |
void |
computeAbsolute()
The status of this proof or of the proof of a formula on which this proof depends may has changed. |
void |
cut(ProofState state)
Cut proof at denoted state. |
void |
extend(ProofState state,
ProofState[] children)
Inform proof that state was extended by children. |
ProofState |
getCurrent()
get current open proof state |
ProofState |
getOpenGoal()
get open leaf goal |
ProofState[] |
getOpenGoals()
get open leaf goals |
java.util.Collection |
getReferenced()
Get collection of symbols of those entities referenced in the last call of toNode(). |
ProofState |
getRoot()
get root of proof |
ProofState |
getState(java.lang.String tag)
Get proof state with denoted tag. |
java.lang.String |
getStatus()
Get status of proof. |
FormulaSymbol |
getSymbol()
get symbol of formula proved |
boolean |
isAbsolute()
Is proof absolute? |
boolean |
isClosed()
Is proof closed? |
boolean |
isSkeleton()
Is proof skeleton? |
boolean |
isTrusted()
Is proof trusted? |
static Proof |
newProof(FormulaSymbol symbol,
boolean autoSimplify)
Construct new proof for formula denoted by symbol. |
void |
nextOpenState()
switch current state to next open state in sequence. |
void |
prevOpenState()
switch current state to previous open state in sequence. |
void |
print()
Print proof. |
void |
printStatus(java.io.PrintWriter out)
Print status of proof to out |
boolean |
redo(ProofState state)
Redo proof at denoted state. |
void |
referenced(Identifier ident)
Mark identifier as referenced in current proof. |
boolean |
replay()
Replay skeleton proof. |
boolean |
replay(ProofState state)
Replay skeleton proof on proof state and its children. |
void |
setAbsolute(boolean absolute)
Signal whether proof is closed. |
void |
setClosed(boolean closed)
Signal whether proof is closed. |
void |
setCurrent(ProofState state)
set current open proof state |
void |
setSkeleton(boolean skeleton)
Signal whether proof is skeleton. |
void |
setTrusted(boolean trusted)
Signal whether proof is trusted. |
org.w3c.dom.Node |
toNode(org.w3c.dom.Document document)
Convert proof to DOM node in denoted document. |
static Proof |
toProof(FormulaSymbol symbol,
org.w3c.dom.Node node)
Construct skeleton proof from DOM representation. |
Methods inherited from class java.lang.Object |
---|
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Method Detail |
---|
public static Proof newProof(FormulaSymbol symbol, boolean autoSimplify)
symbol
- a formula symbolautoSimplify
- true iff automatic simplification is switched on
public boolean isSkeleton()
public void setSkeleton(boolean skeleton)
skeleton
- true iff proof is skeleton.public boolean isTrusted()
public void setTrusted(boolean trusted)
trusted
- true iff proof is trusted.public boolean isClosed()
public void setClosed(boolean closed)
closed
- true iff proof is closed.public boolean isAbsolute()
public void setAbsolute(boolean absolute)
absolute
- true iff proof is closed.public FormulaSymbol getSymbol()
public ProofState getRoot()
public ProofState getCurrent()
public void setCurrent(ProofState state)
state
- an open proof statepublic ProofState getOpenGoal()
public ProofState[] getOpenGoals()
public ProofState getState(java.lang.String tag)
tag
- the tag of the state
public void computeAbsolute()
public void cut(ProofState state)
state
- state at which the proof is cutpublic void close(ProofState state)
state
- a proof state that was closedpublic boolean redo(ProofState state)
state
- state at which the proof is redone.
public void extend(ProofState state, ProofState[] children)
state
- a proof state that was extended by childrenchildren
- open children states of statepublic void nextOpenState()
public void prevOpenState()
public void printStatus(java.io.PrintWriter out)
out
- output stream.public java.lang.String getStatus()
public void print()
public java.util.Collection getReferenced()
public void referenced(Identifier ident)
ident
- the identifier that is marked as referenced.public org.w3c.dom.Node toNode(org.w3c.dom.Document document)
document
- the document to which the proof belongs.
public static Proof toProof(FormulaSymbol symbol, org.w3c.dom.Node node)
symbol
- the symbol of the formula which is proved.node
- a DOM node representing the proof.
public boolean replay()
public boolean replay(ProofState state)
state
- the state on which the proof is to be replayed.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |