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

Related Items (5)

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

This page was built for publication: ExpTime tableau decision procedures for regular grammar logics with converse