PSPACE Reasoning for Graded Modal Logics

We present a PSPACE algorithm that decides satisfiability of the graded modal logic Gr(KR)—a natural extension of propositional modal logic KR by counting expressions—which plays an important role in the area of knowledge representation. The algorithm employs a tableaux approach and is the first kno...

Full description

Saved in:
Bibliographic Details
Published in:Journal of logic and computation 2001-02, Vol.11 (1), p.85-106
Main Author: Tobies, S.
Format: Article
Language:English
Subjects:
complexity
counting
description logic
graded modalities
Modal logic
Citations: Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present a PSPACE algorithm that decides satisfiability of the graded modal logic Gr(KR)—a natural extension of propositional modal logic KR 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∩−1, which augments Gr(KR) with inverse relations and intersection of accessibility relations. This establishes a kind of ‘theoretical benchmark’ that all algorithmic approaches can be measured against.
ISSN:0955-792X
1465-363X
DOI:10.1093/logcom/11.1.85