Pandora.NDRules
Class NotElim

java.lang.Object
  Pandora.NDRules.NDRule
      Pandora.NDRules.NotElim

public class NotElim
extends NDRule

Implements the Not Elmination rule.
Extends abstract class Rule.

Field Summary

Fields inherited from class Pandora.NDRules.NDRule

firstLine

Constructor Summary

NotElim(ProofBox proof)
Constructs a NotElim.

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)
Formula	converse(Formula formula) 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.
boolean	haveAll() Returns true if the rule has all of the required input lines.

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

NotElim

public NotElim(ProofBox proof)

Constructs a NotElim.

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.

Specified by:

addLine in class NDRule

Parameters:

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

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.

Specified by:

apply in class NDRule

Throws:

java.lang.Exception

converse

public Formula converse(Formula formula)

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:

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