Terminating Tableau Calculi for Hybrid Logics Extending K

Thomas Bolander*, Patrick Blackburn

*Corresponding author

Publikation: Bidrag til tidsskriftTidsskriftartikelpeer review

Abstract

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.
OriginalsprogEngelsk
TidsskriftElectronic Notes in Theoretical Computer Science
Vol/bind231
Udgave nummerC
Sider (fra-til)21-39
Antal sider19
ISSN1571-0661
DOI
StatusUdgivet - 25 mar. 2009
Udgivet eksterntJa

Emneord

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

Citer dette