Raptor.NDRules
Class NDRule

java.lang.Object
  Raptor.NDRules.NDRule

Direct Known Subclasses:

AndElim, AndIntro, EM, ExistsElim, ExistsIntro, FalsityElim, FalsityIntro, ForallArrowElim, ForallElim, ForallIntro, ForallTick, IffElim, IffElimDerived, IffIntro, IffIntroDerived, ImpliesElim, ImpliesIntro, Instantiate, Lemma, NotElim, NotIntro, NotNot, OrElim, OrIntro, PC, Reflexivity, Substitution, Tick, TM, TMTick, TopIntro

public abstract class NDRule
extends java.lang.Object

Abstract NDRule class.
Extended by each of the rule classes.

Constructor Summary

NDRule(ProofBox pProof)

Method Summary

void	addInputLine(ProofLine pLine) Adds the input line to the rule.
abstract void	addLine(ProofLine pLine) Adds the extra lines to the rule once the input line has been added.
abstract void	apply() Called by the controller to apply the rule.
abstract void	check() Called by the controller to check the input lines to the rule.
boolean	checkSignature(Formula pFormula) Returns true if the given formula contains only predicates/terms/functions already in the signature of the proof and if it does not clash with any of the previously declared predicates/functions and constants.
protected Formula	getNewFormula(java.lang.String pOldFormula, java.lang.String pMessage) Takes as input a formula that was rejected because its atoms were not in the signature of the proof.
abstract boolean	haveAll() Returns true if the rule ahs all of the required input lines.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

NDRule

public NDRule(ProofBox pProof)

Method Detail

addInputLine

public void addInputLine(ProofLine pLine)
                  throws java.lang.Exception

Adds the input line to the rule.
The line is checked to ensure it is an empty line or a goal.

Parameters:

pLine - ProofLine which is the first line selected

Throws:

java.lang.Exception

haveAll

public abstract boolean haveAll()

Returns true if the rule ahs all of the required input lines.

addLine

public abstract void addLine(ProofLine pLine)
                      throws java.lang.Exception

Adds the extra lines to the rule once the input line has been added.

Parameters:

pLine - ProofLine which has been selected

Throws:

java.lang.Exception

check

public abstract void check()
                    throws java.lang.Exception

Called by the controller to check the input lines to the rule.

Throws:

java.lang.Exception

apply

public abstract void apply()
                    throws java.lang.Exception

Called by the controller to apply the rule.

Throws:

java.lang.Exception

checkSignature

public boolean checkSignature(Formula pFormula)

Returns true if the given formula contains only predicates/terms/functions already in the signature of the proof
and if it does not clash with any of the previously declared predicates/functions and constants.

Parameters:

pFormula - the formula to be checked against the signature

getNewFormula

protected Formula getNewFormula(java.lang.String pOldFormula,
                                java.lang.String pMessage)
                         throws java.lang.Exception

Takes as input a formula that was rejected because its atoms were not in the signature of the proof.
Creates a dialog box asking the user to input a new formula.
Parses the new formula and gives the user options of what to do if the atoms are not in the signature.
The options are the add the atoms to the signature, cancel the rule or to type a new formula.
Returns a formula entered by the user, whose atoms are now in the signature of the proof.

Parameters:

pOldFormula - the formula with atoms that are not in the signature of the proof

Throws:

java.lang.Exception