Terminating tableau systems for hybrid logic with difference and converse

DOI10.1007/s10849-009-9087-8zbMath1188.03013OpenAlexW1981904119MaRDI 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 logichybrid logictableau systemsdifference modalitytableau-based decision procedure

Mathematics Subject Classification ID

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

Related Items

An efficient approach to nominal equalities in hybrid logic tableaux, Lightweight hybrid tableaux, Quantified multimodal logics in simple type theory, Combining and automating classical and non-classical logics in classical higher-order logics, Completeness in hybrid type theory, A Tableaux Based Decision Procedure for a Broad Class of Hybrid Formulae with Binders, Terminating Tableaux for Hybrid Logic with Eventualities, Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners), 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

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item