Terminating tableau systems for hybrid logic with difference and converse

DOI10.1007/s10849-009-9087-8zbMath1188.03013MaRDI QIDQ1047795

Gert Smolka, Mark Kaminski

Publication date: 6 January 2010

Published in: Journal of Logic, Language and Information (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10849-009-9087-8

zbMATH Keywords

modal logic; hybrid logic; tableau systems; difference modality; tableau-based decision procedure

Mathematics Subject Classification ID

03B45: Modal logic (including the logic of norms)

03B35: Mechanization of proofs and logical operations

03B62: Combined logics

Related Items

Terminating Tableaux for Hybrid Logic with Eventualities, Completeness in hybrid type theory, Lightweight hybrid tableaux, Combining and automating classical and non-classical logics in classical higher-order logics, Quantified multimodal logics in simple type theory, A prover dealing with nominals, binders, transitivity and relation hierarchies, Blocking and other enhancements for bottom-up model generation methods, A tableaux calculus for default intuitionistic logic, A goal-directed decision procedure for hybrid PDL, A tableau based decision procedure for an expressive fragment of hybrid logic with binders, converse and global modalities, Extended decision procedure for a fragment of HL with binders, An efficient approach to nominal equalities in hybrid logic tableaux, A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders, Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The seven virtues of simple type theory
• A guide to completeness and complexity for modal logics of knowledge and belief
• Modal logic with names
• A tableau decision procedure for \(\mathcal{SHOIQ}\)
• Tableau-based Decision Procedures for Hybrid Logic
• Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
• The modal logic of inequality
• A description logic with transitive and inverse roles and role hierarchies
• Hybrid Tableaux for the Difference Modality
• Termination for Hybrid Tableaus
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi