Home  Online Resources  Table of Contents

Journal of Logic and Computation, Volume 11, Issue 1, pp. 85-106: Abstract.

PSPACE Reasoning for Graded Modal Logics

Stephan Tobies

LuFg Theoretical Computer Science, RWTH Aachen, Theoretische Informatik, Ahornstr. 55, D-52074 Aachen, Germany. E-mail: tobies@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 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(KR[cap][minus]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

  Full-Text PDF  (235 KB)

[ Oxford University Press]   [ Oxford Journals]   [ Comments & Feedback]   Copyright© Oxford University Press, 2001.