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