Publication details

Saarland University Computer Science

Spartacus: A Tableau Prover for Hybrid Logic

Daniel Götzmann, Mark Kaminski, Gert Smolka

M4M-6, Vol. 262 of ENTCS, pp. 127-139, Elsevier, May 2010

Spartacus is a tableau prover for hybrid multimodal logic with global modalities and reflexive and transitive relations. Spartacus is the first system to use pattern-based blocking for termination. To achieve a competitive performance, Spartacus implements a number of optimization techniques, including a new technique that we call lazy branching. We evaluate the practical impact of pattern-based blocking and lazy branching for the basic modal logic K and observe high effectiveness of both techniques.

DOI: 10.1016/j.entcs.2010.04.010

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy