|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.NDRules.NDRule
Pandora.NDRules.ForallIntro
public class ForallIntro
Implements the For All Introduction rule.
Extends abstract class Rule.
Field Summary |
---|
Fields inherited from class Pandora.NDRules.NDRule |
---|
firstLine |
Constructor Summary | |
---|---|
ForallIntro(ProofBox proof)
Constructs a ForallIntro. |
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. |
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. |
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 ForallIntro(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 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 |