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.

References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Alviano, Mario; Batsakis, Sotiris; Baryannis, George: Modal logic S5 satisfiability in answer set programming (2021)
  2. Cialdea Mayer, Marta: A prover dealing with nominals, binders, transitivity and relation hierarchies (2020)
  3. Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare: (\mathrmK_\mathrmS\mathrmP) a resolution-based theorem prover for (\mathsfK_n): architecture, refinements, strategies and experiments (2020)
  4. Lagniez, Jean-Marie; Le Berre, Daniel; de Lima, Tiago; Montmirail, Valentin: An assumption-based approach for solving the Minimal S5-Satisfiability problem (2018)
  5. Blackburn, Patrick; Bolander, Thomas; Braüner, Torben; Jørgensen, Klaus Frovin: Completeness and termination for a Seligman-style tableau system (2017)
  6. Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare: (\mathrmK_ \mathrmS\mathrmP): a resolution-based prover for multimodal K (2016)
  7. Areces, Carlos; Orbe, Ezequiel: Symmetric blocking (2015)
  8. Kaminski, Mark; Smolka, Gert: A goal-directed decision procedure for hybrid PDL (2014)
  9. Kaminski, Mark; Tebbi, Tobias: InKreSAT: modal reasoning via incremental reduction to SAT (2013)
  10. Kaminski, Mark; Schneider, Sigurd; Smolka, Gert: Terminating tableaux for graded hybrid logic with global modalities and role hierarchies (2011)
  11. Madeira, Alexandre; Faria, José M.; Martins, Manuel A.; Barbosa, Luís S.: Hybrid specification of reactive systems: an institutional approach (2011)
  12. Cerrito, Serenella; Mayer, Marta Cialdea: An efficient approach to nominal equalities in hybrid logic tableaux (2010)
  13. Cialdea Mayer, Marta; Cerrito, Serenella: Herod and Pilate: two tableau provers for basic hybrid logic (2010)
  14. Götzmann, Daniel; Kaminski, Mark; Smolka, Gert: Spartacus: a tableau prover for hybrid logic (2010) ioport
  15. Kaminski, Mark; Smolka, Gert: Terminating tableaux for hybrid logic with eventualities (2010)