Terminating Tableau Calculi for Hybrid Logics Extending K
Copyright policy )Terminating Tableau Calculi for Hybrid Logics Extending K
AbstractThis 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.
Hybrid logic, tableau systems, loop-checks, tense logic, decision procedures, Theoretical Computer Science, Computer Science(all)
Hybrid logic, tableau systems, loop-checks, tense logic, decision procedures, Theoretical Computer Science, Computer Science(all)
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).8 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!