ExpTime tableau decision procedures for regular grammar logics with converse

DOI10.1007/s11225-011-9341-3zbMath1244.03055OpenAlexW2110126675MaRDI QIDQ763333

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

zbMATH Keywords

modal logicautomated reasoningtableauxsatisfiabilityglobal cachingregular grammar logics with converse

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)

Related Items

Modal Logics with Hard Diamond-Free Fragments, ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching, A Tableau Calculus for Regular Grammar Logics with Converse, Efficient local reductions to basic modal logic, Local is best: efficient reductions to modal logic \textsf{K}

Uses Software

• KL-ONE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• 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
• The Complexity of Regularity in Grammar Logics and Related Modal Logics
• A Tableau Calculus for Regular Grammar Logics with Converse
• EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
• Automated Reasoning with Analytic Tableaux and Related Methods
• 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