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.
|
