×

PSpace tableau algorithms for acyclic modalized \({\mathcal{ALC}}\). (English) Zbl 1291.68387

Summary: We study \(\mathcal{ALCK}_m\) and \(\mathcal{ALCS}4_m\), which extend the description logic \(\mathcal{ALC}\) by adding modal operators of the basic multi-modal logics \(\mathrm{K} _{m }\) and \(\mathrm{S4}_{m }\). We develop a sound and complete tableau algorithm \(\Lambda_\mathcal{K}\) for answering \(\mathcal{ALCK}_m\) queries w.r.t. an \(\mathcal{ALCK}_m\) knowledge base with an acyclic TBox. Defining tableau expansion rules in the presence of acyclic definitions by considering only the concept names on the left-hand side of TBox definitions or their negations, allows us to give a PSPACE implementation for \(\Lambda_\mathcal{K}\). We then consider answering \(\mathcal{ALCS}4_m\) queries w.r.t. an \(\mathcal{ALCS}4_m\) knowledge base (with an acyclic TBox) in which the epistemic operators correspond to those of classical multi-modal logic \(\mathrm{S4}_{m }\). The expansion rules in the tableau algorithm \(\Lambda _{\mathrm{S4}}\) are designed to syntactically incorporate the epistemic properties. Blocking is corporated into the tableau expansion rules to ensure termination. We also provide a PSPACE implementation for \(\Lambda _{\mathrm{S4}}\). In light of the fact that the satisfiability problem for \(\mathcal{ALCK}_m\) with general TBox and no epistemic properties (i.e., \(\mathbf{K}_{\mathcal{ALC}}\)) is NEXPTIME-complete, we conclude that both \(\mathcal{ALCK}_m\) and \(\mathcal{ALCS}4_m\) offer computationally manageable and practically useful fragments of \(\mathbf{K}_{\mathcal{ALC}}\).

MSC:

68T27 Logic in artificial intelligence
03B42 Logics of knowledge and belief (including belief change)
03B35 Mechanization of proofs and logical operations
68Q25 Analysis of algorithms and problem complexity
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

KL-ONE
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003) · Zbl 1058.68107
[2] Schmidt-Schauß, M., Smolka, G.: Attributive concept descriptions with complements. Artif. Intell. 48(1), 1–26 (1991) · Zbl 0712.68095
[3] Calvanese, D., De Giacomo, G., Lenzerini, M., Nardi, D.: Reasoning in expressive description logics. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1581–1634. Elsevier and MIT Press (2001) · Zbl 0992.03036
[4] Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Stud. Log. 69(1), 5–40 (2001) · Zbl 0991.03012 · doi:10.1023/A:1013882326814
[5] Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive description logics. Log. J. IGPL 8(3), 239–264 (2000) · Zbl 0967.03026 · doi:10.1093/jigpal/8.3.239
[6] Horrocks, I.: Daml+oil: a description logic for the semantic web. IEEE Data Eng. Bull. 25(1), 4–9 (2002) · Zbl 1054.68785
[7] Horrocks, I., Patel-Schneider, P.F., van Harmelen, F.: From shiq and rdf to owl: the making of a web ontology language. J. Web Sem. 1(1), 7–26 (2003) · Zbl 05461265 · doi:10.1016/j.websem.2003.07.001
[8] Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995) · Zbl 0839.68095
[9] Meyer, J.-J.C., Van Der Hoek, W.: Epistemic Logic for AI and Computer Science. Cambridge University Press, Cambridge (2004) · Zbl 0868.03001
[10] Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol. 3. Elsevier Science Inc., New York, NY, USA (2006) · Zbl 1114.03001
[11] Rosati, R.: On the semantics of epistemic description logics. In: Padgham, L., Franconi, E., Gehrke, M., McGuinness, D.L., Patel-Schneider, P.F. (eds.) Description Logics. AAAI Technical Report, vol. WS-96-05, pp. 185–188. AAAI Press (1996)
[12] Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Epistemic first-order queries over description logic knowledge bases. In: Proc. of the 2006 Description Logic Workshop (DL 2006). CEUR (2006)
[13] Donini, F.M., Lenzerini, M., Nardi, D., Schaerf, A., Nutt, W.: Adding epistemic operators to concept languages. In: KR, pp. 342–353 (1992) · Zbl 0906.68144
[14] Donini, F.M., Lenzerini, M., Nardi, D, Nutt, W., Schaerf, A.: An epistemic operator for description logics. Artif. Intell. 100(1–2), 225–274 (1998) · Zbl 0906.68144 · doi:10.1016/S0004-3702(98)00009-5
[15] Baader, F., Laux, A.: Terminological logics with modal operators. In: IJCAI (1), pp. 808–815 (1995)
[16] Lutz, C., Sturm, H., Wolter, F., Zakharyaschev, M.: A tableau decision algorithm for modalized $\(\backslash\)mathcal{ALC}$ with constant domains. Stud. Log. 72(2), 199–232 (2002) · Zbl 1010.03012 · doi:10.1023/A:1021308527417
[17] Baader, F., Ohlbach, H.J.: A multi-dimensional terminological knowledge representation language. J. Appl. Non-Class. Log. 5(2), 153–197 (1995) · Zbl 0845.68098 · doi:10.1080/11663081.1995.10510854
[18] Mosurovic, M., Zakharyaschev, M.: On the complexity of description logics with modal operators. In: Koletsos, G., Kolaitis, P.G. (eds.) 2nd PLS, pp. 166–171 (1999)
[19] Wolter, F., Zakharyaschev, M.: Multi-dimensional description logics. In: Dean, T. (ed.) IJCAI, pp. 104–109. Morgan Kaufmann, San Mateo (1999) · Zbl 0951.03011
[20] Wolter, F., Zakharyaschev, M.: Satisfiability problem in description logics with modal operators. In: KR, pp. 512–523 (1998)
[21] Wolter, F., Zakharyaschev, M.: Dynamic description logics. In: Zakharyaschev, M., Segerberg, K., de Rijke, M., Wansing, H. (eds.) Advances in Modal Logic, pp. 431–446. CSLI Publications (1998) · Zbl 0993.03043
[22] Wolter, F., Zakharyaschev, M.: Modal description logics: modalizing roles. Fundam. Inform. 39(4), 411–438 (1999) · Zbl 0951.03011
[23] Wolter, F., Zakharyaschev, M.: Decidable fragments of first-order modal logics. J. Symb. Log. 66(3), 1415–1438 (2001) · Zbl 0996.03010 · doi:10.2307/2695115
[24] Donini, F.M., Nardi, D, Rosati, R.: Description logics of minimal knowledge and negation as failure. ACM Trans. Comput. Log. (TOCL) 3(2), 225 (2002) · Zbl 1365.68403
[25] Tobies, S.: Complexity results and practical algorithms for logics in knowledge representation. CoRR. cs.LO/0106031 (2001) · Zbl 0992.03028
[26] Buchheit, M., Donini, F.M., Schaerf, A.: Decidable reasoning in terminological knowledge representation systems. J. Artif. Intell. Res. (JAIR) 1, 109–138 (1993) · Zbl 0900.68396
[27] Hladik, J., Peñaloza, R.: PSPACE automata for description logics. In: 2006 International Workshop on Description Logics DL’06, p. 74 (2006) · Zbl 1149.68073
[28] Baader, F., Nutt, W.: Basic description logics. In: Baader et al. (eds.) The Description Logic Handbook: Theory, Implementation, and Applications, pp. 43–95. Cambridge University Press, Cambridge (2003)
[29] Horrocks, I., Hustadt, U., Sattler, U., Schmidt, R.: Computational modal logic. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic, chap. 4, pp. 181–245. Elsevier (2006)
[30] Lutz, C.: Complexity of terminological reasoning revisited. In: Ganzinger, H., McAllester, D.A., Voronkov, A. (eds.) LPAR. Lecture Notes in Computer Science, vol. 1705, pp. 181–200. Springer (1999) · Zbl 0949.03030
[31] Nebel, B.: Terminological reasoning is inherently intractable. Artif. Intell. 43(2), 235–249 (1990) · Zbl 0717.68089 · doi:10.1016/0004-3702(90)90087-G
[32] Vardi, M.Y.: A model-theoretic analysis of monotonic knowledge. In: Proc. Ninth International Joint Conference on Artificial Intelligence (IJCAI’85), pp. 509–512 (1985)
[33] Baader, F., Hladik, J., Peñaloza, R.: Automata can show PSPACE results for description logics. Inf. Comput. 206(9–10), 1045–1056 (2008) · Zbl 1149.68073 · doi:10.1016/j.ic.2008.03.006
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.