{PSPACE} Reasoning for Graded Modal Logics
Aus International Center for Computational Logic
{PSPACE} Reasoning for Graded Modal Logics
Stephan TobiesStephan Tobies

Stephan Tobies
{PSPACE} Reasoning for Graded Modal Logics
Journal of Logic and Computation, 11(1):85--106, 2001
{PSPACE} Reasoning for Graded Modal Logics
Journal of Logic and Computation, 11(1):85--106, 2001
- KurzfassungAbstract
We present a PSPACE algorithm that decides satisfiability of the gradedmodal 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
a EXPTIME-hardness conjecture. We extend the results to the logic Gr(K_{R_\cap^{-1
@article{T2001,
author = {Stephan Tobies},
title = {{PSPACE} Reasoning for Graded Modal Logics},
journal = {Journal of Logic and Computation},
volume = {11},
number = {1},
year = {2001},
pages = {85--106}
}
),
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.
|ISBN= |ISSN= |Link= |Download=Tobies-JLC-2001.ps.gz |Slides= |DOI Name= |Projekt= |Forschungsgruppe=Automatentheorie |BibTex=@article{ Tobies-JLC-2001,
author = {Stephan {Tobies} }, journal = {Journal of Logic and Computation}, number = {1}, pages = {85--106}, title = { {PSPACE} Reasoning for Graded Modal Logics}, volume = {11}, year = {2001},
}
}}