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: <a href="http://dx.doi.org/10.1016/j.entcs.2010.04.010">10.1016/j.entcs.2010.04.010</a> <!-- Also available from <a href="http://www.ruc.dk/dat_en/research/reports/128/">http://www.ruc.dk/dat_en/research/reports/128/</a><br> -->