Spartacus: A Tableau Prover for Hybrid Logic

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.

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: Daniel Götzmann, Mark Kaminski, Gert Smolka
• Keywords: ENTCS 2010, Hybrid Multimodal Logic, Lazy Branching, Spartacus