Abstract
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. This establishes a kind of “theoretical benchmark” that all algorithmic approaches can be measured with.
This work was supported by the DFG, Project No. GR 1324/3-1
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Y. André, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217–274, 1998.
F. Baader, M. Buchheit, and B. Hollunder. Cardinality restrictions on concepts. Artificial Intelligence, 88(1-2):195–213, 1996.
D. Calvanese, M. Lenzerini, and D. Nardi. A Unified Framework for Class Based Representation Formalisms. Proc. of KR-94, 1994.
W. Van der Hoek, and M. De Rijke. Counting objects. Journal of Logic and Computation, 5(3):325–345, June 1995.
F. M. Donini, M. Lenzerini, D. Nardi, and W. Nutt. The complexity of concept languages.. Information and Computation, 134(1):1–58, 10 April 1997.
K. Fine. In so many possible worlds. Notre Dame Journal of Formal Logic, 13:516–520, 1972.
F. Giunchiglia and R. Sebastiani. Building decision procedures for modallogics from propositional decision procedures—the case study of modal K.. Proc. of CADE-13, LNCS 1104. Springer, 1996.
B. Hollunder and F. Baader. Qualifying number restrictions in concept languages. In Proc. of KR-91, pages 335–346, Boston (USA) 1991.
J. Y. Halpern and Y. Moses. A guide to completeness and complexity for model logics of knowledge and belief. Artificial Intelligence 54(3):319–379, April 1992.
U. Hustadt and R. A. Schmidt. On evaluating decision procedures for modal logic. In Proc. of IJCAI-97, volume 1, pages 202–207, 1997.
R. E. Ladner. The computational complexity of provability in systems of modal propositional logic. SIAM Journal on Computing,, 6(3):467–480, September 1977.
H. J. Ohlbach and R. A. Schmidt. Functional translation and second-order frame properties of modal logics. Journal of Logic and Computation, 7(5):581–603, October 1997.
H. J. Ohlbach, R. A. Schmidt, and U. Hustadt. Translating graded modalities into predicate logic.. In H. Wansing, editor, Proof Theory of Modal Logic volume 2 of Applied Logic Series, pages 253–291. Kluwer, 1996.
W. J. Savitch. Relationships between nondeterministic and deterministic tape complexities. Journal of Computer and System Sciences, 4(2):177–192, April 1970.
K. Schild. A correspondence theory for terminological logics: Preliminary report. In Proc. of IJCAI-91,, pages 466–471, 1991.
R. A. Schmidt. Resolution is a decision procedure for many propositional modal logics: Extended abstract. In M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, editors, Advances in Modal Logic ’96. CLSI Publications, 1997.
M. Schmidt-Schauß and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48:1–26, 1991.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Tobies, S. (1999). A PSpace Algorithm for Graded Modal Logic. In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_4
Download citation
DOI: https://doi.org/10.1007/3-540-48660-7_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66222-8
Online ISBN: 978-3-540-48660-2
eBook Packages: Springer Book Archive