Dr Szabolcs Mikulas / Research / Theorem Provers
Theorem - Provers
There are two theorem provers running based on papers I have co-written.

The first one is a theorem-prover for temporal logic with future and past over linear flow of time. It is written by Mark Reynolds and based on the paper:

Maarten Marx, Szabolcs Mikulas, and Mark Reynolds, The mosaic method for temporal logics. In R.Dyckhoff, editor, Tableaux 2000, volume 1847 of Lecture Notes in Artificial Intelligence, pages 324-340. Springer Verlag, 2000
An earlier version is available as postscript.
Abstract: We apply the mosaic idea to temporal logics to get easy proofs for completeness, decidability and complexity. Furthermore, we sketch how to implement the mosaic idea to design a theorem-prover for temporal logics.
You can try the prover by clicking here.

The other prover works for two-dimensional local square modal logic. It is written by Maarten Marx and Stefan Schlobach. You can see the theoretical background at the following paper:

Maarten Marx, Szabolcs Mikulas, and Stefan Schlobach, Tableau calculus for local cubic modal logic and its implementation. Logic Journal of the IGPL, 7:755-778, 1999
Available as postscript.
Abstract: A sound and complete labelled tableau calculus is presented for two-dimensional modal logic interpreted on local squares. We also give a short system description of the Prolog theorem-prover based on the calculus.
Logic Journal of the IGPL, 7/6:755-778, 1999.
The prover is availbale here.