|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object fmrisc.Proving.ProofState
public final class ProofState
The state of a proof. A proof state E(AX): A1,...,An |- B1,...Bm consists of - an environment E of function/predicate cohnstant definitions - a sequence of axioms assumed true in that state - a sequence of formulas ("assumptions") A1,...,An - a sequence of formulas (potential "goals") B1,...,Bm. - potentially, a sequence of formulas (the counterexample) C1,...,Co. The state logically represents the formula AX => (~A1 \/ ... \/ ~An) \/ (B1 \/ ... \/ Bm) i.e. AX => (A1 /\ ... /\ An) => (B1 \/ ... \/ Bm). If given, the counterexample represents a formula C1 /\ ... /\ Co which implies AX /\ (A1 /\ ... /\ An) /\ (~B1 /\ ... /\ ... /\ ~Bn).
Constructor Summary | |
---|---|
ProofState(Proof proof)
Construct a skeleton proof state (all fields but the proof remain uninitialized). |
|
ProofState(Proof proof,
Environment env,
Expression goal,
boolean autoSimplify)
construct a root state from a single goal and without assumptions |
|
ProofState(ProofState parent,
Environment env)
construct a proof state without path and formulas yet |
Method Summary | |
---|---|
Formula[] |
add(Formula[] formulas,
Formula formula)
Adds a formula to a sequence of formulas in this state. |
Formula[] |
add(Formula[] formulas,
Formula[] formulas0)
Adds a sequence of formulas to a sequence of formulas in this state. |
void |
addOpen(java.util.Vector vector)
Add open state and all open children recursively to vector. |
void |
close(java.lang.String reason)
close the state. |
Formula[] |
copy(Formula[] formulas)
Copy a sequence of formulas in this state. |
void |
extend(Command command,
ProofState[] children)
command extends current state by adding and labeling children |
Formula |
getAssumption(java.lang.String label)
returns assumption with denoted label |
Formula[] |
getAssumptions()
get assumptions of proof state |
Formula[] |
getAxioms()
get axioms of proof state |
ProofState[] |
getChildren()
get children of proof state |
Command |
getCommand()
get command of proof state |
Expression[] |
getCounterExample()
Get counterexample for state. |
Environment |
getEnvironment()
get environment of proof state |
Formula |
getFormula(java.lang.String label)
returns formula (assumption or goal) with denoted label |
Formula |
getGoal(java.lang.String label)
returns goal with denoted label |
Formula[] |
getGoals()
get goals of proof state |
java.lang.String |
getLabel()
return label of proof state |
ProofStateListener |
getListener()
Get listener that is notified when proof state has changed. |
ProofState |
getParent()
get parent of proof state |
java.lang.String |
getPath()
get path of proof state |
Proof |
getProof()
get proof to which proof state belong |
UniqueNameTable |
getSkolemTable()
Get unique name table to be used for creating skolemization constants. |
void |
hasChanged(boolean file)
Signal that state has changed updating presentation of this state. |
boolean |
isClosed()
check whether proof state is closed |
void |
labelChildren()
Label the children of the current state. |
void |
open()
open the state. |
void |
print(java.io.PrintWriter out)
print proof state on output stream |
void |
print(java.io.PrintWriter out,
int level)
Print proof state including children. |
void |
redo()
Redo the proof at the denoted state (if possible) |
Formula[] |
remove(Formula[] formulas,
Formula formula)
Remove a formula from a sequence of formulas in this state. |
Formula[] |
replace(Formula[] formulas,
Formula formula,
Formula rformula)
Replace a formula in a sequence of formulas in this state. |
void |
setAssumptions(Formula[] formulas)
set assumptions of proof state |
void |
setAutoSimplify(boolean on)
Set automatic simplification status of proof state |
void |
setAxioms(Formula[] formulas)
Set axioms of proof state. |
void |
setChildren(Command command,
ProofState[] children)
set children of proof state |
void |
setCommand(Command command)
set command of proof state |
void |
setCounterExample(Expression[] formulas)
Set counterexample for state. |
void |
setEnvironment(Environment env)
set environment of proof state |
void |
setGoals(Formula[] formulas)
set goals of proof state |
void |
setListener(ProofStateListener listener)
Set listener that is notified when proof state has changed. |
void |
setParent(ProofState parent)
set parent of proof state |
void |
setPath(java.lang.String path)
set path of proof state |
boolean |
simplify(boolean hard)
simplify the current proof state and potentially close it. |
boolean |
useAutoSimplify()
get automatic simplification status of proof state |
Methods inherited from class java.lang.Object |
---|
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Constructor Detail |
---|
public ProofState(Proof proof, Environment env, Expression goal, boolean autoSimplify)
proof
- the proof to which the state belongsenv
- the environment in which all constants are declaredgoal
- the goal formulaautoSimplify
- true iff automatic simplification is on in statepublic ProofState(ProofState parent, Environment env)
parent
- the parent stateenv
- the environment in which all constants are declaredpublic ProofState(Proof proof)
proof
- the proof to which the state shall belong.Method Detail |
---|
public java.lang.String getLabel()
public Proof getProof()
public java.lang.String getPath()
public void setPath(java.lang.String path)
path
- the path of the state (must be unique in the current proof)public ProofState getParent()
public void setParent(ProofState parent)
parent
- the parent of the statepublic Environment getEnvironment()
public void setEnvironment(Environment env)
env
- the environment.public Formula[] getAxioms()
public void setAxioms(Formula[] formulas)
formulas
- the axioms of the statepublic Formula[] getAssumptions()
public void setAssumptions(Formula[] formulas)
formulas
- the assumptions of the statepublic Formula[] getGoals()
public void setGoals(Formula[] formulas)
formulas
- the goals of the statepublic Expression[] getCounterExample()
public void setCounterExample(Expression[] formulas)
formulas
- sequence of formulas interpreted as a conjunction.public Command getCommand()
public void setCommand(Command command)
command
- the command applied to the proof statepublic boolean useAutoSimplify()
public void setAutoSimplify(boolean on)
on
- true iff automatic simplification is to be switched onpublic ProofState[] getChildren()
public void setChildren(Command command, ProofState[] children)
command
- the command that generated the childrenchildren
- the new children of the statepublic Formula getAssumption(java.lang.String label)
public Formula getGoal(java.lang.String label)
public Formula getFormula(java.lang.String label)
public UniqueNameTable getSkolemTable()
public void setListener(ProofStateListener listener)
listener
- the listener that is notified.public ProofStateListener getListener()
public void hasChanged(boolean file)
file
- true iff also presentation on file is to bechanged.public void print(java.io.PrintWriter out)
out
- the stream on which to print the formulapublic void close(java.lang.String reason)
reason
- explanation why state is closed.public void open()
public void redo()
public void labelChildren()
public void extend(Command command, ProofState[] children)
command
- the command extending the statechildren
- the children of the proof statepublic boolean isClosed()
public boolean simplify(boolean hard)
hard
- true iff hard (and time-consuming) simplification is tried.
public Formula[] copy(Formula[] formulas)
formulas
- a sequence of formulas
public Formula[] add(Formula[] formulas, Formula formula)
formulas
- a sequence of formulasformula
- a formula belonging to this state
public Formula[] add(Formula[] formulas, Formula[] formulas0)
formulas
- a sequence of formulasformulas0
- a sequence of formulas belonging to this state
public Formula[] remove(Formula[] formulas, Formula formula)
formulas
- a sequence of formulasformula
- a formula occuring in that sequence once
public Formula[] replace(Formula[] formulas, Formula formula, Formula rformula)
formulas
- a sequence of formulasformula
- a formula occuring in that sequence oncerformula
- a formula belonging to this state
public void print(java.io.PrintWriter out, int level)
out
- the stream to print the state to.level
- the level of the proof state (0 = root).public void addOpen(java.util.Vector vector)
vector
- vector receiving all open proof states.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |