Documentation For First Order Logic System

The First Order Logic Proof System currently resides in the first-order-logic branch of this repository. All relevant files are located in the first-order Folder. In addition, the ConditionalElim branch contains code for Conditional Elimination.

Files Within The first-order Folder:

• expressionparser.h and expressionparser.cpp. This is a Helper Function for the Shunting Yard Algorithm (i.e., See Notes Under FirstOrderTree).

• FirstOrderTree.h and FirstOrderTree.cpp. This is the structure that the First Order Logic System uses to store expressions. It is a Tree Structure based on the Original Tree Structure that was created for storing expressions in ALPACA. It uses the Shunting Yard Algorithm to parse in an expression and store it in the tree.

• ProofChecker.h and ProofChecker.cpp. These files contain the Main Functionality of the First Order Logic System. ProofChecker, as the name implies, is responsible for proving that one statement follows from a set of previous statement. This file is very important, so we will discuss it in its own section.

Using ProofChecker Class:

Calling the general ProofChecker() constructor constructs a new ProofChecker Object with an empty statement and the justification "Introduction".

If you are trying to construct a Proof to prove that expression a follows from other expressions, call the string constructor ProofChecker(a) where a is the expression represented as a string.

To set the justification for your proof, call the changeJustification(j) function on the ProofChecker Object, where j is the justification represented as a string. The following justifications are supported:

• "~I": Negation Introduction
• "~E": Negation Elimination
• "&I": And Introduction
• "&E": And Elimination
• "|I": Or Introduction
• "|E": Or Elimination
• ">I": Conditional Introduction
• ">E": Conditional Elimination
• "=I": Biconditional Introduction
• "=E": Biconditional Elimination

Forall Introduction/Elimination and Exists Introduction/Elimination are not yet supported. However, we do plan to support them as this is part of First Order Logic.

As of right now, AND Introduction Rule, AND Elimination Rule, Conditional Elimination Rule, OR Introduction Rule, NOT Introduction Rule, NOT Elimination Rule are initially implemented. Note: NOT Introduction Rule needs to be further reviewed to account for seeing if statements correctly "follow" from other statements.

Now, we will describe an overview of the implementation for the currently supported rules:

1. AND Introduction Rule: Currently the AND Introduction Rule makes use of the Recursive isSubtreeSame() Helper Function To Determine If The Current & Statement's Left + Right Children Are Exactly The Same As The Justification Statements. Also, the current implementation makes use of the common accepted rule of AND Introduction Rule which is that there can only be at most two justification statements.
2. AND Elimination Rule: Currently the AND Elimination Rule also makes use of the Recursive isSubtreeSame() Helper Function To Determine If The Current Statement Is Either The Left Child of The Justification Child Statement OR The Right Child "". Remember, that in this case, the current statement would be some complex statement like (A | B) with the child statement being a conjunction such as (A | B) & (C = D). In these ways, the current statement is linked back to the main conjunctive statement and it is then correctly determined whether the current statement follows as such.
3. Conditional Elimination Rule: The Conditional Elimination takes in two justification statements. It figures out which one has the conditional, and makes sure that the antecedent of the conditional matches the other justification statement. Similarly, it takes the consequent of the conditional and makes sure it matches with the current statement. Currently, the Conditional Elimination Rule compares trees using their getString() methods, as it was implemented before the isSubtreeSame() helper function. However, it would still function if changed to be consistent with And Introduction.
4. The OR Introduction Rule simply checks that the goal's head node's opType is |, and that the child statement is present in either the right or left subtree of the goal. If so, the proof is valid.
5. Biconditional Elimination first looks at the two children statements and locates the one that contains an = optype (if this is not present, the proof fails). It then takes that first child's statement and verifies that its right or left subtree is equal to the second child statement. If the other subtree of the first child is equal to the goal, the proof is valid.
6. Negation Introduction requires that you have a child statement of the form A, a child statement of the form ~B, and a statement of the form B (the last child statement must be the opposite of one of the first two children). It then allows you to prove ~A.
7. Negation Elimination requires that you have a child statement of the form ~B, a child statement of the form ~C, and a statement of the form B (the last child statement must be the opposite of one of the first two children). It then allows you to prove C. This is very similar to negation introduction.

To add "children" statements to your Proof (i.e., statements that support your Final Conclusion), use the addChild(c) function where c is a FirstOrderTree Object representing the expression.

Finally, to check whether your Proof is Valid, run this isValid() function where a Boolean Value is returned.

• ProofCheckerTest.cpp. Test File for ProofChecker. Runs Testing Suite For All Implemented Rules.

• treeTest.cpp. Test File for the First Order Tree Structure with the Shunting Yard Algorithm.