Raptor.NDRules
Class IffElimDerived

java.lang.Object
  Raptor.NDRules.NDRule
      Raptor.NDRules.IffElimDerived

public class IffElimDerived
extends NDRule

Implements the Iff Elimination Derived rule
Extends abstract class NDRule.

Constructor Summary

IffElimDerived(ProofBox pProof)
Constructs an IffElimDerived.

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.
static boolean	contradictory(Formula pFirst, Formula pSecond) 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 Raptor.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

IffElimDerived

public IffElimDerived(ProofBox pProof)

Constructs an IffElimDerived.

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.
This is an empty method as only one line is required to implement this rule.

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
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 pFirst,
                                    Formula pSecond)

Checks if the two formulas ar contradictory(One is the Not of the other one)

Parameters:

pFirst - Formula represents the first formula

pSecond - 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