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

automated reasoningglobal cachingmodal logicregular grammar logics with conversesatisfiabilitytableaux

Mathematics Subject Classification ID

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

Review text

The paper presents sound and complete tableau calculi for the general satisfiability problem of regular grammar logics with converse and the problem of checking consistency of an ABox w.r.t. a TBox in such a logic. The authors use a direct approach instead of a translation to another logic, which seems to be something new for grammar logics with converse. In particular, they give an optimal decision procedure for the general satisfiability problem of REGc logics with the corresponding complexity proofs. They prove the new result that the data complexity of the instance checking problem in regular grammar logics is coNP-complete.

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

• A near-optimal method for reasoning about action
• A Tableau Calculus for Regular Grammar Logics with Converse
• 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 for ALC
• EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies
• Horn knowledge bases in regular description logics with PTime data complexity
• scientific article; zbMATH DE number 5295720 (Why is no real title available?)
• scientific article; zbMATH DE number 1189095 (Why is no real title available?)
• 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)

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

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)