ExpTime tableau decision procedures for regular grammar logics with converse

DOI10.1007/S11225-011-9341-3MaRDI QIDQ763333zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

modal logicsatisfiabilityautomated reasoningtableauxglobal cachingregular grammar logics with converse

Mathematics Subject Classification ID

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)

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

Cites work

• scientific article; zbMATH DE number 5295720 (Why is no real title available?)
• scientific article; zbMATH DE number 1189095 (Why is no real title available?)
• A Tableau Calculus for Regular Grammar Logics with Converse
• A near-optimal method for reasoning about action
• An efficient tableau prover using global caching for the description logic \({\mathcal{ALC}}\)
• An overview of tableau algorithms for description logics
• Analytic Cut-Free Tableaux for Regular Modal Logics of Agent Beliefs
• Analytic tableau systems and interpolation for the modal logics KB, KDB, K5, KD5
• Automated Reasoning with Analytic Tableaux and Related Methods
• Checking consistency of an ABox w.r.t. global assumptions in PDL
• Combining deduction and model checking into tableaux and algorithms for converse-PDL.
• Decidability of SHIQ with complex role inclusion axioms
• Deciding regular grammar logics with converse through first-order logic
• EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
• EXPtime tableaux for ALC
• Horn knowledge bases in regular description logics with PTime data complexity
• Modal tableau calculi and interpolation
• Optimal and cut-free tableaux for propositional dynamic logic with converse
• Optimizing description logic subsumption
• Proof methods for modal and intuitionistic logics
• Sound global state caching for ALC with inverse roles
• Tableau methods for modal and temporal logics
• The Complexity of Regularity in Grammar Logics and Related Modal Logics

Cited in

(8)

• Modal logics with hard diamond-free fragments
• Efficient local reductions to basic modal logic
• The Complexity of Regularity in Grammar Logics and Related Modal Logics
• Automated Reasoning with Analytic Tableaux and Related Methods
• ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
• Deciding regular grammar logics with converse through first-order logic
• A Tableau Calculus for Regular Grammar Logics with Converse
• Local is best: efficient reductions to modal logic \textsf{K}

Describes a project that uses

Uses Software

• KL-ONE

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)