A B C D E F G H I J K L M N O P Q R S T U V W Y _

A

accept(File) - Method in class Pandora.xGui.PandoraFileFilter
Tests whether or not the specified abstract pathname should be included in the pathname list.
action_obj - Variable in class Pandora.LogicParser.parser
Instance of action encapsulation class.
action_table() - Method in class Pandora.LogicParser.parser
Access to parse-action table.
actionPerformed(ActionEvent) - Method in class Pandora.Help.Help
Handles the events thrown by the TextFieldListener and action Listeners attached to the Search and Radio Buttons.
actionPerformed(ActionEvent) - Method in class Pandora.ProofWindow
Performs actions performed within the ProofWindow
actionPerformed(ActionEvent) - Method in class Pandora.View
Handles actions carried out in Pandora.
Add - Class in Pandora.LogicParser.Formula.AExp
Creates an addition expression.
Add(Term, Term) - Constructor for class Pandora.LogicParser.Formula.AExp.Add
Constructs a new Add AExp.
addConstant(String) - Method in class Pandora.PanSignature
This method is called when a user wants to add a new Constant to the signature via the "Add to signtaure" option on the menu.
addConstant() - Method in class Pandora.ProofWindow
Adds a Constant to the signature
addConstsToSignature(List<SimpleTerm>) - Method in class Pandora.PanSignature
Adds all the SimpleTerms in the passed SimpleTerm List to this PanSignature's Constant list IF the signature does not already contain them.
addFirstLine(ProofLine) - Method in class Pandora.RuleController
Takes the first selected line and stores it in currentLine.
addFuncsToSignature(List<Function>) - Method in class Pandora.PanSignature
Adds all the Functions in the passed Function List to this PanSignature's Function list IF the signature does not already contain them.
addFunction(String, int) - Method in class Pandora.PanSignature
This method is called when a user wants to add a new function to the signature via the "Add to signtaure" option on the menu.
addFunction() - Method in class Pandora.ProofWindow
Adds a Function to the signature
addInputLine(ProofLine) - Method in class Pandora.NDRules.ForallTick
Adds the input line to the rule.
The line is checked to ensure it is a goal line.
addInputLine(ProofLine) - Method in class Pandora.NDRules.NDRule
Adds the input line to the rule.
addItem(ProofItem) - Method in class Pandora.ProofBox
Adds ProofItem to the LinkedList of ProofItems in the ProofBox.
addItem(int, ProofItem) - Method in class Pandora.ProofBox
Adds ProofItem to specified position in LinkedList of ProofItems.
addKW(String) - Method in class Pandora.Help.HelpAccessProcedures
Adds the specified keyword to the keyword list of the file if it does not already contain it.
addLine(ProofLine) - Method in class Pandora.NDRuleController
Adds the given ProofLine to the proof as extra input.
addLine(ProofLine) - Method in class Pandora.NDRules.AndElim
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.AndIntro
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.EM
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.ExistsElim
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.ExistsIntro
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.FalsityElim
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.FalsityIntro
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.ForallArrowElim
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.ForallArrowIntro
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.ForallElim
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.ForallIntro
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.ForallTick
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.IffElim
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.IffElimDerived
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.IffIntro
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.IffIntroDerived
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.ImpliesElim
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.ImpliesIntro
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.Instantiate
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.Lemma
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.NDRule
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.NotElim
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.NotIntro
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.NotNot
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.OrElim
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.OrIntro
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.PC
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.Reflexivity
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.Substitution
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.Tick
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.TM
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.TMTick
Adds the extra lines to the rule once the input line has been added.
addLine(ProofLine) - Method in class Pandora.NDRules.TopIntro
Adds the extra lines to the rule once the input line has been added.
addLineToProof(Formula, String) - Method in class Pandora.ProofWindow
Adds a ProofLine while in solveProofMode
addPredicate(String, int) - Method in class Pandora.PanSignature
This method is called when a user wants to add a new Predicate to the signature via the "Add to signtaure" option on the menu.
addPredicate() - Method in class Pandora.ProofWindow
Adds a Predicate to the signature
addProofWindow() - Method in class Pandora.View
Creates a new tab for proof window.
addProofWindow(String) - Method in class Pandora.View
Creates a new tab with specified title for proof window
addRule(String) - Method in class Pandora.RuleController
Creates a NDRuleController.
addSkolems(ProofBox, PanSignature) - Method in class Pandora.ProofBox
 
addTermsToSignature(List<Term>) - Method in class Pandora.PanSignature
Adds all the Terms in the passed Term List to this PanSignature IF the signature does not already contain them.
addToGiven(String) - Method in class Pandora.ProofWindow
Allows a string to be appended to the givens text box in enterProofMode
addToGoal(String) - Method in class Pandora.ProofWindow
Allows a string to be appended to the goal text box in enterProofMode
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.AExp.AExp
This method adds this Term to the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.And
This method adds the Atoms and Terms of this Formula to the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Atom
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.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.BExp.BExp
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
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Exists
This method adds this Formula to the passed PanSignature's IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Forall
This method adds this Formula to the passed PanSignature's IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Formula
This method adds this Formula to the passed PanSignature's Predicate list IF it is not already in the signature
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Function
This method adds this Function to the Function List and its Terms to the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Iff
This method adds the Atoms and Terms of this Formula to the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Implies
This method adds the Atoms and Terms of this Formula to the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Not
This method adds the Atoms and Terms of this Formula to the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Num
This method adds this Term to the passed PanSignature IF it is not already in the signature
I.e.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Or
This method adds the Atoms and Terms of this Formula to the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.SimpleTerm
This method adds this SimpleTerm to the Constant List of the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.SkTerm
This method adds this Term to the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.SVar
This method adds this Term to the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Term
This method adds this Term to the passed PanSignature IF it is not already in the signature
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Unknown
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
addToSignature(PanSignature) - Method in class Pandora.LogicParser.Formula.Var
This method adds this Var to the Variable List of the passed PanSignature IF it is not already in the signature.
addToSignature(PanSignature) - Method in class Pandora.PanSignature
 
addToSignature(List<Atom>) - Method in class Pandora.PanSignature
Adds all the Atoms in the passed Atom List to this PanSignature's Predicate list IF the signature does not already contain them.
addToSignature(List<Atom>) - Method in class Pandora.ProofBox
Adds the given list of Atoms to the signature of the ProofBox.
addVarsToSignature(List<Var>) - Method in class Pandora.PanSignature
Adds all the Vars in the passed Var List to this PanSignature's Var list IF the signature does not already contain them.
addVarToSignature(Var) - Method in class Pandora.PanSignature
Adds the passed Var to this PanSignature's Variable list IF the signature does not already contain them.
AExp - Class in Pandora.LogicParser.Formula.AExp
Abstract class for arithmetic expressions.
AExp() - Constructor for class Pandora.LogicParser.Formula.AExp.AExp
 
and - Static variable in class Pandora.Help.ErrorMessages
 
and - Static variable in class Pandora.Help.HelpMessages
 
And - Class in Pandora.LogicParser.Formula
The And formula.
Extends abstract Formula class.
And(Formula, Formula) - Constructor for class Pandora.LogicParser.Formula.And
Constructs an And Formula.
AND - Static variable in class Pandora.LogicParser.sym
 
and_elimination - Variable in class Pandora.Help.HelpMessages
 
and_elimination_input_left - Variable in class Pandora.Help.HelpMessages
 
and_elimination_input_right - Variable in class Pandora.Help.HelpMessages
 
and_forwards - Static variable in class Pandora.Help.ErrorMessages
 
AndElim - Class in Pandora.NDRules
Implements the And Elmination rule.
Extends abstract class Rule.
AndElim(ProofBox) - Constructor for class Pandora.NDRules.AndElim
Constructs an AndElim.
AndElim - Static variable in class Pandora.Types
 
AndEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the And Elimination Rule.
AndEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'AndEliminationFile'.
AndIntro - Class in Pandora.NDRules
Implements the And Introduction rule.
Extends abstract class Rule.
AndIntro(ProofBox) - Constructor for class Pandora.NDRules.AndIntro
Constructs an AndIntro.
AndIntro - Static variable in class Pandora.Types
 
AndIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the And Introduction Rule.
AndIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'AndIntroductionFile'.
apply() - Method in class Pandora.NDRuleController
Called by RuleController to apply the RAPRule.
apply() - Method in class Pandora.NDRules.AndElim
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.AndIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.EM
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.ExistsElim
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.ExistsIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.FalsityElim
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.FalsityIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.ForallArrowElim
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.ForallArrowIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.ForallElim
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.ForallIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.ForallTick
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.IffElim
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.IffElimDerived
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.IffIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.IffIntroDerived
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.ImpliesElim
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.ImpliesIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.Instantiate
Called by the controller to apply the instantiate rule.
apply() - Method in class Pandora.NDRules.Lemma
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.NDRule
Called by the controller to apply the rule.
apply() - Method in class Pandora.NDRules.NotElim
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.NotIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.NotNot
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.OrElim
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.OrIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.PC
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.Reflexivity
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.Substitution
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.Tick
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.TM
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.TMTick
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.NDRules.TopIntro
Called by the RuleController to apply the rule.
apply() - Method in class Pandora.RuleController
First call adds the currentLine to the currentRule.
applyFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Apply Menu.
applyFont(JComponent, String) - Method in class Pandora.View
 
applyKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'applyFile'.
arrow - Static variable in class Pandora.Help.ErrorMessages
 
arrow - Static variable in class Pandora.Help.HelpMessages
 
arrow_backwards - Static variable in class Pandora.Help.ErrorMessages
 
ArrowEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Arrow Elimination Rule.
ArrowEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'ArrowEliminationFile'.
ArrowIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Arrow Introduction Rule.
ArrowIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'ArrowIntroductionFile'.
artisticGreen - Static variable in class Pandora.xGui.Colour
 
artisticSlightlyMoreGreenThanTennisBallYellowGreen - Static variable in class Pandora.xGui.Colour
 
Assume - Static variable in class Pandora.Types
 
Atom - Class in Pandora.LogicParser.Formula
The Atom formula.
Extends abstract class Formula.
Atom(String) - Constructor for class Pandora.LogicParser.Formula.Atom
Constructs an Atom Formula.

B

basicConceptsFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Basic Concepts.
basicConceptsKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'basicConceptsFile'.
BExp - Class in Pandora.LogicParser.Formula.BExp
Abstract class for boolean expressions.
BExp() - Constructor for class Pandora.LogicParser.Formula.BExp.BExp
 
black - Static variable in class Pandora.xGui.Colour
 
borderBlue - Static variable in class Pandora.xGui.Colour
 
BOTTOM - Static variable in class Pandora.LogicParser.sym
 
BottomEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Bottom Elimination Rule.
BottomEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'BottomEliminationFile'.

C

changeFontSize(int) - Method in class Pandora.View
Changes the size of font in View
check(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Formula
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y
check() - Method in class Pandora.NDRules.AndElim
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.AndIntro
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.EM
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.ExistsElim
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.ExistsIntro
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.FalsityElim
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.FalsityIntro
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.ForallArrowElim
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.ForallArrowIntro
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.ForallElim
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.ForallIntro
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.ForallTick
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.IffElim
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.IffElimDerived
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.IffIntro
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.IffIntroDerived
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.ImpliesElim
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.ImpliesIntro
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.Instantiate
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.Lemma
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.NDRule
Called by the controller to check the input lines to the rule.
check() - Method in class Pandora.NDRules.NotElim
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.NotIntro
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.NotNot
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.OrElim
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.OrIntro
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.PC
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.Reflexivity
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.Substitution
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.Tick
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.TM
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.TMTick
Called by the RuleController to check the input lines to the rule.
check() - Method in class Pandora.NDRules.TopIntro
Called by the RuleController to check the input lines to the rule.
check2(Term, Term, Equals) - Method in class Pandora.LogicParser.Formula.Equals
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.
check2(Term, Term, Predicate) - Method in class Pandora.LogicParser.Formula.Predicate
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.
checkFunc(Function, Function) - Method in class Pandora.LogicParser.Formula.Predicate
 
checkGoal(String, ProofWindow) - Method in class Pandora.ParseInputController
Parses the goal which has been input and allows further input.
checkInput(String, ProofWindow) - Method in class Pandora.ParseInputController
Parses the givens which have been input and allows further input.
checkSignature(Term) - Method in class Pandora.NDRules.ExistsIntro
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.
checkSignature(Term) - Method in class Pandora.NDRules.ForallArrowElim
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.
checkSignature(Term) - Method in class Pandora.NDRules.ForallElim
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.
checkSignature(Formula) - Method in class Pandora.NDRules.NDRule
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.
checkSignature(Term) - Method in class Pandora.NDRules.Reflexivity
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.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.And
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Formula
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Atom
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Atom
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.BExp.BExp
Returns true if the passed formula f can be reached by substituting the occurrences of Term x by Term y.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Equals
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Formula.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Exists
Returns true if the passed formula f can be reached by substituting the occurrences of Term x by Term y.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.False
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Formula.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Forall
Returns true if the passed formula f can be reached by substituting the occurrences of Term x by Term y.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Formula
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Iff
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Formula.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Implies
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Formula.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Not
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Formula.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Or
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Formula.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Predicate
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.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.True
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Formula.
checkSub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Unknown
Returns true if the passed formula f can be reached by substituting th eoccurrences of Term x by Term y in this Unknown.
checkVarSub(Formula) - Method in class Pandora.NDRules.ExistsIntro
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.
checkVarSub(Formula) - Method in class Pandora.NDRules.ForallElim
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.
checkVarSub(Formula, Formula) - Method in class Pandora.NDRules.ForallTick
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.AExp.AExp
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.And
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.
clashes(Atom) - Method in class Pandora.LogicParser.Formula.Atom
Returns true if this Atom clashes with the passed Atom
An Atom clashes with another Atom if they have the same name but different arities.
clashes(Term) - Method in class Pandora.LogicParser.Formula.Atom
Returns true if this Atom clashes with the passed Term
An Atom clashes with a Term if they have the same name.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Atom
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
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.BExp.BExp
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.False
Returns an Empty String "" as a bottom formula never clashes with a signature.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Formula
Returns a String containing an Error character if this Formula clashes with the passed PanSignature, Otherwise it will return an Empty String ""
clashes(Atom) - Method in class Pandora.LogicParser.Formula.Function
Returns true if the passed Atom clashes with this Function
An Atom clashes with a Function if they have the same name.
clashes(Term) - Method in class Pandora.LogicParser.Formula.Function
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Function
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Iff
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Implies
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Not
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Num
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Or
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Quantifier
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.
clashes(Atom) - Method in class Pandora.LogicParser.Formula.SimpleTerm
Returns true if the passed Atom clashes with this SimpleTerm
An Atom clashes with a SimpleTerm if they have the same name.
clashes(Term) - Method in class Pandora.LogicParser.Formula.SimpleTerm
Returns true if the passed Term(Constant/Function/Variable) clashes with this SimpleTerm
A SimpleTerm clashes with a Term if they have the same name.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.SimpleTerm
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Sk
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
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.SkTerm
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.SVar
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Term
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.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.True
Returns an Empty String "" as a top formula never clashes with a signature.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Unknown
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.
clashes(Atom) - Method in class Pandora.LogicParser.Formula.Var
Returns true if the passed Atom clashes with this Var
An Atom clashes with a Var if they have the same name.
clashes(Term) - Method in class Pandora.LogicParser.Formula.Var
Returns true if the passed Term(Constant/Function/Var) clashes with this Var.
A Var clashes with a Term if they have the same name.
clashes(PanSignature) - Method in class Pandora.LogicParser.Formula.Var
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.
cleanup() - Method in class Pandora.ProofBox
Removes the empty line before a goal line when that goal has become proved but there are still goals remaining in the proof.
clearLastRuleSelected() - Method in class Pandora.ProofWindow
Resets the button which was last selected
clearLastSelectedLine() - Method in class Pandora.ProofWindow
Deselects the selected ProofItem
clone() - Method in class Pandora.LogicParser.Formula.AExp.AExp
Returns a copy(clone) of this Term.
clone() - Method in class Pandora.LogicParser.Formula.Function
Returns a copy(clone) of this Function.
clone() - Method in class Pandora.LogicParser.Formula.Num
Returns a copy(clone) of this Term.
clone() - Method in class Pandora.LogicParser.Formula.Predicate
Returns a clone(copy) of this Predicate.
clone() - Method in class Pandora.LogicParser.Formula.SimpleTerm
Returns a copy(clone) of this SimpleTerm.
clone() - Method in class Pandora.LogicParser.Formula.SkTerm
Returns a copy(clone) of this Term.
clone() - Method in class Pandora.LogicParser.Formula.SVar
Returns a copy(clone) of this Term.
clone() - Method in class Pandora.LogicParser.Formula.Term
Returns a copy(clone) of this Term.
clone() - Method in class Pandora.LogicParser.Formula.Var
Returns a copy(clone) of this Var.
clone() - Method in class Pandora.PanSignature
Returns a copy(clone) of this PanSignature.
Colour - Class in Pandora.xGui
Constants for colours
Colour() - Constructor for class Pandora.xGui.Colour
 
COMMA - Static variable in class Pandora.LogicParser.sym
 
comment - Static variable in class Pandora.xGui.Colour
 
commitSaveState() - Method in class Pandora.ProofWindow
Adds the temporarily stored copy of the ProofBox to the undo list and clears all the redo states.
compare(PanSignature) - Method in class Pandora.PanSignature
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.
compare(ProofLine, ProofLine) - Method in class Pandora.PLComparator
 
compareTo(ProofLine) - Method in class Pandora.ProofLine
 
compatible(Formula, Formula) - Method in class Pandora.NDRules.ForallArrowElim
 
concatNoDup(List<Term>) - Method in class Pandora.LogicParser.Formula.Formula
This method removes the duplicates from Formula's Term list.
concatNoDup(List<Term>) - Method in class Pandora.LogicParser.Formula.Term
This method removes the duplicates from the Term list.
contradictory(Formula, Formula) - Static method in class Pandora.NDRules.EM
Checks if the two formulas ar contradictory(One is the Not of the other one)
contradictory(Formula, Formula) - Static method in class Pandora.NDRules.FalsityIntro
Checks if the two formulas ar contradictory(One is the Not of the other one)
contradictory(Formula, Formula) - Static method in class Pandora.NDRules.IffElimDerived
Checks if the two formulas ar contradictory(One is the Not of the other one)
contradictory(Formula, Formula) - Static method in class Pandora.NDRules.IffIntroDerived
Checks if the two formulas ar contradictory(One is the Not of the other one)
contradictory(Formula, Formula) - Static method in class Pandora.NDRules.NotElim
Checks if the two formulas ar contradictory(One is the Not of the other one)
converse(Formula) - Method in class Pandora.NDRules.FalsityIntro
Returns the negated form of the given formula
If the formula is already negated it will remove the Not sign (e.g.
converse(Formula) - Method in class Pandora.NDRules.NotElim
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.
converse(Formula) - Method in class Pandora.NDRules.NotIntro
Returns the negated form of the given formula
If the formula is already negated it will remove the Not sign (e.g.
createNodes(DefaultMutableTreeNode) - Method in class Pandora.Help.Help
Creates the nodes in the tree attached to the Tree Tab.pathURL = Help.class.getResource( "help/welcome.html" );

D

darkGreen - Static variable in class Pandora.xGui.Colour
 
DashedBorder - Class in Pandora.xGui
Part of the extra Gui functions.
DashedBorder() - Constructor for class Pandora.xGui.DashedBorder
Creates a new DashedBorder.
DashedBorder(Color, int, int) - Constructor for class Pandora.xGui.DashedBorder
Creates a new DashedBorder.
defaultButtonBackground - Static variable in class Pandora.xGui.Colour
 
defaultButtonUI - Static variable in class Pandora.xGui.Colour
 
deselectAll() - Method in class Pandora.ProofBox
Used to deselect the items once a rule has been executed or the rule failed to execute.
deselectLine() - Method in class Pandora.ProofLine
Carries out the methods required to show and record that a ProofLine has been deselected.
deselectLineNoClear() - Method in class Pandora.ProofLine
Carries out the methods required to show and record that a ProofLine has been deselected without clearing the last selected item for the ProofWindow.
deselectRule(JButton) - Method in class Pandora.ProofWindow
Clears the button to be deselected
disableButtons() - Method in class Pandora.ProofWindow
Used when a TM rule is invoked which disables all rule buttons
display() - Method in class Pandora.Justification
Returns a String which can be used to display the Justification in the Proofline.
display() - Method in class Pandora.LogicParser.Formula.AExp.Add
Returns a String to display the add expression.
display() - Method in class Pandora.LogicParser.Formula.AExp.AExp
Returns a String to display the AExp.
display() - Method in class Pandora.LogicParser.Formula.AExp.Multiply
Returns a String to display the multiply expression.
display() - Method in class Pandora.LogicParser.Formula.AExp.Subtract
Returns a String to display the subtract expression.
display() - Method in class Pandora.LogicParser.Formula.And
Returns the a String to display the And formula.
display() - Method in class Pandora.LogicParser.Formula.Atom
Returns the a String to display the Atom formula.
display() - Method in class Pandora.LogicParser.Formula.BExp.BExp
Returns a String to display the BExp.
display() - Method in class Pandora.LogicParser.Formula.BExp.EqualTo
Returns a String to display the equals to expression.
display() - Method in class Pandora.LogicParser.Formula.BExp.GreaterThan
Returns a String to display the greater than expression.
display() - Method in class Pandora.LogicParser.Formula.BExp.GTE
Returns a String to display the greater than expression.
display() - Method in class Pandora.LogicParser.Formula.BExp.LessThan
Returns a String to display the less than expression.
display() - Method in class Pandora.LogicParser.Formula.BExp.LTE
Returns a String to display the less than expression.
display() - Method in class Pandora.LogicParser.Formula.BExp.NotEqual
Returns a String to display the not equals expression.
display() - Method in class Pandora.LogicParser.Formula.Equals
Returns the String to display the equality formula.
display() - Method in class Pandora.LogicParser.Formula.Exists
Returns the a String to display the There Exists Formula.
display() - Method in class Pandora.LogicParser.Formula.False
Returns the a String to display the Bottom Formula.
display() - Method in class Pandora.LogicParser.Formula.Forall
Returns the a String to display the For All formula.
display() - Method in class Pandora.LogicParser.Formula.Formula
Returns the a String to display the Formula.
display() - Method in class Pandora.LogicParser.Formula.Function
Returns the String to display the Function term.
display() - Method in class Pandora.LogicParser.Formula.Iff
Returns the a String to display the Implies formula.
display() - Method in class Pandora.LogicParser.Formula.Implies
Returns the a String to display the Implies formula.
display() - Method in class Pandora.LogicParser.Formula.Not
Returns the a String to display the Implies formula.
display() - Method in class Pandora.LogicParser.Formula.Num
Returns a String to display the num term.
display() - Method in class Pandora.LogicParser.Formula.Or
Returns the a String to display the Or formula.
display() - Method in class Pandora.LogicParser.Formula.Predicate
Returns an String representation of the Predicate formula.
display() - Method in class Pandora.LogicParser.Formula.Quantifier
Returns the a String to display the Atom formula.
display() - Method in class Pandora.LogicParser.Formula.SimpleTerm
Returns a String to display the SimpleTerm.
display() - Method in class Pandora.LogicParser.Formula.SkTerm
Returns a String to display the Term.
display() - Method in class Pandora.LogicParser.Formula.SVar
Returns a String to display the const term.
display() - Method in class Pandora.LogicParser.Formula.Term
Returns a String to display the Term.
display() - Method in class Pandora.LogicParser.Formula.True
Returns the a String to display the Implies formula.
display() - Method in class Pandora.LogicParser.Formula.Unknown
Returns a String to display the var term.
display() - Method in class Pandora.LogicParser.Formula.Var
Returns a String to display the Var.
display() - Method in class Pandora.NDRules.Pair
 
display() - Method in class Pandora.PanSignature
 
display() - Method in class Pandora.ProofBox
Returns the ProofBox within a JPanel.
display() - Method in class Pandora.ProofItem
Returns a JPanel containing this ProofItem.
display() - Method in class Pandora.ProofLine
Returns JPanel containing this ProofLine.
displayAllSignature() - Method in class Pandora.ProofWindow
Updatse the contents of all signature display boxes
displayColour() - Method in class Pandora.ProofItem
Sets the display colour of the ProofItem depending on if the item is selected.
displayColour() - Method in class Pandora.ProofLine
Sets the display colour of the ProofLine depending on if the line is selected.
displayFormula() - Method in class Pandora.Help.HelpMessages
 
displayFormula(Formula) - Method in class Pandora.Help.HelpMessages
 
do_action(int, lr_parser, Stack, int) - Method in class Pandora.LogicParser.parser
Invoke a user supplied parse action.

E

editFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Edit Menu.
editKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'editFile'.
em - Static variable in class Pandora.Help.HelpMessages
 
EM - Class in Pandora.NDRules
Implements the Excluded Middle(EM) rule.
Extends abstract class Rule.
EM(ProofBox) - Constructor for class Pandora.NDRules.EM
Constructs an EM.
EM - Static variable in class Pandora.Types
 
EMFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the EM Rule.
EMKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'EMFile'.
Empty - Static variable in class Pandora.Types
 
empty_line - Static variable in class Pandora.Help.ErrorMessages
 
enableButtons() - Method in class Pandora.ProofWindow
Used when a TM rule is completed which enables all rule buttons
EOF - Static variable in class Pandora.LogicParser.sym
 
EOF_sym() - Method in class Pandora.LogicParser.parser
EOF Symbol index.
EqualitySubstitutionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Equality Substitution Rule.
EqualitySubstitutionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'EqualitySubstitutionFile'.
equals(Atom) - Method in class Pandora.LogicParser.Formula.Atom
Returns true if this Atom is equal with the passes Atom
Two Atoms are equal if they have the same name and the same arity
Equals - Class in Pandora.LogicParser.Formula
The Equals formula.
Extends class Predicate.
Equals(Vector<Term>) - Constructor for class Pandora.LogicParser.Formula.Equals
Constructs an Equals formula.
equals(Term) - Method in class Pandora.LogicParser.Formula.Function
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
equals(Predicate) - Method in class Pandora.LogicParser.Formula.Predicate
Returns true if the passed Predicate is equal to this Predicate
Two predicates are equal if they have the same name and the same arity.
equals(Term) - Method in class Pandora.LogicParser.Formula.SimpleTerm
Returns true if the passed Term is equal to this SimpleTerm
A Term is equal to a SimpleTerm if it is a SimpleTerm and they have the same name.
equals(Term) - Method in class Pandora.LogicParser.Formula.SkTerm
Returns true if this Term is equal to the passed Term.
equals(Term) - Method in class Pandora.LogicParser.Formula.SVar
Returns true if the passed Term is equal to this Term.
equals(Term) - Method in class Pandora.LogicParser.Formula.Term
Returns true if the passed Term is equal to this Term.
equals(Term) - Method in class Pandora.LogicParser.Formula.Var
Returns true if the passed Term is equal to this Var
A Term is equal to a Var if it is a Var and they have the same name.
EQUALS - Static variable in class Pandora.LogicParser.sym
 
EqualTo - Class in Pandora.LogicParser.Formula.BExp
Creates an equals to expression.
EqualTo(Term, Term) - Constructor for class Pandora.LogicParser.Formula.BExp.EqualTo
Constructs a new EqualTo BExp.
equivalent(Function) - Method in class Pandora.LogicParser.Formula.Function
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
 
error_sym() - Method in class Pandora.LogicParser.parser
error Symbol index.
ErrorFrame - Class in Pandora.Help
Implements custom error messages.
ErrorFrame() - Constructor for class Pandora.Help.ErrorFrame
 
ErrorMessages - Class in Pandora.Help
Class which keeps all the error messages.
ErrorMessages() - Constructor for class Pandora.Help.ErrorMessages
 
errorRed - Static variable in class Pandora.xGui.Colour
 
Exists - Class in Pandora.LogicParser.Formula
The There Exists quantifier formula.
Extends abstract class Formula.
Exists(Var, Formula) - Constructor for class Pandora.LogicParser.Formula.Exists
Constructs a There Exists Formula.
EXISTS - Static variable in class Pandora.LogicParser.sym
 
ExistsElim - Static variable in class Pandora.Help.ErrorMessages
 
ExistsElim - Class in Pandora.NDRules
Implements the There Exists Elimination rule.
Extends abstract class Rule.
ExistsElim(ProofBox) - Constructor for class Pandora.NDRules.ExistsElim
Constructs an ExistsElim.
ExistsElim - Static variable in class Pandora.Types
 
ExistsEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Exists Elimination Rule.
ExistsEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'ExistsEliminationFile'.
ExistsIntro - Class in Pandora.NDRules
Implements the There Exists Introduction rule.
Extends abstract class Rule.
ExistsIntro(ProofBox) - Constructor for class Pandora.NDRules.ExistsIntro
Constructs an ExistsIntro.
ExistsIntro - Static variable in class Pandora.Types
 
ExistsIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Exists Introduction Rule.
ExistsIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'ExistsIntroductionFile'.
exitRule() - Method in class Pandora.RuleController
Called when rule execution failed or the rule finished execution.

F

False - Class in Pandora.LogicParser.Formula
The Bottom formula.
Extends abstract class Formula.
False() - Constructor for class Pandora.LogicParser.Formula.False
Constructs a Bottom Formula.
falsity - Static variable in class Pandora.Help.ErrorMessages
 
falsity - Static variable in class Pandora.Help.HelpMessages
 
falsity_elimination_forwards - Static variable in class Pandora.Help.HelpMessages
 
falsity_forwards - Static variable in class Pandora.Help.ErrorMessages
 
FalsityElim - Class in Pandora.NDRules
Implements the Falsity Elimination rule.
Extends abstract class Rule.
FalsityElim(ProofBox) - Constructor for class Pandora.NDRules.FalsityElim
Constructs a FalsityElim.
FalsityElim - Static variable in class Pandora.Types
 
FalsityEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Falsity Elimination Rule.
FalsityEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'FalsityEliminationFile'.
FalsityIntro - Class in Pandora.NDRules
Implements the Falsity Introduction rule.
Extends abstract class Rule.
FalsityIntro(ProofBox) - Constructor for class Pandora.NDRules.FalsityIntro
Constructs a FalsityIntro.
FalsityIntro - Static variable in class Pandora.Types
 
FalsityIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Falsity introduction Rule.
FalsityIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'FalsityIntroductionFile'.
fileFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the File Menu.
fileKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'fileFile'.
files - Static variable in class Pandora.Help.HelpPagesHTML
The List of all the available HelpAccessProceduress (help files).
findAll(ProofLine, ProofLine) - Method in class Pandora.NDRules.Substitution
This method is only used when the Substitution rule is applied forwards.
It finds all the possible substitution between two passed lines' formulae.
findMatch(Formula, Equals, ProofLine) - Method in class Pandora.NDRules.Substitution
This is a helper method called by the findAll method,
to check if the passed Term is cotained in the passed Equals Formula's left or right hand side.
findMatch(Term, Equals, ProofLine) - Method in class Pandora.NDRules.Substitution
 
finishedRule() - Method in class Pandora.ProofWindow
Performed when a rule application has been completed.
firstLine - Variable in class Pandora.NDRules.NDRule
 
firstTMLine - Variable in class Pandora.ProofWindow
 
focusGained(FocusEvent) - Method in class Pandora.ProofWindow
Invoked when a component gains the keyboard focus
focusLost(FocusEvent) - Method in class Pandora.ProofWindow
Invoked when a component loses the keyboard focus
Forall - Class in Pandora.LogicParser.Formula
The Forall quantifier formula.
Extends abstract class Formula.
Forall(Var, Formula) - Constructor for class Pandora.LogicParser.Formula.Forall
Constructs a Forall Formula.
FORALL - Static variable in class Pandora.LogicParser.sym
 
forall_elimination_backwards_input - Variable in class Pandora.Help.HelpMessages
 
forall_elimination_backwards_optional - Static variable in class Pandora.Help.HelpMessages
 
forall_elimination_backwards_specify - Variable in class Pandora.Help.HelpMessages
 
forall_elimination_backwards_specify_input - Variable in class Pandora.Help.HelpMessages
 
forall_elimination_forwards - Variable in class Pandora.Help.HelpMessages
 
forall_introduction_forwards - Static variable in class Pandora.Help.HelpMessages
 
ForallArrowElim - Class in Pandora.NDRules
Implements the For All Arrow Elimination rule.
Extends abstract class Rule.
ForallArrowElim(ProofBox) - Constructor for class Pandora.NDRules.ForallArrowElim
Constructs a ForallElim.
ForallArrowElim - Static variable in class Pandora.Types
 
ForallArrowEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Forall Arrow Elimination Rule.
ForallArrowEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'ForallArrowEliminationFile'.
forAllArrowIntro - Static variable in class Pandora.Help.ErrorMessages
 
ForallArrowIntro - Class in Pandora.NDRules
Implements the For All Introduction rule.
Extends abstract class Rule.
ForallArrowIntro(ProofBox) - Constructor for class Pandora.NDRules.ForallArrowIntro
Constructs a ForallIntro.
ForallArrowIntro - Static variable in class Pandora.Types
 
forAllArrowIntro_backwards - Static variable in class Pandora.Help.ErrorMessages
 
ForallArrowIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Forall Arrow Introduction Rule.
ForallArrowIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'ForallArrowIntroductionFile'.
ForallElim - Class in Pandora.NDRules
Implements the For All Elimination rule.
Extends abstract class Rule.
ForallElim(ProofBox) - Constructor for class Pandora.NDRules.ForallElim
Constructs a ForallElim.
ForallElim - Static variable in class Pandora.Types
 
forAllElim_backwards - Static variable in class Pandora.Help.ErrorMessages
 
ForallEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Forall Elimination Rule.
ForallEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'ForallEliminationFile'.
ForallIntro - Class in Pandora.NDRules
Implements the For All Introduction rule.
Extends abstract class Rule.
ForallIntro(ProofBox) - Constructor for class Pandora.NDRules.ForallIntro
Constructs a ForallIntro.
ForallIntro - Static variable in class Pandora.Types
 
forAllIntro_backwards - Static variable in class Pandora.Help.ErrorMessages
 
ForallIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Forall Introduction Rule.
ForallIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'ForallIntroductionFile'.
forAllTick - Static variable in class Pandora.Help.ErrorMessages
 
ForallTick - Class in Pandora.NDRules
Implements the For All Tick rule.
Extends abstract class Rule.
ForallTick(ProofBox) - Constructor for class Pandora.NDRules.ForallTick
Constructs a ForallTick.
ForallTick - Static variable in class Pandora.Types
 
forAllTick_backwards - Static variable in class Pandora.Help.ErrorMessages
 
foralltick_backwards - Static variable in class Pandora.Help.HelpMessages
 
ForallTickFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Forall Tick Rule.
ForallTickKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the ForallTickFile'.
formula - Variable in class Pandora.Help.HelpMessages
 
Formula - Class in Pandora.LogicParser.Formula
Abstract Formula class.
Extended by each of the Formula classes.
Formula() - Constructor for class Pandora.LogicParser.Formula.Formula
 
Function - Class in Pandora.LogicParser.Formula
The Function Term.
Extends abstract class Term.
Function(String, Vector<Term>) - Constructor for class Pandora.LogicParser.Formula.Function
Constructs a Function Term.

G

getAllTerms() - Method in class Pandora.LogicParser.Formula.Quantifier
This method returns a list of all the Terms this formula contain including the variables.
getArity() - Method in class Pandora.LogicParser.Formula.Atom
 
getArity() - Method in class Pandora.LogicParser.Formula.Function
Returns the arity of the Function.
getArity() - Method in class Pandora.LogicParser.Formula.Predicate
Returns the Arity of the Predicate.
getAtoms() - Method in class Pandora.LogicParser.Formula.Formula
Returns the list of atoms contained in a Formula tree.
getBody() - Method in class Pandora.Help.HelpAccessProcedures
Returns the body of the file.
getBody(String) - Static method in class Pandora.Help.HelpPagesHTML
Searches within the list of all the available Help HelpPagesHTML.
getBorderInsets(Component) - Method in class Pandora.xGui.DashedBorder
Returns the insets of the border.
getConstants() - Method in class Pandora.PanSignature
Returns the Constant list of the PanSignature.
getDescription() - Method in class Pandora.xGui.PandoraFileFilter
Returns the String description of a Pandora file.
getDisplayBorder() - Method in class Pandora.ProofBox
Returns true is the box is displayed.
getDisplayItems() - Method in class Pandora.ProofBox
Returns true if box's ProofItems are not hidden, otherwise false.
getExtraLines() - Method in class Pandora.Justification
Returns the extra lines contained in the justification.
getFirst() - Method in class Pandora.LogicParser.Formula.Tuple
Returns the first Term of the Tuple.
getFirst() - Method in class Pandora.NDRules.Pair
 
getFormula(NDRule) - Method in class Pandora.Help.HelpMessages
 
getFormula() - Method in class Pandora.LogicParser.Formula.Exists
Returns the Formula which is bound by the quantifier.
getFormula() - Method in class Pandora.LogicParser.Formula.Forall
Returns the Formula which is bound by the quantifier.
getFormula() - Method in class Pandora.LogicParser.Formula.Not
Returns the formula on which negation is applied.
getFormula() - Method in class Pandora.LogicParser.Formula.Quantifier
Returns the Formula this Quantifier is applied on.
getFormula() - Method in class Pandora.ProofLine
Returns the formula of this ProofLine.
getFunctions() - Method in class Pandora.PanSignature
Returns the Function list of the PanSignature.
getIndex(ProofItem) - Method in class Pandora.ProofBox
Returns the index of a given ProofItem
getJustification() - Method in class Pandora.ProofLine
Returns the justification of this ProofLine.
getKW() - Method in class Pandora.Help.HelpAccessProcedures
Returns the keyword list of the file.
getKWs(String) - Static method in class Pandora.Help.HelpPagesHTML
Searches within the list of all the available Help HelpPagesHTML.
getLastRuleSelected() - Method in class Pandora.ProofWindow
Returns the button which was last selected
getLeft() - Method in class Pandora.LogicParser.Formula.AExp.AExp
Returns the left hand side of the arithmetic expression.
getLeft() - Method in class Pandora.LogicParser.Formula.And
Returns the left side formula.
getLeft() - Method in class Pandora.LogicParser.Formula.Formula
Default getLeft() method for when a Formula has no left Formula.
getLeft() - Method in class Pandora.LogicParser.Formula.Iff
Returns the left side formula.
getLeft() - Method in class Pandora.LogicParser.Formula.Implies
Returns the left side formula.
getLeft() - Method in class Pandora.LogicParser.Formula.Or
Returns the left side formula.
getLeftTerm() - Method in class Pandora.LogicParser.Formula.BExp.BExp
Returns the left hand side of the boolean expression.
getLeftTerm() - Method in class Pandora.LogicParser.Formula.Equals
Returns the left hand side of the equality.
getLine() - Method in class Pandora.NDRules.Pair
 
getLineComment() - Method in class Pandora.ProofLine
Returns the comment of this ProofLine
getLineNum() - Method in class Pandora.ProofLine
Returns to line number of the ProofLine.
getLines() - Method in class Pandora.Justification
Returns the lines contained in the Justification.
getMainSignature() - Method in class Pandora.ProofBox
 
getName() - Method in class Pandora.LogicParser.Formula.AExp.AExp
Returns the name of the expression.
getName() - Method in class Pandora.LogicParser.Formula.Atom
Returns the name of the atom.
getName() - Method in class Pandora.LogicParser.Formula.Function
Returns the name of the Function.
getName() - Method in class Pandora.LogicParser.Formula.Num
Returns the name of the Term.
getName() - Method in class Pandora.LogicParser.Formula.Predicate
Returns the name of the Predicate.
getName() - Method in class Pandora.LogicParser.Formula.SimpleTerm
Returns the name of the SimpleTerm.
getName() - Method in class Pandora.LogicParser.Formula.Sk
Returns the name of the atom.
getName() - Method in class Pandora.LogicParser.Formula.SkTerm
Returns the name of the Term.
getName() - Method in class Pandora.LogicParser.Formula.SVar
Returns the name of the Term.
getName() - Method in class Pandora.LogicParser.Formula.Term
Returns the name of the Term.
getName() - Method in class Pandora.LogicParser.Formula.Var
Returns the name of the Var.
getNewFormula(String, String) - Method in class Pandora.NDRules.ExistsIntro
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.
getNewFormula(String, String) - Method in class Pandora.NDRules.ForallArrowIntro
Takes as input a formula that was rejected because its atoms were not in the signature of the proof.
getNewFormula(String, String) - Method in class Pandora.NDRules.ForallElim
Takes as input a formula that was rejected because its atoms were not in the signature of the proof.
getNewFormula(String, String) - Method in class Pandora.NDRules.ForallIntro
Takes as input a formula that was rejected because its atoms were not in the signature of the proof.
getNewFormula(String, String) - Method in class Pandora.NDRules.IffIntro
Takes as input a formula that was rejected because its atoms were not in the signature of the proof.
getNewFormula(String, String) - Method in class Pandora.NDRules.ImpliesIntro
Takes as input a formula that was rejected because its atoms were not in the signature of the proof.
getNewFormula(String, String) - Method in class Pandora.NDRules.NDRule
Takes as input a formula that was rejected because its atoms were not in the signature of the proof.
getNewFormula(String, String) - Method in class Pandora.NDRules.NotIntro
Takes as input a formula that was rejected because its atoms were not in the signature of the proof.
getNewTerm(String, String, Formula) - Method in class Pandora.NDRules.ExistsIntro
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.
getNewTerm(String, String, Formula) - Method in class Pandora.NDRules.ForallArrowElim
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.
getNewTerm(String, String, Formula) - Method in class Pandora.NDRules.ForallElim
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.
getNewTerm(String, String) - Method in class Pandora.NDRules.Reflexivity
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.
getNextBox() - Method in class Pandora.ProofBox
Returns the next ProofBox in the list.
getOccurrences() - Method in class Pandora.NDRules.Pair
 
getOlderSiblingBox() - Method in class Pandora.ProofBox
Returns the ProofBox that references this ProofBox as its nextBox.
getParams() - Method in class Pandora.LogicParser.Formula.Function
Returns the list of parameters of the Function.
getParams() - Method in class Pandora.LogicParser.Formula.Predicate
Returns the list of parameters of this Predicate.
getParentBox() - Method in class Pandora.ProofItem
Returns the ProofBox that contains the current ProofItem.
getParentWindow() - Method in class Pandora.ProofItem
Returns the ProofWindow that contains this ProofItem.
getPrecedence() - Method in class Pandora.LogicParser.Formula.And
Returns an integer representing the precedence of this formula according to binding conventions
getPrecedence() - Method in class Pandora.LogicParser.Formula.Atom
Returns an integer representing the precedence of this formula according to binding conventions
getPrecedence() - Method in class Pandora.LogicParser.Formula.BExp.BExp
 
getPrecedence() - Method in class Pandora.LogicParser.Formula.Formula
Returns an integer representing the precedence of this formula according to binding conventions
getPrecedence() - Method in class Pandora.LogicParser.Formula.Iff
Returns an integer representing the precedence of this formula according to binding conventions
getPrecedence() - Method in class Pandora.LogicParser.Formula.Implies
Returns an integer representing the precedence of this formula according to binding conventions
getPrecedence() - Method in class Pandora.LogicParser.Formula.Not
Returns an integer representing the precedence of this formula according to binding conventions
getPrecedence() - Method in class Pandora.LogicParser.Formula.Or
Returns an integer representing the precedence of this formula according to binding conventions
getPrecedence() - Method in class Pandora.LogicParser.Formula.Quantifier
Returns an integer representing the precedence of this formula according to binding conventions
getPrecedence() - Method in class Pandora.LogicParser.Formula.Unknown
Returns an integer representing the precedence of this formula according to binding conventions
getPredicates() - Method in class Pandora.PanSignature
Returns the Predicate list of the PanSignature.
getProofBox() - Method in class Pandora.ProofWindow
 
getProofItems() - Method in class Pandora.ProofBox
Returns the list of ProofItems contained in the box.
getRight() - Method in class Pandora.LogicParser.Formula.AExp.AExp
Returns the right hand side of the arithmetic expression.
getRight() - Method in class Pandora.LogicParser.Formula.And
Returns the right side formula.
getRight() - Method in class Pandora.LogicParser.Formula.Formula
Default getRight() method for when a Formula has no right Formula.
getRight() - Method in class Pandora.LogicParser.Formula.Iff
Returns the right side formula.
getRight() - Method in class Pandora.LogicParser.Formula.Implies
Returns the right side formula.
getRight() - Method in class Pandora.LogicParser.Formula.Or
Returns the right side formula.
getRightTerm() - Method in class Pandora.LogicParser.Formula.BExp.BExp
Returns the right hand side of the boolean expression.
getRightTerm() - Method in class Pandora.LogicParser.Formula.Equals
Returns the right hand side of the equality.
getSecond() - Method in class Pandora.LogicParser.Formula.Tuple
Returns the second Term of the Tuple.
getSecond() - Method in class Pandora.NDRules.Pair
 
getSignature() - Method in class Pandora.ProofBox
Returns the signature of the ProofBox.
getSignature() - Method in class Pandora.ProofWindow
 
getSkolems() - Method in class Pandora.PanSignature
Returns the Skolem Constant list of the PanSignature.
getSVars() - Method in class Pandora.PanSignature
Returns the SVariable list of the PanSignature.
getSymbol() - Method in class Pandora.Justification
Returns the String representing the type of the Justification.
getTerm(String, String, Formula) - Method in class Pandora.NDRules.ExistsIntro
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.
getTerm(String, String, Formula) - Method in class Pandora.NDRules.ForallArrowElim
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.
getTerm(String, String, Formula) - Method in class Pandora.NDRules.ForallElim
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.
getTerms() - Method in class Pandora.LogicParser.Formula.Equals
Returns both left and right side of the equality in a list of Terms.
getTerms() - Method in class Pandora.LogicParser.Formula.Formula
This method returns a list of all the Terms this formula contain.
getTerms() - Method in class Pandora.LogicParser.Formula.Function
This method returns a list of all the Terms this Function contain.
getTerms() - Method in class Pandora.LogicParser.Formula.Iff
This method returns a list of all the Terms this Formula contain.
getTerms() - Method in class Pandora.LogicParser.Formula.Implies
This method returns a list of all the Terms this Formula contain.
getTerms() - Method in class Pandora.LogicParser.Formula.Not
This method returns a list of all the Terms this Formula contain.
getTerms() - Method in class Pandora.LogicParser.Formula.Or
This method returns a list of all the Terms this Formula contain.
getTerms() - Method in class Pandora.LogicParser.Formula.Predicate
This method returns a list of all the Terms this formula contain.
getTerms() - Method in class Pandora.LogicParser.Formula.Quantifier
This method returns a list of all the Terms this formula contain excluding the variables.
getTerms() - Method in class Pandora.LogicParser.Formula.Unknown
This method returns a list of all the Terms this formula contains.
i.e.
getTitle() - Method in class Pandora.Help.HelpAccessProcedures
Returns the title of the file.
getTuples() - Method in class Pandora.LogicParser.Formula.Formula
Returns a list of all the bindings that has taken place so far.
I.e.
getVar() - Method in class Pandora.LogicParser.Formula.Exists
Returns the bound variable of the quantifier formula.
getVar() - Method in class Pandora.LogicParser.Formula.Forall
Returns the bound variable of the quantifier formula.
getVar() - Method in class Pandora.LogicParser.Formula.Quantifier
Returns the bound variable of the quantifier formula.
getVar(String, String, Formula) - Method in class Pandora.NDRules.ExistsIntro
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.
getVar(String, String, Formula) - Method in class Pandora.NDRules.ForallArrowElim
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.
getVar(String, String, Formula) - Method in class Pandora.NDRules.ForallElim
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.
getVariables() - Method in class Pandora.PanSignature
Returns the Variable list of the PanSignature.
getVars() - Method in class Pandora.LogicParser.Formula.Formula
This method returns the list of all the variables this Formula is bound to.
getVars() - Method in class Pandora.LogicParser.Formula.Term
Returns the list of all varibles this Term is bound to.
getView() - Method in class Pandora.ParseInputController
Returns the View associated with this Controller
Given - Static variable in class Pandora.Types
 
Goal - Static variable in class Pandora.Types
 
GreaterThan - Class in Pandora.LogicParser.Formula.BExp
Creates a greater than expression.
GreaterThan(Term, Term) - Constructor for class Pandora.LogicParser.Formula.BExp.GreaterThan
Constructs a new GreaterThan BExp.
GTE - Class in Pandora.LogicParser.Formula.BExp
Creates a greater than or equal to expression.
GTE(Term, Term) - Constructor for class Pandora.LogicParser.Formula.BExp.GTE
Constructs a new GreaterThanOrEqual BExp.

H

hasNextBox() - Method in class Pandora.ProofBox
A ProofBox item in a proof may be a list of ProofBoxes.
haveAll() - Method in class Pandora.NDRuleController
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.AndElim
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.AndIntro
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.EM
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.ExistsElim
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.ExistsIntro
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.FalsityElim
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.FalsityIntro
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.ForallArrowElim
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.ForallArrowIntro
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.ForallElim
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.ForallIntro
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.ForallTick
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.IffElim
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.IffElimDerived
Returns true if the rule has all of the required input lines
Only the first line is required so this method returns true.
haveAll() - Method in class Pandora.NDRules.IffIntro
Returns true if the rule has all of the required input lines
Only the first line is required so this method returns true.
haveAll() - Method in class Pandora.NDRules.IffIntroDerived
Returns true if the rule has all of the required input lines
Only the first line is required so this method returns true.
haveAll() - Method in class Pandora.NDRules.ImpliesElim
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.ImpliesIntro
Returns true if the rule has all of the required input lines
Only the first line is required so this method returns true.
haveAll() - Method in class Pandora.NDRules.Instantiate
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.Lemma
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.NDRule
Returns true if the rule ahs all of the required input lines.
haveAll() - Method in class Pandora.NDRules.NotElim
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.NotIntro
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.NotNot
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.OrElim
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.OrIntro
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.PC
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.Reflexivity
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.Substitution
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.Tick
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.TM
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.TMTick
Returns true if the rule has all of the required input lines.
haveAll() - Method in class Pandora.NDRules.TopIntro
Returns true if the rule has all of the required input lines.
Help - Class in Pandora.Help
Implements the Help frame for Pandora IV.
Help() - Constructor for class Pandora.Help.Help
Constructs the Help Frame for Pandora IV.
HelpAccessProcedures - Class in Pandora.Help
Implements a data structure for storing the Pandora IV Help Files.
HelpAccessProcedures(String, String, LinkedList<String>) - Constructor for class Pandora.Help.HelpAccessProcedures
Creates an instance of the HelpAccessProcedures.
helpFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Help Menu.
HelpFrame - Class in Pandora.Help
Implements the Help messages.
HelpFrame() - Constructor for class Pandora.Help.HelpFrame
 
helpKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'helpFile'.
HelpMessages - Class in Pandora.Help
Class which keeps all the help messages.
HelpMessages(NDRule) - Constructor for class Pandora.Help.HelpMessages
 
HelpMessages(Formula) - Constructor for class Pandora.Help.HelpMessages
 
HelpPagesHTML - Class in Pandora.Help
Creates a database of all the help files (HelpAccessProceduress) used in Pandora IV Help System.
HelpPagesHTML() - Constructor for class Pandora.Help.HelpPagesHTML
Constructs an instance of the HelpPagesHTML.
higher(Formula) - Method in class Pandora.LogicParser.Formula.Formula
 

I

IDENT - Static variable in class Pandora.LogicParser.sym
 
iff - Static variable in class Pandora.Help.ErrorMessages
 
iff - Static variable in class Pandora.Help.HelpMessages
 
Iff - Class in Pandora.LogicParser.Formula
The IFF formula.
Extends abstract class Formula.
Iff(Formula, Formula) - Constructor for class Pandora.LogicParser.Formula.Iff
Constructs an Iff Formula.
IFF - Static variable in class Pandora.LogicParser.sym
 
iff_backwards - Static variable in class Pandora.Help.ErrorMessages
 
iff_introduction - Static variable in class Pandora.Help.HelpMessages
 
IffElim - Class in Pandora.NDRules
Implements the Iff Elimination rule.
Extends abstract class Rule.
IffElim(ProofBox) - Constructor for class Pandora.NDRules.IffElim
Constructs an IffElim.
IffElim - Static variable in class Pandora.Types
 
IffElimDerived - Class in Pandora.NDRules
Implements the Iff Elimination Derived rule.
Extends abstract class Rule.
IffElimDerived(ProofBox) - Constructor for class Pandora.NDRules.IffElimDerived
Constructs an IffElimDerived.
IffEliminationDerivedFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Iff Elimination Derived Rule.
IffEliminationDerivedKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'IffEliminationDerivedFile'.
IffEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Iff Elimination Rule.
IffEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'IffEliminationFile'.
IffIntro - Class in Pandora.NDRules
Implements the Iff Introduction rule.
Extends abstract class Rule.
IffIntro(ProofBox) - Constructor for class Pandora.NDRules.IffIntro
Constructs an IffIntro.
IffIntro - Static variable in class Pandora.Types
 
IffIntroDerived - Class in Pandora.NDRules
Implements the Iff Introduction Derived rule.
Extends abstract class Rule.
IffIntroDerived(ProofBox) - Constructor for class Pandora.NDRules.IffIntroDerived
Constructs an IffIntroDerived.
IffIntroductionDerivedFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Iff Introduction Derived Rule.
IffIntroductionDerivedKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'IffIntroductionDerivedFile'.
IffIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Iff Introduction Rule.
IffIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'IffIntroductionFile'.
Implies - Class in Pandora.LogicParser.Formula
The Implies formula.
Extends abstract class Formula.
Implies(Formula, Formula) - Constructor for class Pandora.LogicParser.Formula.Implies
Constructs an Implies Formula.
IMPLIES - Static variable in class Pandora.LogicParser.sym
 
implies_introduction_forwards - Static variable in class Pandora.Help.HelpMessages
 
ImpliesElim - Class in Pandora.NDRules
Implements the Implies Elimination rule.
Extends abstract class Rule.
ImpliesElim(ProofBox) - Constructor for class Pandora.NDRules.ImpliesElim
Constructs an ImpliesElim.
ImpliesElim - Static variable in class Pandora.Types
 
ImpliesIntro - Class in Pandora.NDRules
Implements the Implies Introduction rule.
Extends abstract class Rule.
ImpliesIntro(ProofBox) - Constructor for class Pandora.NDRules.ImpliesIntro
Constructs an ImpliesIntro.
ImpliesIntro - Static variable in class Pandora.Types
 
incrementOccurrences() - Method in class Pandora.NDRules.Pair
 
init_actions() - Method in class Pandora.LogicParser.parser
Action encapsulation object initializer.
initialise() - Method in class Pandora.NDRuleController
Called by RuleController to add the first line to the rule.
inProof - Variable in class Pandora.ProofWindow
 
InputGuideBody - Static variable in class Pandora.Help.HelpPagesHTML
 
inputProofMode() - Method in class Pandora.ProofWindow
Mode for inputting data into the proof.
Instantiate - Class in Pandora.NDRules
Implements the instantiate rule.
Instantiate(ProofBox) - Constructor for class Pandora.NDRules.Instantiate
Constructs an Instantiate rule instance.
Instantiate - Static variable in class Pandora.Types
 
intersection(List<Term>, List<Term>, List<Var>) - Method in class Pandora.NDRules.ForallArrowElim
 
isBorderOpaque() - Method in class Pandora.xGui.DashedBorder
The border is never opaque so this function returns false.
isBracketed(String) - Method in class Pandora.LogicParser.Formula.Formula
 
isDone() - Method in class Pandora.ProofWindow
 
isEmpty() - Method in class Pandora.PanSignature
Returns true if the PanSignature is empty.
A PanSignature is empty if its Predicate,Constant and the Function lists are empty.
isIn(PanSignature) - Method in class Pandora.LogicParser.Formula.AExp.AExp
Returns true if this Term is in the passed PanSignature.
isIn(PanSignature) - Method in class Pandora.LogicParser.Formula.Atom
Returns true if this Atom is in the passed PanSignature's Predicate list.
isIn(PanSignature) - Method in class Pandora.LogicParser.Formula.Function
Returns true if this Function is in the Function list of the passed PanSignature
isIn(PanSignature) - Method in class Pandora.LogicParser.Formula.Num
Returns true if this Term is in the passed PanSignature
I.e.
isIn(PanSignature) - Method in class Pandora.LogicParser.Formula.SimpleTerm
Returns true if this SimpleTerm is in the Constant list of the passed PanSignature
isIn(PanSignature) - Method in class Pandora.LogicParser.Formula.SkTerm
Returns true if this Term is in the passed PanSignature
isIn(PanSignature) - Method in class Pandora.LogicParser.Formula.SVar
Returns true if this Term is in the passed PanSignature
I.e.
isIn(PanSignature) - Method in class Pandora.LogicParser.Formula.Term
Returns true if this Term is in the passed PanSignature
isIn(List<Term>) - Method in class Pandora.LogicParser.Formula.Term
Returns true if this term is in the passed List.
isIn(PanSignature) - Method in class Pandora.LogicParser.Formula.Var
Returns true if this Var is in the Variable list of the passed PanSignature
isIn(List<Pair>) - Method in class Pandora.NDRules.Pair
 
isInList(List<SimpleTerm>) - Method in class Pandora.LogicParser.Formula.SkTerm
returns true if this Term is in the passed list of Simple Terms.
isInVars(List<Var>) - Method in class Pandora.LogicParser.Formula.Term
Returns true if this Term is in the passed List.
isProved() - Method in class Pandora.ProofBox
 

J

Justification - Class in Pandora
Implements the Justification for a line in a proof.
Justification(String) - Constructor for class Pandora.Justification
Constructs a Justification.
Justification(String, List<ProofLine>) - Constructor for class Pandora.Justification
Constructs a Justification.

K

keyPressed(KeyEvent) - Method in class Pandora.ProofWindow
Handle the key pressed event
keyReleased(KeyEvent) - Method in class Pandora.ProofWindow
Handle the key released event
keyTyped(KeyEvent) - Method in class Pandora.ProofWindow
Handle the key typed event

L

launch(String) - Static method in class Pandora.Help.ErrorFrame
 
launch(String, String) - Static method in class Pandora.Help.ErrorFrame
 
launch(String) - Static method in class Pandora.Help.HelpFrame
 
left - Variable in class Pandora.LogicParser.Formula.AExp.AExp
 
left - Variable in class Pandora.LogicParser.Formula.BExp.BExp
 
Lemma - Class in Pandora.NDRules
Implements the Lemma rule.
Extends abstract class Rule.
Lemma(ProofBox) - Constructor for class Pandora.NDRules.Lemma
Constructs a Lemma.
LEMMA - Static variable in class Pandora.Types
 
lemma_forwards_backwards - Static variable in class Pandora.Help.HelpMessages
 
LemmaFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Lemma Rule.
LemmaKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'LemmaFile'.
LessThan - Class in Pandora.LogicParser.Formula.BExp
Creates a less than expression.
LessThan(Term, Term) - Constructor for class Pandora.LogicParser.Formula.BExp.LessThan
Constructs a new GreaterThan BExp.
lightBlue - Static variable in class Pandora.xGui.Colour
 
lightGreen - Static variable in class Pandora.xGui.Colour
 
lightPurple - Static variable in class Pandora.xGui.Colour
 
lineGreen - Static variable in class Pandora.xGui.Colour
 
lineSelected(ProofLine) - Method in class Pandora.RuleController
Gives the newly selected lines to the Rule as the extra input.
LPAREN - Static variable in class Pandora.LogicParser.sym
 
LSQB - Static variable in class Pandora.LogicParser.sym
 
LTE - Class in Pandora.LogicParser.Formula.BExp
Creates a less than or equal to expression.
LTE(Term, Term) - Constructor for class Pandora.LogicParser.Formula.BExp.LTE
Constructs a new GreaterThanOrEqual BExp.

M

main(String[]) - Static method in class Pandora.Help.Help
 
main(String[]) - Static method in class Pandora.LogicParser.parser
 
main(String[]) - Static method in class Pandora.Pandora
Can be used to starts Pandora from the command line.
mainProofBox - Variable in class Pandora.ProofWindow
 
makeTree() - Method in class Pandora.Help.Help
Creates the tree in the first tab (Tree Tab).
map(Term, List<Tuple>) - Method in class Pandora.LogicParser.Formula.Formula
Checks if the passed Term is equal to the first element of any of the Tuples in the passed List.
mouseClicked(MouseEvent) - Method in class Pandora.ProofBox
Responds to a ProofBox with a mouse listener being clicked.
mouseClicked(MouseEvent) - Method in class Pandora.ProofItem
Responds to a ProofItem with a mouse listener being clicked.
mouseClicked(MouseEvent) - Method in class Pandora.ProofLine
Responds to a ProofItem with a mouse listener being clicked.
mouseClicked(MouseEvent) - Method in class Pandora.View
Responds to a ProofItem with a mouse listener being clicked.
mouseEntered(MouseEvent) - Method in class Pandora.ProofItem
Responds to an object with a mouse listener when a mouse over occurs.
mouseEntered(MouseEvent) - Method in class Pandora.View
Responds to an object with a mouse listener when a mouse over occurs.
mouseExited(MouseEvent) - Method in class Pandora.ProofItem
Responds to an object with a mouse listener when a mouse over occurs.
mouseExited(MouseEvent) - Method in class Pandora.View
Responds to an object with a mouse listener when a mouse over occurs.
mousePressed(MouseEvent) - Method in class Pandora.ProofItem
Responds to an object with a mouse listener being clicked.
mousePressed(MouseEvent) - Method in class Pandora.View
Responds to an object with a mouse listener being clicked.
mouseReleased(MouseEvent) - Method in class Pandora.ProofItem
Responds to an object with a mouse listener being clicked.
mouseReleased(MouseEvent) - Method in class Pandora.View
Responds to an object with a mouse listener being clicked.
Multiply - Class in Pandora.LogicParser.Formula.AExp
Creates a multiplication expression.
Multiply(Term, Term) - Constructor for class Pandora.LogicParser.Formula.AExp.Multiply
Constructs a new Multiply AExp.

N

NDRule - Class in Pandora.NDRules
Abstract Rule class.
Extended by each of the rule classes.
NDRule(ProofBox) - Constructor for class Pandora.NDRules.NDRule
 
NDRuleController - Class in Pandora
Implements the correct NDRule when a first line and a rule have been selected.
NDRuleController(String, ProofLine, ProofBox) - Constructor for class Pandora.NDRuleController
Constructs a NDRuleController.
next(ProofItem) - Method in class Pandora.ProofBox
Returns the next ProofItem in the ProofItems list
not - Static variable in class Pandora.Help.ErrorMessages
 
not - Static variable in class Pandora.Help.HelpMessages
 
Not - Class in Pandora.LogicParser.Formula
The Not formula.
Extends abstract class Formula.
Not(Formula) - Constructor for class Pandora.LogicParser.Formula.Not
Constructs a Not Formula.
NOT - Static variable in class Pandora.LogicParser.sym
 
not_bottom - Static variable in class Pandora.Help.ErrorMessages
 
not_in_scope - Static variable in class Pandora.Help.ErrorMessages
 
not_introduction - Static variable in class Pandora.Help.HelpMessages
 
NotElim - Class in Pandora.NDRules
Implements the Not Elmination rule.
Extends abstract class Rule.
NotElim(ProofBox) - Constructor for class Pandora.NDRules.NotElim
Constructs a NotElim.
NotElim - Static variable in class Pandora.Types
 
notElim_backwards - Static variable in class Pandora.Help.ErrorMessages
 
notElim_backwards - Static variable in class Pandora.Help.HelpMessages
 
NotEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Not Elimination Rule.
NotEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'NotEliminationFile'.
NotEqual - Class in Pandora.LogicParser.Formula.BExp
Creates a not equal to expression.
NotEqual(Term, Term) - Constructor for class Pandora.LogicParser.Formula.BExp.NotEqual
Constructs a new NotEqual BExp.
NOTEQUALS - Static variable in class Pandora.LogicParser.sym
 
NotIntro - Class in Pandora.NDRules
Implements the Not Introduction rule.
Extends abstract class Rule.
NotIntro(ProofBox) - Constructor for class Pandora.NDRules.NotIntro
Constructs a NotIntro.
NotIntro - Static variable in class Pandora.Types
 
NotIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Not Introduction Rule.
NotIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'NotIntroductionFile'.
notnot - Static variable in class Pandora.Help.ErrorMessages
 
notnot - Static variable in class Pandora.Help.HelpMessages
 
NOTNOT - Static variable in class Pandora.LogicParser.sym
 
NotNot - Class in Pandora.NDRules
Implements the NotNot rule.
Extends abstract class NDRule.
NotNot(ProofBox) - Constructor for class Pandora.NDRules.NotNot
Constructs a NotNot.
NotNot - Static variable in class Pandora.Types
 
NotNotFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the NotNot Rule.
NotNotKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'NotNotFile'.
Num - Class in Pandora.LogicParser.Formula
Creates a number term.
Num(int) - Constructor for class Pandora.LogicParser.Formula.Num
Constructs a new Num Term.

O

openProof(String) - Method in class Pandora.ProofWindow
Deserializes the given/goal or proofBox from given file location.

Please see the comment for saveProof, it may be a better idea to store the files in an XML format.
optionsFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Options Menu.
optionsKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'optionsFile'.
or - Static variable in class Pandora.Help.ErrorMessages
 
or - Static variable in class Pandora.Help.HelpMessages
 
Or - Class in Pandora.LogicParser.Formula
The Or formula.
Extends abstract Formula class.
Or(Formula, Formula) - Constructor for class Pandora.LogicParser.Formula.Or
Constructs an Or Formula.
OR - Static variable in class Pandora.LogicParser.sym
 
or_elimination_forwards - Variable in class Pandora.Help.HelpMessages
 
or_introduction_backwards - Static variable in class Pandora.Help.HelpMessages
 
or_introduction_forwards - Static variable in class Pandora.Help.HelpMessages
 
or_introduction_forwards_input_left - Variable in class Pandora.Help.HelpMessages
 
or_introduction_forwards_input_right - Variable in class Pandora.Help.HelpMessages
 
or_selected - Static variable in class Pandora.Help.ErrorMessages
 
OrElim - Class in Pandora.NDRules
Implements the Or Elmination rule.
Extends abstract class NDRule.
OrElim(ProofBox) - Constructor for class Pandora.NDRules.OrElim
Constructs an OrElim.
OrElim - Static variable in class Pandora.Types
 
OrEliminationFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Or Elimination Rule.
OrEliminationKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'OrEliminationFile'.
OrIntro - Class in Pandora.NDRules
Implements the Or Introduction rule.
Extends abstract class NDRule.
OrIntro(ProofBox) - Constructor for class Pandora.NDRules.OrIntro
Constructs an OrIntro.
OrIntro - Static variable in class Pandora.Types
 
OrIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Or Introduction Rule.
OrIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'OrIntroductionFile'.

P

paintBorder(Component, Graphics, int, int, int, int) - Method in class Pandora.xGui.DashedBorder
Paints the border for the specified component with the specified position and size.
Pair - Class in Pandora.NDRules
 
Pair(Term, Term, ProofLine, int) - Constructor for class Pandora.NDRules.Pair
 
pandaExtension - Static variable in class Pandora.xGui.PandoraFileFilter
 
Pandora - package Pandora
 
Pandora - Class in Pandora
This is called to start Pandora.
Pandora() - Constructor for class Pandora.Pandora
 
Pandora.Help - package Pandora.Help
 
Pandora.LogicParser - package Pandora.LogicParser
 
Pandora.LogicParser.Formula - package Pandora.LogicParser.Formula
 
Pandora.LogicParser.Formula.AExp - package Pandora.LogicParser.Formula.AExp
 
Pandora.LogicParser.Formula.BExp - package Pandora.LogicParser.Formula.BExp
 
Pandora.NDRules - package Pandora.NDRules
 
Pandora.xGui - package Pandora.xGui
 
PandoraFileFilter - Class in Pandora.xGui
Part of the extra Gui functions.
PandoraFileFilter() - Constructor for class Pandora.xGui.PandoraFileFilter
 
PanSignature - Class in Pandora
The Pandora Signature.
PanSignature(List<Atom>, List<SimpleTerm>, List<Function>, List<Var>, List<SimpleTerm>) - Constructor for class Pandora.PanSignature
Constructs a PanSignature with the passed list of parameters
PanSignature() - Constructor for class Pandora.PanSignature
Constructs an empty PanSignature.
paramsEqual(Function) - Method in class Pandora.LogicParser.Formula.Function
Returns true if the passed Function has the same parameters as this Function.
ParseController - Class in Pandora.LogicParser
Controls the communication between the GUI and the parser, for a single line of input to be parsed.
ParseController(String) - Constructor for class Pandora.LogicParser.ParseController
Constructs a ParseController.
parseGoal(String, ProofWindow) - Method in class Pandora.ParseInputController
Parses the goal which has been input and starts proof.
parseInput(String, ProofWindow) - Method in class Pandora.ParseInputController
Parses the givens which have been input and starts proof.
ParseInputController - Class in Pandora
Passes data between the View and Parser
ParseInputController() - Constructor for class Pandora.ParseInputController
Constructs a Controller
parseLine() - Method in class Pandora.LogicParser.ParseController
Carries out the parsing of the line of input and returns the formula generated.
parser - Class in Pandora.LogicParser
CUP v0.11a beta 20060608 generated parser.
parser() - Constructor for class Pandora.LogicParser.parser
Default constructor.
parser(Scanner) - Constructor for class Pandora.LogicParser.parser
Constructor which sets the default scanner.
parser(Scanner, SymbolFactory) - Constructor for class Pandora.LogicParser.parser
Constructor which sets the default scanner.
pc - Static variable in class Pandora.Help.HelpMessages
 
PC - Class in Pandora.NDRules
Implements the Proof By Contradiction rule.
Extends abstract class NDRule.
PC(ProofBox) - Constructor for class Pandora.NDRules.PC
Constructs a PC.
PC - Static variable in class Pandora.Types
 
PCFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the PC Rule.
PCKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'PCFile'.
PLComparator - Class in Pandora
 
PLComparator() - Constructor for class Pandora.PLComparator
 
Predicate - Class in Pandora.LogicParser.Formula
The Predicate formula.
Extends abstract class Atom.
Predicate(String, Vector<Term>) - Constructor for class Pandora.LogicParser.Formula.Predicate
Constructs a Predicate Formula.
production_table() - Method in class Pandora.LogicParser.parser
Access to production table.
ProofBox - Class in Pandora
Implements a box in a proof.
ProofBox(ProofWindow) - Constructor for class Pandora.ProofBox
Constructs a ProofBox (Outer).
ProofBox(ProofWindow, ProofBox) - Constructor for class Pandora.ProofBox
Constructs a ProofBox.
ProofBox(ProofLine, ProofWindow, ProofBox) - Constructor for class Pandora.ProofBox
Constructs a ProofBox (with Goal).
ProofItem - Class in Pandora
Extended by ProofBox and ProofLine.
ProofItem(ProofWindow) - Constructor for class Pandora.ProofItem
Constructs a ProofItem.
ProofItem(ProofWindow, ProofBox) - Constructor for class Pandora.ProofItem
Constructs a ProofItem.
ProofLine - Class in Pandora
Is a line contained inside a ProofBox.
Extends ProofItem
ProofLine(Formula, ProofWindow, ProofBox) - Constructor for class Pandora.ProofLine
Constructs a ProofLine with a formula.
ProofLine(Formula, String, ProofWindow, ProofBox) - Constructor for class Pandora.ProofLine
Constructs a ProofLine with a Formula and a String which will become the Justification.
ProofLine(Formula, Justification, ProofWindow, ProofBox) - Constructor for class Pandora.ProofLine
Constructs a ProofLine with a Formula and a Justification.
ProofLine(Formula, Justification, int, ProofWindow, ProofBox) - Constructor for class Pandora.ProofLine
Constructs a ProofLine with a Formula, Justification and Line number.
ProofWindow - Class in Pandora
Everything contained within each tab is a ProofWindow.
ProofWindow(View) - Constructor for class Pandora.ProofWindow
Creates a new ProofWindow.

Q

Quantifier - Class in Pandora.LogicParser.Formula
The Forall quantifier formula.
Extends abstract class Formula, Extended by Forall and Exists Formulae.
Quantifier() - Constructor for class Pandora.LogicParser.Formula.Quantifier
 

R

recalculateLineNum(int) - Method in class Pandora.ProofBox
Recalculates the line numbers within the ProofBox.
recalculateLineNum(int) - Method in class Pandora.ProofItem
Returns the line number for next ProofItem.
recalculateLineNum(int) - Method in class Pandora.ProofLine
Returns the line number for next ProofItem.
redo() - Method in class Pandora.ProofWindow
Redoes rules which have been undone
redoList - Variable in class Pandora.ProofWindow
 
reduce_table() - Method in class Pandora.LogicParser.parser
Access to reduce_goto table.
Reflexivity - Class in Pandora.NDRules
Implements the Reflexivity rule.
Extends abstract class NDRule.
Reflexivity(ProofBox) - Constructor for class Pandora.NDRules.Reflexivity
Constructs a Reflexivity.
Reflexivity - Static variable in class Pandora.Types
 
reflexivity_forwards - Static variable in class Pandora.Help.HelpMessages
 
reflexivity_forwards_no_constants - Static variable in class Pandora.Help.HelpMessages
 
ReflexivityFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Reflexivity Rule.
ReflexivityKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'ReflexivityFile'.
regenerate() - Method in class Pandora.LogicParser.Formula.And
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Atom
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.BExp.EqualTo
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.BExp.GreaterThan
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.BExp.GTE
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.BExp.LessThan
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.BExp.LTE
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.BExp.NotEqual
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Equals
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Exists
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.False
 
regenerate() - Method in class Pandora.LogicParser.Formula.Forall
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Formula
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Iff
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Implies
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Not
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Or
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Predicate
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.True
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate() - Method in class Pandora.LogicParser.Formula.Unknown
Returns a copy of the Formula which can be saved as part of the copy made for the undo function.
regenerate(ProofBox, ProofWindow) - Method in class Pandora.ProofBox
Copies (this) ProofBox to the given outsideBox.
reloadProofBox() - Method in class Pandora.ProofWindow
Refreshes the outermost main proof box in the ProofWindow
removeAllGiven() - Method in class Pandora.ProofWindow
Removes all the input for givens in the enterProofMode
removeAllGoal() - Method in class Pandora.ProofWindow
Removes all the input for goal in the enterProofMode
removeItem(int) - Method in class Pandora.ProofBox
Removes the specified item from the list of ProofItems
removeProofWindow() - Method in class Pandora.View
Removes current proof window tab.
resetFontSize() - Method in class Pandora.View
Resets all of the font sizes in View
right - Variable in class Pandora.LogicParser.Formula.AExp.AExp
 
right - Variable in class Pandora.LogicParser.Formula.BExp.BExp
 
RPAREN - Static variable in class Pandora.LogicParser.sym
 
RSQB - Static variable in class Pandora.LogicParser.sym
 
rule - Variable in class Pandora.Help.HelpMessages
 
RuleController - Class in Pandora
Calls the NDRuleController when a first line and a rule have been selected.
RuleController() - Constructor for class Pandora.RuleController
Constructs a RuleController.
ruleCtrl - Variable in class Pandora.ProofWindow
 

S

s() - Method in class Pandora.LogicParser.Formula.And
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.Atom
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.BExp.EqualTo
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.BExp.GreaterThan
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.BExp.GTE
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.BExp.LessThan
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.BExp.LTE
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.BExp.NotEqual
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.Exists
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.Forall
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.Formula
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.Iff
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.Implies
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.Not
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.Or
Creates SVar to replace PVar in the formula where necessary.
s() - Method in class Pandora.LogicParser.Formula.Unknown
Creates SVar to replace PVar in the formula where necessary.
saveProof(String) - Method in class Pandora.ProofWindow
Serializes the given/goal or proofBox to given file location.

I would prefer to encode this into XML.
search(String, DefaultMutableTreeNode, DefaultListModel) - Method in class Pandora.Help.Help
Searches the help files (HelpAccessProceduress) for the required text phrase.
seeThrough - Static variable in class Pandora.xGui.Colour
 
selectedButton - Static variable in class Pandora.xGui.Colour
 
selectLine() - Method in class Pandora.ProofLine
Carries out the methods required to show and record that a ProofLine has been selected.
selectRule(JButton) - Method in class Pandora.ProofWindow
Sets the button which was last selected.
serialVersionUID - Static variable in class Pandora.ProofWindow
 
serialVersionUID - Static variable in class Pandora.View
 
setAtoms() - Method in class Pandora.LogicParser.Formula.And
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.Atom
Adds this atom to the list of atoms for the formula.
setAtoms() - Method in class Pandora.LogicParser.Formula.BExp.BExp
Adds the list of Atoms in a given tree to the list of Atoms.
setAtoms() - Method in class Pandora.LogicParser.Formula.Equals
Adds this atom to the list of atoms for the formula.
setAtoms() - Method in class Pandora.LogicParser.Formula.Exists
Adds this atom to the list of atoms for the formula.
The list of atoms is found in Formula class.
setAtoms() - Method in class Pandora.LogicParser.Formula.Forall
Adds this formula's Atoms to the list of Atoms.
The list of Atoms is found in Formula class.
setAtoms() - Method in class Pandora.LogicParser.Formula.Formula
Adds the list of Atoms in a given tree to the list of Atoms.
setAtoms() - Method in class Pandora.LogicParser.Formula.Iff
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.Implies
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.
setAtoms() - Method in class Pandora.LogicParser.Formula.Unknown
Obtains the atoms in the formula and adds them to the list of atoms for the tree which contains this formula.
setBoxStarted(boolean) - Method in class Pandora.ProofBox
Sets if the box has been started or not
setDashedBox(boolean) - Method in class Pandora.ProofBox
Controls the appearance of the ProofBox.
setDisplayBorder(boolean) - Method in class Pandora.ProofBox
Used to set the display options of the ProofBox.
setDisplayItems(boolean) - Method in class Pandora.ProofBox
Controls if the content of the ProofBox should be displayed.
setExtraLines(List<ProofLine>) - Method in class Pandora.Justification
Sets the extra lines of the justification.
setFormula(Formula) - Method in class Pandora.ProofLine
Sets the formula
setJustification(Justification) - Method in class Pandora.ProofLine
Sets a new justification of the ProofLine.
setLastSelectedLine(ProofLine) - Method in class Pandora.ProofWindow
Changes the new selected ProofItem and deselects previous ones
setLeft(Formula) - Method in class Pandora.LogicParser.Formula.Formula
Default setLeft() method for when a Formula has no left Formula.
setLine(ProofLine) - Method in class Pandora.NDRules.Pair
 
setLineComment(String) - Method in class Pandora.ProofLine
Sets the comment of this ProofLine
setLineNum(int) - Method in class Pandora.ProofLine
Sets the line number of this ProofLine.
setLines(List<ProofLine>) - Method in class Pandora.Justification
Sets the lines of the justification
setNextBox() - Method in class Pandora.ProofBox
Creates a new ProofBox to follow the current ProofBox and returns this new sibling ProofBox.
setOlderSiblingBox(ProofBox) - Method in class Pandora.ProofBox
Sets the olderSiblingBox of this ProofBox as the ProofBox that refernces this ProofBox as its nextBox.
setParams(Vector<Term>) - Method in class Pandora.LogicParser.Formula.Predicate
Sets the parameter list of this Predicate to the passed list
setParentBox(ProofBox) - Method in class Pandora.ProofItem
Sets the ProofBox that contains this ProofItem.
setRight(Formula) - Method in class Pandora.LogicParser.Formula.Formula
Default setRight() method for when a Formula has no right Formula.
setSecond(Term) - Method in class Pandora.NDRules.Pair
 
setSignature(PanSignature) - Method in class Pandora.PanSignature
Sets this PanSignature to the passed PanSignature by copying its lists' contents.
setTuples(List<Tuple>) - Method in class Pandora.LogicParser.Formula.Formula
Replaces the binidng list of this formula with the passed binding list.
setupMainProofBox() - Method in class Pandora.ProofWindow
 
setVar(Var) - Method in class Pandora.LogicParser.Formula.Exists
 
setVars(Var) - Method in class Pandora.LogicParser.Formula.AExp.AExp
This method adds Var v to the list of variables this Term is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.And
This method adds Var v to the list of variables this formula is bound to
setVars(Var) - Method in class Pandora.LogicParser.Formula.Atom
This method adds Var v to the list of variables this Atom is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.BExp.BExp
This method adds Var v to the list of variables this Formula is bound to
setVars(Var) - Method in class Pandora.LogicParser.Formula.Exists
This method adds Var v to the list of variables this Formula is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Forall
This method adds Var v to the list of variables this Formula is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Formula
This method adds Var v to the list of variables this Formula is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Function
This method adds Var v to the list of variables this Function is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Iff
This method adds Var v to the list of variables this formula is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Implies
This method adds Var v to the list of variables this formula is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Not
This method adds Var v to the list of variables this formula is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Num
This method adds Var v to the list of variables this Term is bound to
setVars(Var) - Method in class Pandora.LogicParser.Formula.Or
This method adds Var v to the list of variables this formula is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Predicate
This method adds Var v to the list of variables this Predicate is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.SimpleTerm
This method adds Var v to the list of variables this SimpleTerm is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.SkTerm
This method adds Var v to the list of variables this Term is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.SVar
This method adds Var v to the list of variables this Term is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Term
This method adds Var v to the list of variables this Term is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Unknown
This method adds Var v to the list of variables this Formula is bound to.
setVars(Var) - Method in class Pandora.LogicParser.Formula.Var
This method adds Var v to the list of variables this Variable is bound to
This will help the parser to prevent having nested variables
I.e.
show() - Method in class Pandora.Help.TextFileReader
 
show(List<Term>) - Method in class Pandora.NDRules.ForallArrowElim
 
show(List<Term>) - Method in class Pandora.NDRules.ForallElim
 
show() - Method in class Pandora.PanSignature
Returns a String representation of the PanSignature.
show2(List<Var>) - Method in class Pandora.NDRules.ForallArrowElim
 
showBrackets - Static variable in class Pandora.View
 
showGlobalSignature() - Method in class Pandora.ProofWindow
Displays the global signature
showLocalSignature(PanSignature) - Method in class Pandora.ProofWindow
 
showMatch() - Method in class Pandora.NDRules.Substitution
 
showSignature() - Method in class Pandora.ProofWindow
Shows the signature in sidebar
showTuples() - Method in class Pandora.LogicParser.Formula.Formula
 
SimpleTerm - Class in Pandora.LogicParser.Formula
The SimpleTerm (a Constant)
Extends abstract class Term.
SimpleTerm(String) - Constructor for class Pandora.LogicParser.Formula.SimpleTerm
Constructs a SimpleTerm(A constant)
Sk - Class in Pandora.LogicParser.Formula
The Atom formula.
Sk(String) - Constructor for class Pandora.LogicParser.Formula.Sk
Constructs an Atom Formula.
SK - Static variable in class Pandora.LogicParser.sym
 
skolem - Variable in class Pandora.ProofBox
 
Skolem - Static variable in class Pandora.Types
 
Skolem2 - Static variable in class Pandora.Types
 
SkTerm - Class in Pandora.LogicParser.Formula
The SkTerm term.
SkTerm(String) - Constructor for class Pandora.LogicParser.Formula.SkTerm
Constructs an SkTerm.
solveProofMode() - Method in class Pandora.ProofWindow
Mode for solving proof by applying rules.
start_production() - Method in class Pandora.LogicParser.parser
Indicates start production.
start_state() - Method in class Pandora.LogicParser.parser
Indicates start state.
stateChanged(ChangeEvent) - Method in class Pandora.Help.Help
Invoked by the action listener attached to the Tabbed Panel.
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.AExp.Add
Substitutes all the occurences of Term a by Term b.
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.AExp.Multiply
Substitutes all the occurences of Term a by Term b.
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.AExp.Subtract
Substitutes all the occurences of Term a by Term b.
sub(Term, Term, Formula) - Method in class Pandora.LogicParser.Formula.Formula
Returns the Formula that can be reached by substituting the occurrences of Term x by Term y
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.Function
Substitutes all the occurences of Term x by Term y.
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.Num
Substitutes all the occurences of Term x by Term y.
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.SimpleTerm
Substitutes all the occurences of Term x by Term y.
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.SkTerm
Substitutes all the occurences of Term x by Term y.
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.SVar
Substitutes all the occurences of Term a by Term b.
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.Term
Substitutes all the occurences of Term x by Term y.
sub(Term, Term) - Method in class Pandora.LogicParser.Formula.Var
Substitutes all the occurences of Term x by Term y.
Sub - Static variable in class Pandora.Types
 
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.And
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Atom
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Atom.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.BExp.EqualTo
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.BExp.GreaterThan
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.BExp.GTE
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.BExp.LessThan
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.BExp.LTE
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.BExp.NotEqual
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Equals
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Exists
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.False
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Forall
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Formula
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Iff
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Implies
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Not
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Or
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Predicate
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Predicate.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.True
Returns the Formula that is derived after substituting ALL the occurrences of Term x with Term y in this Formula.
subAll(Term, Term) - Method in class Pandora.LogicParser.Formula.Unknown
Returns the Formula that is derived after substituting ALL the occurrences of Term a with Term b in this Unknown.
subs_backwards - Static variable in class Pandora.Help.ErrorMessages
 
subs_backwards - Static variable in class Pandora.Help.HelpMessages
 
subs_forwards - Static variable in class Pandora.Help.ErrorMessages
 
subs_forwards - Static variable in class Pandora.Help.HelpMessages
 
Substitution - Class in Pandora.NDRules
Implements the Substitution rule.
Extends abstract class NDRule.
Substitution(ProofBox) - Constructor for class Pandora.NDRules.Substitution
Constructs a Substitution.
Subtract - Class in Pandora.LogicParser.Formula.AExp
Creates a subtraction expression.
Subtract(Term, Term) - Constructor for class Pandora.LogicParser.Formula.AExp.Subtract
Constructs a new Subtract AExp.
subVar(Predicate) - Method in class Pandora.LogicParser.Formula.Predicate
 
SVar - Class in Pandora.LogicParser.Formula
Creates an S variable term.
SVar(String) - Constructor for class Pandora.LogicParser.Formula.SVar
Constructs a new variable.
sym - Class in Pandora.LogicParser
CUP generated class containing symbol constants.
sym() - Constructor for class Pandora.LogicParser.sym
 

T

tempProofLines - Variable in class Pandora.ProofWindow
 
Term - Class in Pandora.LogicParser.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 Pandora.LogicParser.Formula.Term
 
TextFileReader - Class in Pandora.Help
 
TextFileReader(String) - Constructor for class Pandora.Help.TextFileReader
 
thereexist_elimination_forwards - Static variable in class Pandora.Help.HelpMessages
 
thereExists - Static variable in class Pandora.Help.ErrorMessages
 
thereExists - Static variable in class Pandora.Help.HelpMessages
 
thereexists_introduction_backwards - Variable in class Pandora.Help.HelpMessages
 
thereexists_introduction_backwards_no_constants - Variable in class Pandora.Help.HelpMessages
 
thereexists_introduction_forwards_input - Variable in class Pandora.Help.HelpMessages
 
thereexists_introduction_forwards_optional - Static variable in class Pandora.Help.HelpMessages
 
thereexists_introduction_forwards_specify - Static variable in class Pandora.Help.HelpMessages
 
thereexists_introduction_forwards_specify_input - Static variable in class Pandora.Help.HelpMessages
 
Tick - Class in Pandora.NDRules
Implements the Tick rule.
Tick(ProofBox) - Constructor for class Pandora.NDRules.Tick
Constructs a Tick.
Tick - Static variable in class Pandora.Types
 
TickFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Tick Rule.
TickKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'TickFile'.
tm - Static variable in class Pandora.Help.HelpMessages
 
TM - Class in Pandora.NDRules
Implements the Trust Me rule.
Extends abstract class NDRule.
TM(ProofBox) - Constructor for class Pandora.NDRules.TM
Constructs a Trust Me.
TM - Static variable in class Pandora.Types
 
tm_backwards - Static variable in class Pandora.Help.HelpMessages
 
tm_forwards - Static variable in class Pandora.Help.HelpMessages
 
tm_tick - Static variable in class Pandora.Help.HelpMessages
 
tm_tick_backwards - Static variable in class Pandora.Help.HelpMessages
 
TMFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the TM Rule.
TMKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'TMFile'.
TMProofLines - Variable in class Pandora.ProofWindow
 
TMTick - Class in Pandora.NDRules
Implements the Trust Me Tick rule.
TMTick(ProofBox) - Constructor for class Pandora.NDRules.TMTick
Constructs a Trust Me Tick.
TMTick - Static variable in class Pandora.Types
 
TOP - Static variable in class Pandora.LogicParser.sym
 
TopIntro - Class in Pandora.NDRules
Implements the Top Introduction rule.
Extends abstract class Rule.
TopIntro(ProofBox) - Constructor for class Pandora.NDRules.TopIntro
Constructs a FalsityIntro.
TopIntro - Static variable in class Pandora.Types
 
TopIntroductionFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the Top Introduction Rule.
TopIntroductionKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'TopIntroductionFile'.
True - Class in Pandora.LogicParser.Formula
The Top formula.
Extends abstract class Formula.
True() - Constructor for class Pandora.LogicParser.Formula.True
Constructs a Top Formula.
truth - Static variable in class Pandora.Help.ErrorMessages
 
truth - Static variable in class Pandora.Help.HelpMessages
 
Tuple - Class in Pandora.LogicParser.Formula
A Tuple of Terms.
Tuple(Term, Term) - Constructor for class Pandora.LogicParser.Formula.Tuple
Constructs a tuple.
Types - Class in Pandora
Constants for justifications.
Types() - Constructor for class Pandora.Types
 

U

undo() - Method in class Pandora.ProofWindow
Undoes rules which have been applied to the ProofBox.
undoList - Variable in class Pandora.ProofWindow
 
Unknown - Class in Pandora.LogicParser.Formula
The unknown item.
Unknown(String) - Constructor for class Pandora.LogicParser.Formula.Unknown
Constructs a new unknown.

V

valueChanged(TreeSelectionEvent) - Method in class Pandora.Help.Help
Handles the events thrown by the TreeSelectionListener.
Var - Class in Pandora.LogicParser.Formula
The Var (a Variable)
Extends abstract class Term.
Var(String) - Constructor for class Pandora.LogicParser.Formula.Var
Constructs a Var(A variable)
view - Variable in class Pandora.ProofWindow
 
View - Class in Pandora
View is a specialisation of JFrame, so when you create an instance of View, a new JFrame is created.
View(ParseInputController) - Constructor for class Pandora.View
Creates a new Pandora Window.
viewFile - Static variable in class Pandora.Help.HelpPagesHTML
The Help file for the View Menu.
viewKW - Static variable in class Pandora.Help.HelpPagesHTML
The keyword list of the 'viewFile'.

W

white - Static variable in class Pandora.xGui.Colour
 

Y

yetAnotherlightBlue - Static variable in class Pandora.xGui.Colour
 

_

_action_table - Static variable in class Pandora.LogicParser.parser
Parse-action table.
_production_table - Static variable in class Pandora.LogicParser.parser
Production table.
_reduce_table - Static variable in class Pandora.LogicParser.parser
reduce_goto table.

A B C D E F G H I J K L M N O P Q R S T U V W Y _