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.
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.
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 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 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 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 Assignment Statement clashes with a signature if any of its left or
right PTerms clash 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 If Statement clashes with a signature if any of its condition, if
branch or else branch clash 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 Instruction clashes with a signature if any of its parts clash 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 Method Statement clashes with a signature if any of its parts clash
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.
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 ""
A PVar Statement clashes with a signature if any of its parts clash 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.
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 ""
A PVar Statement clashes with a signature if any of its parts clash 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 PNum clashes with a signature if any of its parts clash 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 PTerm clashes with a signature if any of its parts clash 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 PVar Statement clashes with a signature if any of its parts clash 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 Skip Statement doesn't clash 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 Statement clashes with a signature if any of its left or right
Instructions clash 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 While Statement clashes with a signature if any of its condition or
code clash with the signature.
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.
Carries out the methods required to show and record that a ProgramLine
has been deselected without clearing the last selected item for the
ProofWindow.
Carries out the methods required to show and record that a ProgramLine
has been deselected without clearing the last selected item for the
ProofWindow.
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.
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 Raptor.LogicParser.sym
error -
Static variable in class Raptor.ProgramParser.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 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.
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.
Returns true if the PanSignature is empty.
A PanSignature is empty if its Predicate, Constant, VVar, PVar, AArray,
PArray and the Function lists are empty.
setAtoms() -
Method in class Raptor.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 Raptor.LogicParser.Formula.Sk
Adds this atom to the list of atoms for the formula.
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 Raptor.LogicParser.Formula.Term