A Tableau Calculus for Regular Grammar Logics with Converse
From MaRDI portal
Publication:5191117
DOI10.1007/978-3-642-02959-2_31zbMath1250.03020MaRDI QIDQ5191117
Linh Anh Nguyen, Andrzej Szałas
Publication date: 28 July 2009
Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_31
03B45: Modal logic (including the logic of norms)
03B35: Mechanization of proofs and logical operations
Related Items
ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching, ExpTime tableau decision procedures for regular grammar logics with converse
Uses Software
Cites Work
- ExpTime tableau decision procedures for regular grammar logics with converse
- Modal tableau calculi and interpolation
- Decidability of SHIQ with complex role inclusion axioms
- Proof methods for modal and intuitionistic logics
- A near-optimal method for reasoning about action
- EXPtime tableaux for ALC
- Combining deduction and model checking into tableaux and algorithms for converse-PDL.
- Deciding regular grammar logics with converse through first-order logic
- Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs
- Optimizing description logic subsumption
- The Complexity of Regularity in Grammar Logics and Related Modal Logics
- EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
- Automated Reasoning with Analytic Tableaux and Related Methods
- An overview of tableau algorithms for description logics
- Analytic tableau systems and interpolation for the modal logics KB, KDB, K5, KD5
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
