Publication details

Saarland University Computer Science

Spartacus: A Tableau Prover for Hybrid Logic

Daniel Götzmann

M.Sc. Thesis, Programming Systems Lab, Department of Computer Science, Saarland University, January 2009

This thesis presents Spartacus, a tableau-based reasoner for hybrid logic with global modalities and reflexive and transitive relations. To obtain termination in the presence of global modalities and transitive relations, Spartacus uses pattern-based blocking. To achieve a competitive performance on practical problems, we employ a range of optimization techniques.
After describing the architecture of Spartacus, we evaluate the impact of pattern-based blocking and the implemented optimization techniques and heuristics on the performance of the prover. We also compare our system with existing reasoners for modal and description logics.
From the evaluation we conclude that pattern-based blocking is a promising technique that can significantly improve the performance of modal reasoning.

Download PDF        Show BibTeX               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009