Abstract
In this paper we consider the most common ABox reasoning services for the description logic \(\mathcal {DL}\langle \mathsf {4LQS}^{\mathsf{R},\!\times }\rangle (\mathbf {D})\) (\(\mathcal {DL}_{\mathbf {D}}^{4,\!\times }\), for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment \(\mathsf {4LQS^R}\). The description logic \(\mathcal {DL}_{\mathbf {D}}^{4,\!\times }\) is very expressive, as it admits various concept and role constructs and data types that allow one to represent rule-based languages such as SWRL.
Decidability results are achieved by defining a generalization of the conjunctive query answering (CQA) problem that can be instantiated to the most widespread ABox reasoning tasks. We also present a KE-tableau based procedure for calculating the answer set from \(\mathcal {DL}_{\mathbf {D}}^{4,\!\times }\)-knowledge bases and higher order \(\mathcal {DL}_{\mathbf {D}}^{4,\!\times }\)-conjunctive queries, thus providing means for reasoning on several well-known ABox reasoning tasks. Our calculus extends a previously introduced KE-tableau based decision procedure for the CQA problem.
This work has been partially supported by the Polish National Science Centre research project DEC-2011/02/A/HS1/00395.
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
Similar content being viewed by others
Notes
- 1.
Definitions of positive and of negative occurrences of a formula within another formula can be found in [4].
- 2.
The map \(\theta \) coincides with the transformation function defined in [7] as far as it concerns the translation of each axiom or assertion H of \(\mathcal {KB}\) in a \(\mathsf {4LQS^R}\)-formula \(\theta (H)\). The map \(\theta \) extends the function introduced in [7] for what regards the translation of the HO query Q and of the substitutions \(\sigma \) of the HO answer set \(\varSigma \). In particular it maps effectively variables in \(\mathsf {V}_{\mathsf {c}}\) in variables of sort 1 (in the language of \(\mathsf {4LQS^R}\)), and variables in \(\mathsf {V}_{\mathsf {ar}}\) and in \(\mathsf {V}_{\mathsf {cr}}\) in variables of sort 3. The constraints \(\xi _1\)–\(\xi _{12}\) are added to make sure that each \(\mathsf {4LQS^R}\)-model of \(\phi _{\mathcal {KB}}\) can be transformed into a \(\mathcal {DL}_{\mathbf {D}}^{4,\!\times }\)-interpretation (cf. [7, Theorem 1]).
References
Calvanese, D., De Giacomo, G., Lenzerini, M.: On the decidability of query containment under constraints. In: PODS, pp. 149–158 (1998)
Calvanese, D., De Giacomo, G., Lenzerini, M.: Conjunctive query containment and answering under description logic constraints. ACM Trans. Comput. Log. 9(3), 22:1–31 (2008)
Cantone, D., Longo, C., Nicolosi-Asmundo, M., Santamaria, D.F.: Web ontology representation and reasoning via fragments of set theory. In: Cate, B., Mileo, A. (eds.) RR 2015. LNCS, vol. 9209, pp. 61–76. Springer, Cham (2015). doi:10.1007/978-3-319-22002-4_6
Cantone, D., Nicolosi-Asmundo, M.: On the satisfiability problem for a 4-level quantified syllogistic and some applications to modal logic. Fundamenta Informaticae 124(4), 427–448 (2013)
Cantone, D., Nicolosi-Asmundo, M., Orłowska, E.: Dual tableau-based decision procedures for some relational logics. In: Proceedings of the 25th Italian Conference on Computational Logic, CEUR-WS, vol. 598, Rende, Italy, 7–9 July 2010 (2010)
Cantone, D., Nicolosi-Asmundo, M., Orłowska, E.: Dual tableau-based decision procedures for relational logics with restricted composition operator. J. Appl. Non-Classical Logics 21(2), 177–200 (2011)
Cantone, D., Nicolosi-Asmundo, M., Santamaria, D.F.: Conjunctive query answering via a fragment of set theory. In: Proceedings of ICTCS 2016, CEUR-WS, Lecce, 7–9 September, vol. 1720, pp. 23–35 (2016)
Cantone, D., Nicolosi-Asmundo, M., Santamaria, D.F.: A set-theoretic approach to ABox reasoning services. CoRR, 1702.03096 (2017). Extended version
Cantone, D., Nicolosi-Asmundo, M., Santamaria, D.F., Trapani, F.: Ontoceramic: an OWL ontology for ceramics classification. In Proceedings of CILC 2015, CEUR-WS, vol. 1459, pp. 122–127, Genova, 1–3 July 2015
D’Agostino, M.: Tableau methods for classical propositional logic. In: D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 45–123. Springer (1999)
Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible \(\cal{SROIQ}\). In: Proceedings of the 10th International Conference on Principles of Knowledge Representation and Reasoning, pp. 57–67. AAAI Press (2006)
Motik, B., Horrocks, I.: OWL datatypes: design and implementation. In: Sheth, A., Staab, S., Dean, M., Paolucci, M., Maynard, D., Finin, T., Thirunarayan, K. (eds.) ISWC 2008. LNCS, vol. 5318, pp. 307–322. Springer, Heidelberg (2008). doi:10.1007/978-3-540-88564-1_20
Ortiz, M., Sebastian, R., Šimkus, M.: Query answering in the Horn fragments of the description logics \(\cal{SHOIQ}\) and \(\cal{SROIQ}\). In: Proceedings of the 22th International Joint Conference on Artificial Intelligence, IJCAI 2011, vol. 2, pp. 1039–1044. AAAI Press (2011)
Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Cantone, D., Nicolosi-Asmundo, M., Santamaria, D.F. (2017). A Set-Theoretic Approach to ABox Reasoning Services. In: Costantini, S., Franconi, E., Van Woensel, W., Kontchakov, R., Sadri, F., Roman, D. (eds) Rules and Reasoning. RuleML+RR 2017. Lecture Notes in Computer Science(), vol 10364. Springer, Cham. https://doi.org/10.1007/978-3-319-61252-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-61252-2_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-61251-5
Online ISBN: 978-3-319-61252-2
eBook Packages: Computer ScienceComputer Science (R0)