A PSpace Algorithm for Graded Modal Logic

From International Center for Computational Logic

"Juli~7--10," is not in the list (Januar, Februar, März, April, Mai, Juni, Juli, August, September, Oktober, ...) of allowed values for the "Month" property.

Toggle side column

A PSpace Algorithm for Graded Modal Logic

Stephan TobiesStephan Tobies
Stephan Tobies
A PSpace Algorithm for Graded Modal Logic
In H. Ganzinger, eds., Automated Deduction – CADE-16, 16th International Conference on Automated Deduction, LNAI 1632, 52-66,  1999. Springer
  • KurzfassungAbstract
    We present a PSPACE algorithm that decides satisfiability of the graded 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 fixe the complexity of the problem and refute a EXPTIME-hardness conjecture. This establishes a kind of ``theoretical benchmark that all algorithmic approaches can be measured with.
  • Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
The final publication is available at Springer.
@inproceedings{ Tobies-CADE-99,
  address = {Trento, Italy},
  author = {S. {Tobies}},
  booktitle = {Automated Deduction -- CADE-16, 16th International Conference on Automated Deduction},
  editor = {H. {Ganzinger}},
  month = {July~7--10,},
  pages = {52--66},
  publisher = {Springer-Verlag},
  series = {LNAI 1632},
  title = {A {PSpace} Algorithm for Graded Modal Logic},
  year = {1999},
}