article

Terminating Tableau Calculi for Hybrid Logics Extending K

Authors:

Thomas Bolander,

Patrick BlackburnAuthors Info & Claims

Electronic Notes in Theoretical Computer Science (ENTCS), Volume 231

Pages 21 - 39

https://doi.org/10.1016/j.entcs.2009.02.027

Published: 01 March 2009 Publication History

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.

References

[1]

Areces, Carlos, Blackburn, Patrick and Marx, Maarten, Hybrid logics: Characterization, interpolation and complexity. Journal of Symbolic Logic. v66. 977-1010.

Google Scholar

[2]

Blackburn, Patrick, Nominal tense logic. Notre Dame Journal of Formal Logic. v34 i1. 56-83.

Google Scholar

[3]

Blackburn, Patrick, Internalizing labelled deduction. Journal of Logic and Computation. v10. 137-168.

Google Scholar

[4]

Blackburn, Patrick, de Rijke, Marrten and Venema, Yde, Modal Logic. In: Cambridge Tracts in Theoretical Computer Science, volume 53. Cambridge University Press, Cambridge, UK.

Google Scholar

[5]

Patrick Blackburn, Claire Gardent, and Wilfried Meyer-Viol. Talking about trees. In Proceedings of the 6th Conference of the European Chapter of the Association for Computational Linguistics, pages 21--29, 1993

Digital Library

Google Scholar

[6]

Blackburn, Patrick and Meyer-Viol, Wilfried, Linguistics, logic, and finite trees. Logic Journal of the IGPL. v2. 3-29.

Google Scholar

[7]

Bolander, Thomas and Blackburn, Patrick, Termination for hybrid tableaus. Journal of Logic and Computation. v17 i3. 517-554.

Google Scholar

[8]

Bolander, Thomas and Braüner, Torben, Tableau-based decision procedures for hybrid logic. Journal of Logic and Computation. v16. 737-763.

Google Scholar

[9]

Gargov, George and Goranko, Valentin, Modal logic with names. Journal of Philosophical Logic. v22 i6. 607-636.

Google Scholar

[10]

Rajeev Gore. Tableau methods for modal and temporal logics. Technical Report TR-ARP-15-95, Australian National University, November 1995

Google Scholar

[11]

ten Cate, Balder and Franceschet, Massimo, On the complexity of hybrid logics with binders. In: Lecture Notes in Computer Science, volume 3634. Springer Verlag. pp. 339-354.

Digital Library

Google Scholar

[12]

Tzakova, Miroslava, Tableau calculi for hybrid logics. Lecture Notes in Computer Science. v1617. 278-292.

Digital Library

Google Scholar

Cited By

View all

Nguyen L(2019)ExpTime Tableaux with Global Caching for Hybrid PDLJournal of Automated Reasoning10.1007/s10817-018-09506-864:1(21-52)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.1007/s10817-018-09506-8
Cialdea Mayer M(2018)Extended Decision Procedure for a Fragment of HL with BindersJournal of Automated Reasoning10.1007/s10817-014-9307-z53:3(305-315)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1007/s10817-014-9307-z
Christoff ZHansen J(2015)A logic for diffusion in social networksJournal of Applied Logic10.1016/j.jal.2014.11.01113:1(48-77)Online publication date: 1-Mar-2015
https://dl.acm.org/doi/10.1016/j.jal.2014.11.011
Show More Cited By

Terminating Tableau Calculi for Hybrid Logics Extending K
1. Theory of computation
  1. Logic
  2. Models of computation

Recommendations

Higher-Order Syntax and Saturation Algorithms for Hybrid Logic

We present modal logic on the basis of the simply typed lambda calculus with a system of equational deduction. Combining first-order quantification and higher-order syntax, we can maintain modal reasoning in terms of classical logic by remarkably simple ...
Clausal Tableaux for Hybrid PDL

We present the first tableau-based decision procedure for PDL with nominals. The procedure is based on a prefix-free clausal tableau system designed as a basis for gracefully degrading reasoners. The clausal system factorizes reasoning into regular, ...
Tableau Calculi for Hybrid Logics
TABLEAUX '99: Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods

Hybrid logics were proposed in [15] as a way of boosting the expressivity of modal logics via a novel mechanism: adding labels for states in Kripke models and viewing these labels as formulae. In addition, hybrid logics may contain quantifiers to bind ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Electronic Notes in Theoretical Computer Science (ENTCS)

Electronic Notes in Theoretical Computer Science (ENTCS) Volume 231, Issue

March, 2009

347 pages

ISSN:1571-0661

Issue’s Table of Contents

Publisher

Elsevier Science Publishers B. V.

Netherlands

Publication History

Published: 01 March 2009

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Nguyen L(2019)ExpTime Tableaux with Global Caching for Hybrid PDLJournal of Automated Reasoning10.1007/s10817-018-09506-864:1(21-52)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.1007/s10817-018-09506-8
Cialdea Mayer M(2018)Extended Decision Procedure for a Fragment of HL with BindersJournal of Automated Reasoning10.1007/s10817-014-9307-z53:3(305-315)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1007/s10817-014-9307-z
Christoff ZHansen J(2015)A logic for diffusion in social networksJournal of Applied Logic10.1016/j.jal.2014.11.01113:1(48-77)Online publication date: 1-Mar-2015
https://dl.acm.org/doi/10.1016/j.jal.2014.11.011
Mayer M(2013)A proof procedure for hybrid logic with binders, transitivity and relation hierarchiesProceedings of the 24th international conference on Automated Deduction10.1007/978-3-642-38574-2_5(76-90)Online publication date: 9-Jun-2013
https://dl.acm.org/doi/10.1007/978-3-642-38574-2_5

Abstract

References

Cited By

Recommendations

Higher-Order Syntax and Saturation Algorithms for Hybrid Logic

Clausal Tableaux for Hybrid PDL

Tableau Calculi for Hybrid Logics

Comments

Information

Published In

Publisher

Publication History

Author Tags

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations