Spartacus

Spartacus is a tableau prover for hybrid logic with global modalities. The key difference of Spartacus to other modal reasoners is the blocking technique used to achieve termination. Spartacus is the first system to implement pattern-based blocking, a novel blocking technique for converse-free modal and hybrid logics. Spartacus implements a number of optimizations, including both established and new techniques.

References

Tableau calculus and pattern-based blocking:

Mark Kaminski and Gert Smolka.
Terminating Tableau Systems for Hybrid Logic with Difference and Converse.
Journal of Logic, Language and Information 18(4), pp. 437-464, October 2009. © Springer.
Mark Kaminski and Gert Smolka.
Hybrid Tableaux for the Difference Modality.
In Proc. 5th Workshop on Methods for Modalities (M4M-5), ENTCS 231, pp. 241-257, March 2009. © Elsevier.

Implementation and optimization techniques:

Daniel Götzmann, Mark Kaminski, and Gert Smolka.
Spartacus: A Tableau Prover for Hybrid Logic.
In Proc. 6th Workshop on Methods for Modalities (M4M-6), ENTCS 262, pp. 127-139, May 2010. © Elsevier.
Daniel Götzmann.
Spartacus: A Tableau Prover for Hybrid Logic.
M.Sc. Thesis, Saarland University, January 2009.

New: You can now use Spartacus without having to install it! Check out the new

Spartacus Online Demo

Also, feel free to download Spartacus and play with it on your own machine! Spartacus is written in Standard ML and compiled with MLton. The current version is

spartacus-1.1.3.tar.bz2 (113 kB)

Historical versions and some benchmark problems can be found on Daniel's web page.

Webmaster, Tue Apr 27 16:02:19 2021