© 2001 by Oxford University Press
| ||||||||||||||||||||||||||||||||||||||||||||||||||
PSPACE Reasoning for Graded Modal Logics
1 LuFg Theoretical Computer Science, RWTH Aachen, Theoretische Informatik, Ahornstr. 55, D-52074 Aachen, Germany. E-mail: tobies{at}informatik.rwth-aachen.de
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
expressionswhich 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.
Keywords: Modal logic; graded modalities; counting; description logic; complexity
Accepted 15 October 1999.