First Order Logic Modifications

Author: Tobias Park

The following is a list of modifications that we may need to make to ALPACA to support first order logic proofs.

1. Tree.cpp, line 138 and beyond - ALPACA's tree structure does not natively support -> and = expressions. Instead, it converts them into OR statements. In first order logic proofs, we need to be able to support conditional introduction/elimination and = introduction/elimination, and we cannot do this if every -> and = symbol is simply turned into an OR statement.

Possible solutions:

• Create a new type of Node in the structure that supports > statements; for instance, it can be a Node object that stores a premise statement and a conclusion statement.
• Still convert > and = to OR statements, but make a note (via a private variable, perhaps) that the statement was originally an > or = -type statement. Then, the first order logic program can be programmed to be able to notice this and tree the modified OR statements as if they were their original > or = counterparts. However, this could be complicated and messy; it may not be an elegant solution.

Also, we may want to remove the requirement to have parentheses around everything....

2. statementevaluator.cpp is not applicable for first order logic because we are not creating truth tables.... unless we want a tool that acts as an automated theorem prover, such as Taut Con in Professor Bram's Intro to Logic Class.