fmrisc.ProofNavigator.Proving

Class Proof

java.lang.Object

fmrisc.ProofNavigator.Proving.Proof

public final class Proof
extends java.lang.Object

A proof represented by a tree of proof states.

Method Summary

Modifier and Type	Method and Description
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<Symbol>	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, State.ProverVersion proverVersion, boolean firstOrder, boolean toLogical) 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

newProof

public static Proof newProof(FormulaSymbol symbol,
                             boolean autoSimplify,
                             State.ProverVersion proverVersion,
                             boolean firstOrder,
                             boolean toLogical)

Construct new proof for formula denoted by symbol.

Parameters:

symbol - a formula symbol

autoSimplify - true iff automatic simplification is switched on

proverVersion - the version of the prover to be used

firstOrder - is prover first order?

toLogical - is conversion boolean to logical to be applied?

Returns:

the proof (null, if something went wrong)

isSkeleton

public boolean isSkeleton()

Is proof skeleton?

Returns:

true iff proof is skeleton.

setSkeleton

public void setSkeleton(boolean skeleton)

Signal whether proof is skeleton.

Parameters:

skeleton - true iff proof is skeleton.

isTrusted

public boolean isTrusted()

Is proof trusted?

Returns:

true iff proof is trusted.

setTrusted

public void setTrusted(boolean trusted)

Signal whether proof is trusted.

Parameters:

trusted - true iff proof is trusted.

isClosed

public boolean isClosed()

Is proof closed?

Returns:

true iff proof is closed.

setClosed

public void setClosed(boolean closed)

Signal whether proof is closed.

Parameters:

closed - true iff proof is closed.

isAbsolute

public boolean isAbsolute()

Is proof absolute?

Returns:

true iff proof is absolute.

setAbsolute

public void setAbsolute(boolean absolute)

Signal whether proof is closed.

Parameters:

absolute - true iff proof is closed.

getSymbol

public FormulaSymbol getSymbol()

get symbol of formula proved

Returns:

the symbol of the formula proved

getRoot

public ProofState getRoot()

get root of proof

Returns:

proof state that represents the root

getCurrent

public ProofState getCurrent()

get current open proof state

Returns:

current open proof state (null, if there is none)

setCurrent

public void setCurrent(ProofState state)

set current open proof state

Parameters:

state - an open proof state

getOpenGoal

public ProofState getOpenGoal()

get open leaf goal

Returns:

some open leaf goal (null, if there is none)

getOpenGoals

public ProofState[] getOpenGoals()

get open leaf goals

Returns:

array of open leaf goals

getState

public ProofState getState(java.lang.String tag)

Get proof state with denoted tag.

Parameters:

tag - the tag of the state

Returns:

the state with this tag (null, if there is no such state)

computeAbsolute

public void computeAbsolute()

The status of this proof or of the proof of a formula on which this proof depends may has changed. Compute and set the absoluteness state.

cut

public void cut(ProofState state)

Cut proof at denoted state.

Parameters:

state - state at which the proof is cut

close

public void close(ProofState state)

Inform proof that state was closed.

Parameters:

state - a proof state that was closed

redo

public boolean redo(ProofState state)

Redo proof at denoted state.

Parameters:

state - state at which the proof is redone.

Returns:

true iff proof could be redone

extend

public void extend(ProofState state,
                   ProofState[] children)

Inform proof that state was extended by children.

Parameters:

state - a proof state that was extended by children

children - open children states of state

nextOpenState

public void nextOpenState()

switch current state to next open state in sequence.

prevOpenState

public void prevOpenState()

switch current state to previous open state in sequence.

printStatus

public void printStatus(java.io.PrintWriter out)

Print status of proof to out

Parameters:

out - output stream.

getStatus

public java.lang.String getStatus()

Get status of proof.

Returns:

the status

print

public void print()

Print proof.

getReferenced

public java.util.Collection<Symbol> getReferenced()

Get collection of symbols of those entities referenced in the last call of toNode().

Returns:

collection of Symbol objects.

referenced

public void referenced(Identifier ident)

Mark identifier as referenced in current proof.

Parameters:

ident - the identifier that is marked as referenced.

toNode

public org.w3c.dom.Node toNode(org.w3c.dom.Document document)

Convert proof to DOM node in denoted document.

Parameters:

document - the document to which the proof belongs.

Returns:

the DOM node of the proof in this document.

toProof

public static Proof toProof(FormulaSymbol symbol,
                            org.w3c.dom.Node node)

Construct skeleton proof from DOM representation.

Parameters:

symbol - the symbol of the formula which is proved.

node - a DOM node representing the proof.

Returns:

the proof (null, if an error occured).

replay

public boolean replay()

Replay skeleton proof.

Returns:

true iff no error occured in replay

replay

public boolean replay(ProofState state)

Replay skeleton proof on proof state and its children.

Parameters:

state - the state on which the proof is to be replayed.

Returns:

true iff no error occured in replay.