fmrisc.ProofNavigator.Proving

Class ProofState

java.lang.Object

fmrisc.ProofNavigator.Proving.ProofState

public final class ProofState
extends java.lang.Object

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 implies (~A1 \/ ... \/ ~An) \/ (B1 \/ ... \/ Bm) i.e. AX implies (A1 /\ ... /\ An) implies (B1 \/ ... \/ Bm). If given, the counterexample represents a formula C1 /\ ... /\ Co which implies AX /\ (A1 /\ ... /\ An) /\ (~B1 /\ ... /\ ... /\ ~Bn).

Constructor Summary

Constructors

Constructor and Description
ProofState(Proof proof) Construct a skeleton proof state (all fields but the proof remain uninitialized).
ProofState(Proof proof, Environment env, Expression goal, boolean autoSimplify, State.ProverVersion proverVersion, boolean firstOrder, boolean toLogical) 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

Modifier and Type	Method and Description
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<ProofState> 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
boolean	firstOrder() is prover first order?
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.
State.ProverVersion	proverVersion() get prover version of proof state
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	toLogical() is conversion BOOLEAN to LOGICAL to be applied?
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

ProofState

public ProofState(Proof proof,
                  Environment env,
                  Expression goal,
                  boolean autoSimplify,
                  State.ProverVersion proverVersion,
                  boolean firstOrder,
                  boolean toLogical)

construct a root state from a single goal and without assumptions

Parameters:

proof - the proof to which the state belongs

env - the environment in which all constants are declared

goal - the goal formula

autoSimplify - true iff automatic simplification is on in state

proverVersion - the version of the prover used in simplification

firstOrder - is prover first order?

toLogical - is conversion boolean to logical to be applied?

ProofState

public ProofState(ProofState parent,
                  Environment env)

construct a proof state without path and formulas yet

Parameters:

parent - the parent state

env - the environment in which all constants are declared

ProofState

public ProofState(Proof proof)

Construct a skeleton proof state (all fields but the proof remain uninitialized).

Parameters:

proof - the proof to which the state shall belong.

Method Detail

getLabel

public java.lang.String getLabel()

return label of proof state

Returns:

the proof state label

getProof

public Proof getProof()

get proof to which proof state belong

Returns:

the proof

getPath

public java.lang.String getPath()

get path of proof state

Returns:

the path of the state

setPath

public void setPath(java.lang.String path)

set path of proof state

Parameters:

path - the path of the state (must be unique in the current proof)

getParent

public ProofState getParent()

get parent of proof state

Returns:

the parent of the state

setParent

public void setParent(ProofState parent)

set parent of proof state

Parameters:

parent - the parent of the state

getEnvironment

public Environment getEnvironment()

get environment of proof state

Returns:

the environment

setEnvironment

public void setEnvironment(Environment env)

set environment of proof state

Parameters:

env - the environment.

getAxioms

public Formula[] getAxioms()

get axioms of proof state

Returns:

the axioms of the proof state

setAxioms

public void setAxioms(Formula[] formulas)

Set axioms of proof state.

Parameters:

formulas - the axioms of the state

getAssumptions

public Formula[] getAssumptions()

get assumptions of proof state

Returns:

the assumptions of the proof state

setAssumptions

public void setAssumptions(Formula[] formulas)

set assumptions of proof state

Parameters:

formulas - the assumptions of the state

getGoals

public Formula[] getGoals()

get goals of proof state

Returns:

the goals of the proof state

setGoals

public void setGoals(Formula[] formulas)

set goals of proof state

Parameters:

formulas - the goals of the state

getCounterExample

public Expression[] getCounterExample()

Get counterexample for state.

Returns:

the counterexample of the state (possibly null).

setCounterExample

public void setCounterExample(Expression[] formulas)

Set counterexample for state.

Parameters:

formulas - sequence of formulas interpreted as a conjunction.

getCommand

public Command getCommand()

get command of proof state

Returns:

command that generated the children states (null, if no children)

setCommand

public void setCommand(Command command)

set command of proof state

Parameters:

command - the command applied to the proof state

useAutoSimplify

public boolean useAutoSimplify()

get automatic simplification status of proof state

Returns:

true iff automatic simplification is switched on

proverVersion

public State.ProverVersion proverVersion()

get prover version of proof state

Returns:

the prover version

firstOrder

public boolean firstOrder()

is prover first order?

Returns:

true if prover is first order.

toLogical

public boolean toLogical()

is conversion BOOLEAN to LOGICAL to be applied?

Returns:

true if conversion is to be applied.

setAutoSimplify

public void setAutoSimplify(boolean on)

Set automatic simplification status of proof state

Parameters:

on - true iff automatic simplification is to be switched on

getChildren

public ProofState[] getChildren()

get children of proof state

Returns:

the children of the current state (null, if none)

setChildren

public void setChildren(Command command,
                        ProofState[] children)

set children of proof state

Parameters:

command - the command that generated the children

children - the new children of the state

getAssumption

public Formula getAssumption(java.lang.String label)

returns assumption with denoted label

Parameters:

label - the label

Returns:

formula or null, if there is no assumption with that label

getGoal

public Formula getGoal(java.lang.String label)

returns goal with denoted label

Parameters:

label - the label

Returns:

formula or null, if there is no goal with that label

getFormula

public Formula getFormula(java.lang.String label)

returns formula (assumption or goal) with denoted label

Parameters:

label - the label

Returns:

formula or null, if there is no formula with that label)

getSkolemTable

public UniqueNameTable getSkolemTable()

Get unique name table to be used for creating skolemization constants.

Returns:

the unique name table

setListener

public void setListener(ProofStateListener listener)

Set listener that is notified when proof state has changed.

Parameters:

listener - the listener that is notified.

getListener

public ProofStateListener getListener()

Get listener that is notified when proof state has changed.

Returns:

the listener that is notified.

hasChanged

public void hasChanged(boolean file)

Signal that state has changed updating presentation of this state.

Parameters:

file - true iff also presentation on file is to be changed.

print

public void print(java.io.PrintWriter out)

print proof state on output stream

Parameters:

out - the stream on which to print the formula

close

public void close(java.lang.String reason)

close the state.

Parameters:

reason - explanation why state is closed.

open

public void open()

open the state.

redo

public void redo()

Redo the proof at the denoted state (if possible)

labelChildren

public void labelChildren()

Label the children of the current state.

extend

public void extend(Command command,
                   ProofState[] children)

command extends current state by adding and labeling children

Parameters:

command - the command extending the state

children - the children of the proof state

isClosed

public boolean isClosed()

check whether proof state is closed

Returns:

true iff proof state is closed

simplify

public boolean simplify(boolean hard)

simplify the current proof state and potentially close it.

Parameters:

hard - true iff hard (and time-consuming) simplification is tried.

Returns:

true iff everything went okay.

copy

public Formula[] copy(Formula[] formulas)

Copy a sequence of formulas in this state.

Parameters:

formulas - a sequence of formulas

Returns:

a sequence of formulas all of which belong to this state such that this sequence equals formulas.

add

public Formula[] add(Formula[] formulas,
                     Formula formula)

Adds a formula to a sequence of formulas in this state.

Parameters:

formulas - a sequence of formulas

formula - a formula belonging to this state

Returns:

a sequence of formulas all of which belong to this state such that this sequence equals formulas appended by formula

add

public Formula[] add(Formula[] formulas,
                     Formula[] formulas0)

Adds a sequence of formulas to a sequence of formulas in this state.

Parameters:

formulas - a sequence of formulas

formulas0 - a sequence of formulas belonging to this state

Returns:

a sequence of formulas all of which belong to this state such that this sequence equals formulas appended by formulas0

remove

public Formula[] remove(Formula[] formulas,
                        Formula formula)

Remove a formula from a sequence of formulas in this state.

Parameters:

formulas - a sequence of formulas

formula - a formula occuring in that sequence once

Returns:

a sequence of formulas all of which belong to this state such that this sequence equals formulas without formula

replace

public Formula[] replace(Formula[] formulas,
                         Formula formula,
                         Formula rformula)

Replace a formula in a sequence of formulas in this state.

Parameters:

formulas - a sequence of formulas

formula - a formula occuring in that sequence once

rformula - a formula belonging to this state

Returns:

a sequence of formulas all of which belong to this state such that this sequence equals formulas without formula but includes rformula

print

public void print(java.io.PrintWriter out,
                  int level)

Print proof state including children.

Parameters:

out - the stream to print the state to.

level - the level of the proof state (0 = root).

addOpen

public void addOpen(java.util.Vector<ProofState> vector)

Add open state and all open children recursively to vector.

Parameters:

vector - vector receiving all open proof states.