ExpTime tableau decision procedures for regular grammar logics with converse
DOI10.1007/S11225-011-9341-3zbMATH Open1244.03055OpenAlexW2110126675MaRDI QIDQ763333FDOQ763333
Authors: 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
Recommendations
- A Tableau Calculus for Regular Grammar Logics with Converse
- Automated Reasoning with Analytic Tableaux and Related Methods
- Deciding regular grammar logics with converse through first-order logic
- The Complexity of Regularity in Grammar Logics and Related Modal Logics
- scientific article; zbMATH DE number 6302922
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
- An efficient tableau prover using global caching for the description logic \({\mathcal{ALC}}\)
- 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?)
- Horn knowledge bases in regular description logics with PTime data complexity
- 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 (8)
- Modal Logics with Hard Diamond-Free Fragments
- Deciding regular grammar logics with converse through first-order logic
- 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)
