Terminating Tableau Calculi for Hybrid Logics Extending K

Thomas Bolander*, Patrick Blackburn

*Corresponding author for this work

Research output: Contribution to journalJournal articlepeer-review


This article builds on work by Bolander and Blackburn [Thomas Bolander and Patrick Blackburn. Termination for hybrid tableaus. Journal of Logic and Computation, 17(3):517-554, 2007] on terminating tableau systems for the minimal hybrid logic K. We provide (for the basic uni-modal hybrid language) terminating tableau systems for a number of non-transitive hybrid logics extending K, such as the logic of irreflexive frames, antisymmetric frames, and so on; these systems don't employ loop-checks. We also provide (for hybrid tense logic enriched with the universal modality) a terminating tableau calculus for the logic of transitive frames; this system makes use of loop-checks.

Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Issue numberC
Pages (from-to)21-39
Number of pages19
Publication statusPublished - 25 Mar 2009
Externally publishedYes


  • decision procedures
  • Hybrid logic
  • loop-checks
  • tableau systems
  • tense logic

Cite this