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).
The current release is version 0.6.4, made available on 2014-05-19 (a minor patch for version 0.6.3 of 2009-11-29). See ‘downloads’ to get this version and/or the associated source code.
In 2012, Lourens Elzinga and Rik Timmers (with some help from Wouter Reckman) extended OOPS to handle many other axiom systems. They have also made some other improvements (e.g. a syntax-highlighting editor). To my shame, I have not yet released these changes. See their project page for documentation.
See the “extensions” branch if you want to give it a try. As I understand, there are some issues to be resolved with the new editor.