Home

This is OOPS, an Object Oriented Prover for S5n. OOPS was created by Gert van Valkenhoef and Elske van der Vaart in the context of a Multi-Agent Systems course project at the University of Groningen.

OOPS makes use of a tableau proof method in order to prove or disprove formulas in the S5n modal logic. OOPS is open source, cross-platform and easy to get running. OOPS is implemented in Java (5.0) and comes with a GUI that enables the visualization of the generated tableaux as well as counter-models. Furthermore, OOPS comes with an integrated scripting language (Lua) that allows powerful interactions with the tableau generator.

Please note: analysis during the ‘Elaborations on OOPS’ project has shown that the proof method employed by OOPS is in EXPTIME. However we believe that some of the features implemented during the same project may still make the tool worthwhile (e.g. visualization of tableaux, generation of counter models).

To encourage future work on OOPS, the source code is available under the GNU General Public License (GNU GPL).

Current Release

See Releases to get the current version and/or the associated source code.