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.