Spartacus: A Tableau Prover for Hybrid Logic
Hybrid logics are expressive extensions of modal logics that contain special symbols, called nominals, which are used to refer to individual states. The expressiveness can be increased even further if additional operators like universal modalities or the difference modality are used.
In order to make practical use of the expressiveness of hybrid logics, efficient tools are needed. Of great importance is the decision problem for hybrid logic. For any given hybrid formula, one wants to be able to decide whether it is satisfiable or not. One approach to decide satisfiability of hybrid logic formulas is to use a tableau-based algorithm. To make the tableau approach scale to practical problems, sophisticated implementation and optimization techniques are used.
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.
Additional information about Spartacus can be found on its project page.