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

Details
Bibtex

KurzfassungAbstract
We present a PSPACE algorithm that decides satisfiability of the graded modal 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},

} }}