Terminating tableau systems for hybrid logic with difference and converse
From MaRDI portal
Publication:1047795
DOI10.1007/s10849-009-9087-8zbMath1188.03013MaRDI QIDQ1047795
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
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 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
- 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
