Pandora.NDRules
Class ExistsIntro

java.lang.Object
  extended by Pandora.NDRules.NDRule
      extended by Pandora.NDRules.ExistsIntro

public class ExistsIntro
extends NDRule

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

ExistsIntro

public ExistsIntro(ProofBox proof)
Constructs an ExistsIntro.

Parameters:
proof - ProofBox representing in which box the rule is being applied
Method Detail

addLine

public void addLine(ProofLine clickedLine)
             throws java.lang.Exception
Adds the extra lines to the rule once the input line has been added.

Specified by:
addLine in class NDRule
Parameters:
clickedLine - ProofLine which has been selected
Throws:
java.lang.Exception

haveAll

public boolean haveAll()
Returns true if the rule has all of the required input lines.

Specified by:
haveAll in class NDRule

check

public void check()
           throws java.lang.Exception
Called by the RuleController to check the input lines to the rule.

Specified by:
check in class NDRule
Throws:
java.lang.Exception

apply

public void apply()
           throws java.lang.Exception
Called by the RuleController to apply the rule.

Specified by:
apply in class NDRule
Throws:
java.lang.Exception

checkVarSub

public boolean checkVarSub(Formula f)
                    throws java.lang.Exception
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.

Parameters:
f - Formula represents the formula which is to be checked if is reachable.
Throws:
java.lang.Exception

checkSignature

public 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.

Parameters:
t - Term represents the Term which is to be checked against the signature.

getTerm

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.

Parameters:
oldTerm - String represents the previous invalid Term which has been input
and will appear as the default Term on the next dialog box.
message - 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.

getNewTerm

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.

Parameters:
oldTerm - String represents the previous invalid Term which has been input
and will appear as the default Term on the next dialog box.
message - 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.

getVar

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. Nested variables are not allowed.

Parameters:
oldTerm - String represents the previous invalid Term which has been input
and will appear as the default Term on the next dialog box.
message - 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.

getNewFormula

protected Formula getNewFormula(java.lang.String oldFormula,
                                java.lang.String message)
                         throws java.lang.Exception
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.

Overrides:
getNewFormula in class NDRule
Parameters:
oldFormula - the formula with atoms that are not in the signature of the proof
Throws:
java.lang.Exception