Saarland University Computer Science

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.


Tableau calculus and pattern-based blocking:

Implementation and optimization techniques:

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