PSpace reasoning for graded modal logics

DOI10.1093/LOGCOM/11.1.85zbMATH Open0992.03028arXivcs/0005009OpenAlexW1636976386MaRDI QIDQ2720401FDOQ2720401

Stephan Tobies

Publication date: 16 September 2002

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

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.

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

zbMATH Keywords

computational complexitydescription logicsatisfiabilitygraded modalitiesgraded modal logicPSpace algorithm

Mathematics Subject Classification ID

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

Cited In (25)

• PSPACE bounds for rank-1 modal logics
• Model-checking graded computation-tree logic with finite path semantics
• Title not available (Why is that?)
• CTL\(^\ast\) 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
• Using tableau to decide description logics with full role negation and identity
• A tableau decision procedure for \(\mathcal{SHOIQ}\)
• Complexity of modal logics with Presburger constraints
• A description logic based situation calculus
• Completing the Picture: Complexity of Graded Modal Logics with Converse
• Answering regular path queries in expressive description logics via alternating tree-automata
• Title not available (Why is that?)
• 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
• COUNTING TO INFINITY: GRADED MODAL LOGIC WITH AN INFINITY DIAMOND

   Recommendations

• Title not available (Why is that?) 👍 👎
• Presburger Modal Logic Is PSPACE-Complete 👍 👎
• Graded computation tree logic 👍 👎
• Title not available (Why is that?) 👍 👎
• A tableau method for graded intersections of modalities: A case for concept languages 👍 👎

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)