We have successfully extended OOPS to support new axiom schemes. We made it possible to add new axiom system because of the reusability of the rules and relations.

We also made some changes to the GUI to make it easier to work with the program. Specially the new editor with highlighting can make it a bit easier for people to work with OOPS.

We have made an axiom test script to check all of the axiom scheme to see if they work correctly. When a new axiom is added to OOPS the script can be update easily to check if the prover is implemented correctly.

Unfortunately we haven’t implemented the C axiom, we couldn’t figure out how to prevent it from going into an infinite loop.