This method adds this Atom to the passed PanSignature's Predicate list IF it is not already in the signature
If this Atom is an instance of Predicate, its Parameters will be added to the signature as well.
This method adds this Formula to the passed PanSignature's Predicate list IF it is not already in the signature
If this Formula is an instance of Predicate, its Parameters will be added to the signature as well
This method adds this Formula to the passed PanSignature's Predicate list IF it is not already in the signature
If this Formula is an instance of Predicate, its Parameters will be added to the signature as well
A helper function used by the checkSub method
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Formula.
A helper function used by th checkSub method
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Predicate.
Returns true if the given formula contains only predicates/terms/functions already in the signature of the proof
and if it does not clash with any of the previously declared predicates/functions and constants.
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Predicate
If no Term is passed to be substituted(a = null) it is the case that we have to check if formula f can be reached
by substituting any of its Terms.
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.
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.
Only used when the rule is applied backwards to check if the passed formula can be reached
by applying For All Tick backwards on the selected line's formula.
Returns a String of error message if this Term clashes with the passed PanSignature.
A Term clashes with a PanSignature if it clashes with any of its Predicates,Constants,Functions or Variables.
If this Term does not clash with the Signature, it is added to the signature and an empty String is returned.
Returns a String containing an Error character if this Formula clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An And Formula clashes with a signature if any of its left or right sub-Formulae clashes with the signature.
Returns a String containing an Error character if this Atom clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An Atom clashes with a signature if it clashes with any of its Predicates/Functions/Constants/Variables
Returns a String of error message if this Term clashes with the passed PanSignature.
A Term clashes with a PanSignature if it clashes with any of its Predicates,Constants,Functions or Variables.
If this Term does not clash with the Signature, it is added to the signature and an empty String is returned.
Returns true if the passed Term(Constant/Function/Variable) clashes with this Function
A Function clashes with a Term if they have the same name.
Two Functions clash if they have the same name but different arities.
Returns a String of error message if this Function clashes with the passed PanSignature
A Function clashes with a PanSignature if it clashes with any of its Predicates,Constants, Functions or Variables.
If this Function does not clash with the Signature, the Function is added to the Function list of the signature
and an empty String is returned.
Returns a String containing an Error character if this Formula clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An Iff Formula clashes with a signature if any of its left or right sub-Formulae clashes with the signature.
Returns a String containing an Error character if this Formula clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An Implies Formula clashes with a signature if any of its left or right sub-Formulae clashes with the signature.
Returns a String containing an Error character if this Formula clashes with the passed PanSignature, Otherwise it will return an Empty String ""
A Not Formula clashes with a signature if any of its left or right sub-Formulae clashes with the signature.
Returns a String of error message if this Term clashes with the passed PanSignature
A Term clashes with a PanSignature if it clashes with any of its Predicates,Constants,Functions or Variables.
I.e.
Returns a String containing an Error character if this Formula clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An Or Formula clashes with a signature if any of its left or right sub-Formulae clashes with the signature.
Returns a String containing an Error character if this Formula clashes with the passed PanSignature, Otherwise it will return an Empty String ""
A Quantifier Formula clashes with a signature if its variable or its Formula clashes with the signature.
Returns a String of error message if this SimpleTerm clashes with the passed PanSignature
A SimpleTerm clashes with a PanSignature if it clashes with any of its Predicates,Constants,Functions or Variables.
If this SimpleTerm does not clash with the Signature, it is added to the Constant list of the signature
and an empty String is returned.
Returns a String containing an Error character if this Atom clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An Atom clashes with a signature if it clashes with any of its Predicates/Functions/Constants/Variables
Returns a String of error message if this Term clashes with the passed PanSignature
A Term clashes with a PanSignature if it clashes with any of its Predicates,Constants,Functions or Variables.
If this Term does not clash with the Signature, it is added to the signature and an empty String is returned.
Returns a String of error message if this Term clashes with the passed PanSignature
A Term clashes with a PanSignature if it clashes with any of its Predicates,Constants,Functions or Variables.
If this Term does not clash with the Signature, it is added to the signature and an empty String is returned.
Returns a String of error message if this Term clashes with the passed PanSignature
A Term clashes with a PanSignature if it clashes with any of its Predicates,Constants,Functions or Variables.
If this Term does not clash with the Signature, it is added to the signature and an empty String is returned.
Returns a String containing an Error character if this Unknown clashes with the passed PanSignature, Otherwise it will return an Empty String ""
An Atom clashes with a signature if it clashes with any of its Predicates/Functions/Constants/Variables.
Returns a String of error message if this Var clashes with the passed PanSignature.
A Var clashes with a PanSignature if it clashes with any of its Predicates,Constants,Functions or Variables.
If this Var does not clash with the Signature, it is added to the Variable list of the signature
and an empty String is returned.
Returns a PanSignature containing the difference of this signature and the passed signature
I.e The returned signature will contain all Predicates/Functions/SimpleTerms/Variables that the passed signaure contains
and this signature doesn't.
Returns the negated form of the given formula
If the formula is already negated it will remove the Not sign (e.g.~a --> a)
Otherwise the formula is negated (e.g.
Returns true if the passed Function is equal to this Function
Two Functions are equal if they have the same name,same arity and the same parameters in the same order.
equals(Term) -
Method in class Pandora.LogicParser.Formula.Num
Returns true if the passed Term is equal to this Term
Returns true if the passed Function is equal to this Function
Two Functions are equal if they have the same name,same arity and the same parameters in the same order.
error -
Static variable in class Pandora.LogicParser.sym
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.
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.
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.
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.
This method is used only when Reflexivity rule is applied forwards,
to get a term to substitute the left and right hand side of the newly introduced Equals Formula.
The returned Term must be in the signature of the box in which this rule is applied in.
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.
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.
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.
getTerms() -
Method in class Pandora.LogicParser.Formula.And
This method returns a list of all the Terms this formula contain.
getTerms() -
Method in class Pandora.LogicParser.Formula.Atom
This method returns a list of all the Terms this formula contain.
i.e.
getTerms() -
Method in class Pandora.LogicParser.Formula.BExp.BExp
Returns both left and right side of the boolean expression in a list of Terms.
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.
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.
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.
Obtains the atoms in the formula and adds them to the list of atoms for the tree which contains this formula.
setAtoms() -
Method in class Pandora.LogicParser.Formula.Not
Obtains the atoms in the formula and adds them to the list of atoms for the tree which contains this formula.
setAtoms() -
Method in class Pandora.LogicParser.Formula.Or
Obtains the atoms in the formula and adds them to the list of atoms for the tree which contains this formula.
The list of atoms is found in Formula class.
setAtoms() -
Method in class Pandora.LogicParser.Formula.Sk
Adds the list of Atoms in a given tree to the list of Atoms.
This abstract class is the superclass of all classes that represent a term in Pnadora
As in Pandora we use first order predicate logic a term can be:
A Constant
A Variable
A Function
Term() -
Constructor for class Pandora.LogicParser.Formula.Term