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.