Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse

DOI10.1007/978-3-540-71070-7_18zbMath1165.03317OpenAlexW1503578951MaRDI QIDQ3541703

Mark Kaminski, Gert Smolka

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_18

zbMATH Keywords

modal logichybrid logictableau systemsdecision proceduresconversedifference modality

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)

Related Items

Hybrid logic with the difference modality for generalisations of graphs, Terminating Tableaux for Hybrid Logic with Eventualities, Terminating tableau systems for hybrid logic with difference and converse

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Modal definability in enriched languages
• A guide to completeness and complexity for modal logics of knowledge and belief
• Modal logic with names
• EXPtime tableaux for ALC
• A tableau decision procedure for \(\mathcal{SHOIQ}\)
• Tableau methods of proof for modal logics
• Higher-Order Syntax and Saturation Algorithms for Hybrid Logic
• Tableau-based Decision Procedures for Hybrid Logic
• The modal logic of inequality
• A description logic with transitive and inverse roles and role hierarchies
• Derivation rules as anti-axioms in modal logic
• Practical reasoning for very expressive description logics
• The computational complexity of hybrid temporal logics
• On the Restraining Power of Guards
• Hybrid Tableaux for the Difference Modality
• Strongly analytic tableaux for normal modal logics
• Termination for Hybrid Tableaus
• EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies