|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.NDRules.NDRule
Pandora.NDRules.ForallElim
public class ForallElim
Implements the For All Elimination rule.
Extends abstract class Rule.
Field Summary |
---|
Fields inherited from class Pandora.NDRules.NDRule |
---|
firstLine |
Constructor Summary | |
---|---|
ForallElim(ProofBox proof)
Constructs a ForallElim. |
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. |
boolean |
checkSignature(Term term)
Returns false if the passed Term clashes with or is not included in the signature of the box this rule is applied in, true otherwise. |
boolean |
checkVarSub(Formula f)
Only used when the rule is applied backwards to check if the passed formula can be reached by applying For All Elimination backwards on the selected line's formula. |
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. |
protected Term |
getNewTerm(java.lang.String oldTerm,
java.lang.String message,
Formula f)
This method is used only when For All Elimination rule is applied forwards, to get a term to substitute the For All variable formula. The returned Term must be in the signature of the box in which this rule is applied in. |
protected Term |
getTerm(java.lang.String oldTerm,
java.lang.String message,
Formula f)
This method is used only when For All Elimination rule is applied backwards, to get a term to substitute the new For All formula's variable. The returned Term must appear free in the passed formula. |
protected Var |
getVar(java.lang.String oldTerm,
java.lang.String message,
Formula f)
This method is used to get a new variable name for the newly introduced For All Formula The variable name must not clash with the signature of the box this rule is applied in. If the passed Formula already contains a quantifier formula, the returned variable must not be the same as its variables. I.e. |
boolean |
haveAll()
Returns true if the rule has all of the required input lines. |
void |
show(java.util.List<Term> terms)
|
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 ForallElim(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
public void show(java.util.List<Term> terms)
public boolean checkVarSub(Formula f) throws java.lang.Exception
java.lang.Exception
public boolean checkSignature(Term term)
t
- Term represents the Term which is to be checked against the signature.protected Term getTerm(java.lang.String oldTerm, java.lang.String message, Formula f)
oldTerm
- String represents the previous invalid Term which has been inputmessage
- String represents the question message to appear on the dialog box.f
- Formula represents the formula which must contain the returned Term as a free Term.protected Term getNewTerm(java.lang.String oldTerm, java.lang.String message, Formula f)
oldTerm
- String represents the previous invalid Term which has been inputmessage
- String represents the question message to appear on the dialog box.f
- Formula represents the There Exists formula whose variable is to be replaced by the returned Term.protected Var getVar(java.lang.String oldTerm, java.lang.String message, Formula f)
oldTerm
- String represents the previous invalid Term which has been inputmessage
- String represents the question message to appear on the dialog box.f
- Formula represents the formula which There Exists quantifier is to be applied on.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 |