Pandora.NDRules
Class ImpliesIntro

java.lang.Object
  extended by Pandora.NDRules.NDRule
      extended by Pandora.NDRules.ImpliesIntro

public class ImpliesIntro
extends NDRule

Implements the Implies Introduction rule.
Extends abstract class Rule.


Field Summary
 
Fields inherited from class Pandora.NDRules.NDRule
firstLine
 
Constructor Summary
ImpliesIntro(ProofBox proof)
          Constructs an ImpliesIntro.
 
Method Summary
 void addLine(ProofLine line)
          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.
protected  Formula getNewFormula(java.lang.String oldFormula, java.lang.String message)
          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
Only the first line is required so this method returns true.
 
Methods inherited from class Pandora.NDRules.NDRule
addInputLine, checkSignature
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

ImpliesIntro

public ImpliesIntro(ProofBox proof)
Constructs an ImpliesIntro.

Parameters:
proof - ProofBox representing in which box the rule is being applied
Method Detail

addLine

public void addLine(ProofLine line)
Adds the extra lines to the rule once the input line has been added.
This is an empty method as only one line is required to implement this rule.

Specified by:
addLine in class NDRule
Parameters:
line - ProofLine which has been selected

haveAll

public boolean haveAll()
Returns true if the rule has all of the required input lines
Only the first line is required so this method returns true.

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.
Applies backwards implies introduction.

Specified by:
apply in class NDRule
Throws:
java.lang.Exception

getNewFormula

protected Formula getNewFormula(java.lang.String oldFormula,
                                java.lang.String message)
                         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:
oldFormula - the formula with atoms that are not in the signature of the proof
Throws:
java.lang.Exception