|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.ObjectPandora.NDRules.NDRule
Pandora.NDRules.ExistsIntro
public class ExistsIntro
Implements the There Exists Introduction rule.
Extends abstract class Rule.
Field Summary |
---|
Fields inherited from class Pandora.NDRules.NDRule |
---|
firstLine |
Constructor Summary | |
---|---|
ExistsIntro(ProofBox proof)
Constructs an ExistsIntro. |
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 forwards to check if the passed formula can be reached by applying There Exists Introduction forwards 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. Creates a dialog box asking the user to input a new formula. Parses the new formula and gives the user options of what to do if the atoms are not in the signature. The options are the add the atoms to the signature, cancel the rule or to type a new formula. Returns a formula entered by the user, whose atoms are now 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 There Exists Introduction rule is applied backwards, to get a term to substitute the There Exists 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 There Exists Introduction rule is applied forwards, to get a term to substitute the new There Exists 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 There Exists 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. |
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 ExistsIntro(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 boolean checkVarSub(Formula f) throws java.lang.Exception
f
- Formula represents the formula which is to be checked if is reachable.
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 |