We have been able to successfully add new axioms system to OOPS. Instead of only using S5, OOPS can now use all of the following axiom systems:

• K
• KE
• T
• B
• D
• K4
• K45
• KD45
• S4
• S4E
• S5
• S5E

Therefore the abbreviation of OOPS isn’t correct anymore since it can now prove for more than just the S5 system. Since, however, most of the underlying mechanics are from the original OOPS project, we have not changed the name of the project.

The visualization of the kripke model of counter examples has also been modified accordingly, where each axiom system specifies its own requirements for the kripke model. The relations that were implemented were seriality, reflexivity, transitivity and symmetry.

There are also some adjustments made to the GUI. The user can easily select which prover to use (while this is also possible from Lua), the implementation of an ‘Edit’ menu ( cut, copy, paste, undo, redo ), and it’s also possible to select a different editor which shows line numbers and has syntax-highlighting.

There is one operator that we didn’t implement and that is the C, the common knowledge operator. The problem is that trying to prove C would cause infinite recursion, since Cφ → Eφ ∧ ECφ, or in layman's terms, if something is common knowledge, then everyone knows it, and everyone knows it's common knowledge. Therefore we still have a C which will use the same rules and will end up in an infinite loop.

The new axioms in OOPS: