ExpTime tableau decision procedures for regular grammar logics with converse
DOI10.1007/S11225-011-9341-3zbMATH Open1244.03055OpenAlexW2110126675MaRDI QIDQ763333FDOQ763333
Linh Anh Nguyen, Andrzej Szałas
Publication date: 9 March 2012
Published in: Studia Logica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s11225-011-9341-3
modal logicsatisfiabilityautomated reasoningtableauxglobal cachingregular grammar logics with converse
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35)
Cites Work
- EXPtime tableaux for ALC
- Decidability of SHIQ with complex role inclusion axioms
- Combining deduction and model checking into tableaux and algorithms for converse-PDL.
- Tableau methods for modal and temporal logics
- A near-optimal method for reasoning about action
- Checking Consistency of an ABox w.r.t. Global Assumptions in PDL
- Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs
- Sound Global State Caching for ALC with Inverse Roles
- Optimizing description logic subsumption
- A Tableau Calculus for Regular Grammar Logics with Converse
- Title not available (Why is that?)
- EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
- Optimal and Cut-Free Tableaux for Propositional Dynamic Logic with Converse
- An overview of tableau algorithms for description logics
- Analytic tableau systems and interpolation for the modal logics KB, KDB, K5, KD5
- Modal tableau calculi and interpolation
- Proof methods for modal and intuitionistic logics
- Deciding regular grammar logics with converse through first-order logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The Complexity of Regularity in Grammar Logics and Related Modal Logics
- Automated Reasoning with Analytic Tableaux and Related Methods
Cited In (7)
- Modal Logics with Hard Diamond-Free Fragments
- The Complexity of Regularity in Grammar Logics and Related Modal Logics
- Automated Reasoning with Analytic Tableaux and Related Methods
- Efficient local reductions to basic modal logic
- A Tableau Calculus for Regular Grammar Logics with Converse
- ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
- Local is best: efficient reductions to modal logic \textsf{K}
Uses Software
This page was built for publication: ExpTime tableau decision procedures for regular grammar logics with converse
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q763333)
