Journal article · Conference paper
Terminating Tableau Calculi for Hybrid Logics extending K
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.
Language: | English |
---|---|
Year: | 2009 |
Pages: | 21-39 |
Proceedings: | Methods for Modalities |
ISSN: | 15710661 |
Types: | Journal article and Conference paper |
DOI: | 10.1016/j.entcs.2009.02.027 |
ORCIDs: | Bolander, Thomas |