There are two theorem
provers running based on papers I have cowritten.
The first one is a theoremprover 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 324340.
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 theoremprover
for temporal logics.
You can try the prover by clicking here.
The other prover works for twodimensional 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:755778, 1999
Available as postscript.
Abstract: A sound and complete labelled
tableau calculus is presented for twodimensional
modal logic interpreted on local squares. We also
give a short system description of the Prolog
theoremprover based on the calculus.
Logic Journal of the IGPL, 7/6:755778,
1999.
The prover is availbale here.
