|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.NDRules.NDRule
Pandora.NDRules.IffIntro
public class IffIntro
Implements the Iff Introduction rule.
Extends abstract class Rule.
Field Summary |
---|
Fields inherited from class Pandora.NDRules.NDRule |
---|
firstLine |
Constructor Summary | |
---|---|
IffIntro(ProofBox proof)
Constructs an IffIntro. |
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 |
---|
public IffIntro(ProofBox proof)
proof
- ProofBox representing in which box the rule is being appliedMethod Detail |
---|
public void addLine(ProofLine line)
addLine
in class NDRule
line
- ProofLine which has been selectedpublic boolean haveAll()
haveAll
in class NDRule
public void check() throws java.lang.Exception
check
in class NDRule
java.lang.Exception
public void apply() throws java.lang.Exception
apply
in class NDRule
java.lang.Exception
protected Formula getNewFormula(java.lang.String oldFormula, java.lang.String message) throws java.lang.Exception
getNewFormula
in class NDRule
oldFormula
- the formula with atoms that are not in the signature of the proof
java.lang.Exception
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |