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.
Keywords for this software
References in zbMATH (referenced in 11 articles )
Showing results 1 to 11 of 11.
- Blackburn, Patrick; Bolander, Thomas; Braüner, Torben; Jørgensen, Klaus Frovin: Completeness and termination for a Seligman-style tableau system (2017)
- Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare: $\text K_ \textS\textP$: a resolution-based prover for multimodal K (2016)
- Areces, Carlos; Orbe, Ezequiel: Symmetric blocking (2015)
- Kaminski, Mark; Smolka, Gert: A goal-directed decision procedure for hybrid PDL (2014)
- Kaminski, Mark; Tebbi, Tobias: InKreSAT: modal reasoning via incremental reduction to SAT (2013)
- Kaminski, Mark; Schneider, Sigurd; Smolka, Gert: Terminating tableaux for graded hybrid logic with global modalities and role hierarchies (2011)
- Madeira, Alexandre; Faria, José M.; Martins, Manuel A.; Barbosa, Luís S.: Hybrid specification of reactive systems: an institutional approach (2011)
- Cerrito, Serenella; Mayer, Marta Cialdea: An efficient approach to nominal equalities in hybrid logic tableaux (2010)
- Cialdea Mayer, Marta; Cerrito, Serenella: Herod and Pilate: two tableau provers for basic hybrid logic (2010)
- Götzmann, Daniel; Kaminski, Mark; Smolka, Gert: Spartacus: a tableau prover for hybrid logic (2010) ioport
- Kaminski, Mark; Smolka, Gert: Terminating tableaux for hybrid logic with eventualities (2010)