|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.NDRules.NDRule
Pandora.NDRules.FalsityIntro
public class FalsityIntro
Implements the Falsity Introduction rule.
Extends abstract class Rule.
Field Summary |
---|
Fields inherited from class Pandora.NDRules.NDRule |
---|
firstLine |
Constructor Summary | |
---|---|
FalsityIntro(ProofBox proof)
Constructs a FalsityIntro. |
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. |
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 |
---|
public FalsityIntro(ProofBox proof)
proof
- ProofBox representing in which box the rule is being appliedMethod Detail |
---|
public void addLine(ProofLine clickedLine) throws java.lang.Exception
addLine
in class NDRule
clickedLine
- ProofLine which has been selected
java.lang.Exception
public boolean haveAll()
haveAll
in class NDRule
public void check() throws java.lang.Exception
check
in class NDRule
java.lang.Exception
public static boolean contradictory(Formula first, Formula second)
first
- Formula represents the first formulasecond
- Formula represents the second formula to be compared against the first formulapublic void apply() throws java.lang.Exception
apply
in class NDRule
java.lang.Exception
public Formula converse(Formula formula)
formula
- Formula represents the formula which is to be negated.
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |