First Order Logic Modifications

Author: Tobias Park

If we want to build first order logic support in ALPACA, we may have to make slight modifications to the structure which stores logical expressions.

Specifically, Tree.cpp, line 138 and beyond, presents an issue - 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, as this is a bit silly.