PSpace reasoning for graded modal logics

DOI10.1093/LOGCOM/11.1.85MaRDI QIDQ2720401zbMATH OpenOpenAlexFDO

Authors Stephan Tobies

Publication date 16 September 2002

Published in Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/cs/0005009

zbMATH Keywords

computational complexitydescription logicgraded modal logicgraded modalitiesPSpace algorithmsatisfiability

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Analysis of algorithms and problem complexity (68Q25)

Abstract: We present a PSPACE algorithm that decides satisfiability of the graded modal logic Gr(K_R)---a natural extension of propositional modal logic K_R by counting expressions---which plays an important role in the area of knowledge representation. The algorithm employs a tableaux approach and is the first known algorithm which meets the lower bound for the complexity of the problem. Thus, we exactly fix the complexity of the problem and refute an ExpTime-hardness conjecture. We extend the results to the logic Gr(K_(R cap I)), which augments Gr(K_R) with inverse relations and intersection of accessibility relations. This establishes a kind of ``theoretical benchmark that all algorithmic approaches can be measured against.

Review text

The paper presents a PSpace algorithm that decides satisfiability of graded modal logic \(\text{Gr(K}_R)\) -- a natural extension of the propositional modal logic \(\text{K}_R\) by counting expressions. The algorithm is based on the tableaux algorithms for \(\text{K}_R\) and tries to prove satisfiability of a given formula by explicitly constructing a model for it. Using an extension of the proposed techniques, the author obtains a PSpace algorithm for the logic which extends \(\text{Gr(K}_R)\) by the inverse relation and the intersection of relations. This solves an open problem.

Recommendations

• scientific article; zbMATH DE number 1341607
• Presburger Modal Logic Is PSPACE-Complete
• Graded computation tree logic
• scientific article; zbMATH DE number 487145
• A tableau method for graded intersections of modalities: A case for concept languages

Cited in

(29)

• CTL^ with graded path modalities
• Answering regular path queries in expressive description logics via alternating tree-automata
• Model-checking graded computation-tree logic with finite path semantics
• A tableau decision procedure for \(\mathcal{SHOIQ}\)
• Reasoning in description logics by a reduction to disjunctive datalog
• Complexity of modal logics with Presburger constraints
• A finite model construction for coalgebraic modal logic
• PSPACE bounds for rank-1 modal logics
• Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra
• PS\textsc{pace} tableau algorithms for acyclic modalized \({\mathcal{ALC}}\)
• CTL Model-Checking with Graded Quantifiers
• Presburger Modal Logic Is PSPACE-Complete
• scientific article; zbMATH DE number 1341607 (Why is no real title available?)
• Comparative study of variable precision rough set model and graded rough set model
• scientific article; zbMATH DE number 7577569 (Why is no real title available?)
• On the Computational Complexity of the Numerically Definite Syllogistic and Related Logics
• Using tableau to decide description logics with full role negation and identity
• scientific article; zbMATH DE number 5046366 (Why is no real title available?)
• On Composing Finite Forests with Modal Logics
• A description logic based situation calculus
• Completing the Picture: Complexity of Graded Modal Logics with Converse
• COUNTING TO INFINITY: GRADED MODAL LOGIC WITH AN INFINITY DIAMOND
• Concrete domains meet expressive cardinality restrictions in description logics
• Are targeted messages more effective?
• \({\mathcal E}\)-connections of abstract description systems
• Decidability of SHIQ with complex role inclusion axioms
• Conceptual logic programs
• A resolution-based decision procedure for \({\mathcal{SHOIQ}}\).
• Data complexity of query answering in expressive description logics via tableaux

This page was built for publication: PSpace reasoning for graded modal logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2720401)