Pandora.NDRules
Class IffIntroDerived

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

public class IffIntroDerived
extends NDRule

Implements the Iff Introduction Derived rule.
Extends abstract class Rule.


Field Summary
 
Fields inherited from class Pandora.NDRules.NDRule
firstLine
 
Constructor Summary
IffIntroDerived(ProofBox proof)
          Constructs an IffIntroDerived.
 
Method Summary
 void addLine(ProofLine clickedLine)
          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.
static boolean contradictory(Formula first, Formula second)
          Checks if the two formulas ar contradictory(One is the Not of the other one)
 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, getNewFormula
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

IffIntroDerived

public IffIntroDerived(ProofBox proof)
Constructs an IffIntroDerived.

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

addLine

public void addLine(ProofLine clickedLine)
             throws java.lang.Exception
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
Throws:
java.lang.Exception

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

contradictory

public static boolean contradictory(Formula first,
                                    Formula second)
Checks if the two formulas ar contradictory(One is the Not of the other one)

Parameters:
first - Formula represents the first formula
second - Formula represents the second formula to be compared against the first formula

apply

public void apply()
           throws java.lang.Exception
Called by the RuleController to apply the rule.
Applies backwards iff introduction derived.

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