Raptor.NDRules
Class ForallArrowElim

java.lang.Object
  Raptor.NDRules.NDRule
      Raptor.NDRules.ForallArrowElim

public class ForallArrowElim
extends NDRule

Implements the For All Arrow Elimination rule.
Extends abstract class NDRule.

Constructor Summary

ForallArrowElim(ProofBox pProof)
Constructs a ForallElim.

Method Summary

void	addLine(ProofLine pClickedLine) 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 pTerm) 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	compatible(Formula pFormula, Formula pImplies)
protected Term	getNewTerm(java.lang.String pOldTerm, java.lang.String pMessage, Formula pFormula) 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 pOldTerm, java.lang.String pMessage, Formula pFormula) 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 pOldTerm, java.lang.String pMessage, Formula pFormula) 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	intersection(java.util.List<Term> pLeftTerms, java.util.List<Term> pRightTerms, java.util.List<Var> pVars)
java.lang.String	show(java.util.List<Term> pTerms)

Methods inherited from class Raptor.NDRules.NDRule

addInputLine, checkSignature, getNewFormula

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ForallArrowElim

public ForallArrowElim(ProofBox pProof)

Constructs a ForallElim.

Parameters:

pProof - ProofBox representing in which box the rule is being applied

Method Detail

addLine

public void addLine(ProofLine pClickedLine)
             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:

pClickedLine - 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

compatible

public boolean compatible(Formula pFormula,
                          Formula pImplies)
                   throws java.lang.Exception

Throws:

java.lang.Exception

show

public java.lang.String show(java.util.List<Term> pTerms)

intersection

public void intersection(java.util.List<Term> pLeftTerms,
                         java.util.List<Term> pRightTerms,
                         java.util.List<Var> pVars)

checkSignature

public boolean checkSignature(Term pTerm)

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:

pTerm - Term represents the Term which is to be checked against the signature.

getTerm

protected Term getTerm(java.lang.String pOldTerm,
                       java.lang.String pMessage,
                       Formula pFormula)

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.

Parameters:

pOldTerm - String represents the previous invalid Term which has been input
and will appear as the default Term on the next dialog box.

pMessage - String represents the question message to appear on the dialog box.

pFormula - Formula represents the formula which must contain the returned Term as a free Term.

getNewTerm

protected Term getNewTerm(java.lang.String pOldTerm,
                          java.lang.String pMessage,
                          Formula pFormula)

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.

Parameters:

pOldTerm - String represents the previous invalid Term which has been input
and will appear as the default Term on the next dialog box.

pMessage - String represents the question message to appear on the dialog box.

pFormula - Formula represents the There Exists formula whose variable is to be replaced by the returned Term.

getVar

protected Var getVar(java.lang.String pOldTerm,
                     java.lang.String pMessage,
                     Formula pFormula)

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

Parameters:

pOldTerm - String represents the previous invalid Term which has been input
and will appear as the default Term on the next dialog box.

pMessage - String represents the question message to appear on the dialog box.

pFormula - Formula represents the formula which There Exists quantifier is to be applied on.