Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@INPROCEEDINGS{GoetzmannEtAl:2009:Spartacus,
  title = {Spartacus: A Tableau Prover for Hybrid Logic},
  author = {Daniel Götzmann and Mark Kaminski and Gert Smolka},
  year = {2010},
  month = {May},
  editor = {Thomas Bolander and Torben Bra{\"u}ner},
  publisher = {Elsevier},
  booktitle = {M4M-6},
  series = {ENTCS},
  volume = {262},
  pages = {127-139},
}

Login to edit