Raptor.NDRules
Class NotIntro

java.lang.Object
  Raptor.NDRules.NDRule
      Raptor.NDRules.NotIntro

public class NotIntro
extends NDRule

Implements the Not Introduction rule
Extends abstract class NDRule.

Constructor Summary

NotIntro(ProofBox pProof)
Constructs an NotIntro.

Method Summary

void	addLine(ProofLine pClickedLine) Adds the extra lines to the rule once the input line has been added.
void	apply() Called by the RuleController to apply the rule.
void	check() Called by the RuleController to check the input lines to the rule.
Formula	converse(Formula pFormula) Returns the negated form of the given formula If the formula is already negated it will remove the Not sign (e.g.
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.
boolean	haveAll() Returns true if the rule has all of the required input lines.

Methods inherited from class Raptor.NDRules.NDRule

addInputLine, checkSignature

Methods inherited from class java.lang.Object

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

Constructor Detail

NotIntro

public NotIntro(ProofBox pProof)

Constructs an NotIntro.

Parameters:

pProof - ProofBox representing in which box the rule is being applied

Method Detail

addLine

public void addLine(ProofLine pClickedLine)
             throws java.lang.Exception

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

Specified by:

addLine in class NDRule

Parameters:

pClickedLine - ProofLine which has been selected

Throws:

java.lang.Exception

haveAll

public boolean haveAll()

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

Specified by:

haveAll in class NDRule

check

public void check()
           throws java.lang.Exception

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

Specified by:

check in class NDRule

Throws:

java.lang.Exception

apply

public void apply()
           throws java.lang.Exception

Called by the RuleController to apply the rule.

Specified by:

apply in class NDRule

Throws:

java.lang.Exception

converse

public Formula converse(Formula pFormula)

Returns the negated form of the given formula
If the formula is already negated it will remove the Not sign (e.g. ~a --> a)
Otherwise the formula is negated (e.g. a --> ~a) or (e.g. ~~a --> ~~~a).

Parameters:

pFormula - Formula represents the formula which is to be negated.

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.

Overrides:

getNewFormula in class NDRule

Parameters:

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

Throws:

java.lang.Exception