Abstract
We present a KE-tableau-based procedure for the main TBox and ABox reasoning tasks for the description logic \(\mathcal {DL}\langle \mathsf {4LQS^{R,\!\times }}\rangle (\mathbf {D})\), in short \(\mathcal {DL}_{\mathbf {D}}^{4,\!\times }\). The logic \(\mathcal {DL}_{\mathbf {D}}^{4,\!\times }\), representable in the decidable multi-sorted quantified set-theoretic fragment \(\mathsf {4LQS^R}\), combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics.
Our algorithm is based on a variant of the KE-tableau system for sets of universally quantified clauses, where the KE-elimination rule is generalized in such a way as to incorporate the \(\gamma \)-rule. The novel system, called KE\(^{\mathbf {\gamma }}\)-tableau, turns out to improve both the system introduced in [3] and the standard first-order KE-tableaux [10]. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that the performances of the KE\(^{\mathbf {\gamma }}\)-tableau-based reasoner are often up to about 400% better than the ones of the other two systems. This a first step towards the construction of efficient reasoners for expressive OWL ontologies based on fragments of computable set theory.
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
Notes
- 1.
The source code is available at https://github.com/dfsantamaria/DL4xD-Reasoner.
- 2.
A separate analysis, to be addressed in a future work, is required by the classification problem of a TBox, consisting in the computation of ancestor and descendant concepts of a given concept in a TBox.
- 3.
- 4.
The procedures \(\textit{Consistency-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}\) and \(\textit{HOCQA}^\gamma \textit{-}{\mathcal {DL}_{\mathbf {D}}^{4,\!\times }}\) can be found in [5] together with their correctness, completeness, and termination proofs.
References
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., Santamaria, D.F.: Conjunctive query answering via a fragment of set theory. In: Proceedings of ICTCS 2016, Lecce, 7–9 September, vol. 1720, pp. 23–35. CEUR-WS (2016)
Cantone, D., Nicolosi-Asmundo, M., Santamaria, D.F.: A set-theoretic approach to abox reasoning services. In: Costantini, S., Franconi, E., Van Woensel, W., Kontchakov, R., Sadri, F., Roman, D. (eds.) RuleML+RR 2017. LNCS, vol. 10364, pp. 87–102. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-61252-2_7
Cantone, D., Nicolosi-Asmundo, M., Santamaria, D.F.: A C++ reasoner for the description logic \(\cal{DL}_{{\mathbf{D}}}^{4,\!\times }\). In: Proceedings of CILC 2017, Naples, Italy, 26–29 September 2017, vol. 1949, pp. 276–280. CEUR WS (2017). ISSN 1613-0073
Cantone, D., Nicolosi-Asmundo, M., Santamaria, D.F.: An optimized KE-tableau-based system for reasoning in the description logic \(\cal{DL}_{{\mathbf{D}}}^{4,\!\times }\). CoRR, 1804.11222 (2018). Extended version
Glimm, B., Horrocks, I., Motik, B., Stoilos, G., Wang, Z.: HermiT: an OWL 2 reasoner. J. Autom. Reason. 53(3), 245–269 (2014)
Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Doherty, P., Mylopoulos, J., Welty, C.A. (eds.) Proceedings of 10th International Conference on Principle of Knowledge Representation and Reasoning, pp. 57–67. AAAI Press (2006)
Krötzsch, M.: OWL 2 profiles: an introduction to lightweight ontology languages. In: Eiter, T., Krennwallner, T. (eds.) Reasoning Web 2012. LNCS, vol. 7487, pp. 112–183. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33158-9_4
Cristiá, M., Rossi, G.: A decision procedure for restricted intensional sets. In: de Moura, L. (ed.) CADE 2017. LNCS, vol. 10395, pp. 185–201. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_12
Mondadori, M., D’Agostino, M.: The taming of the cut. Classical refutations with analytic cut. J. Logic Comput. 4, 285–319 (1994)
Motik, B., Horrocks, I.: OWL datatypes: design and implementation. In: Sheth, A., et al. (eds.) ISWC 2008. LNCS, vol. 5318, pp. 307–322. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88564-1_20
Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: a practical OWL-DL reasoner. J. Web Semant. 5(2), 51–53 (2007)
Smullyan, R.M.: First-order Logic. Dover Books on Advanced Mathematics. Dover, New York (1995)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Cantone, D., Nicolosi-Asmundo, M., Santamaria, D.F. (2018). An Optimized KE-Tableau-Based System for Reasoning in the Description Logic \({\mathcal {DL}}_{{\mathbf {D}}}^{4,\!\times }\). In: Benzmüller, C., Ricca, F., Parent, X., Roman, D. (eds) Rules and Reasoning. RuleML+RR 2018. Lecture Notes in Computer Science(), vol 11092. Springer, Cham. https://doi.org/10.1007/978-3-319-99906-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-99906-7_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99905-0
Online ISBN: 978-3-319-99906-7
eBook Packages: Computer ScienceComputer Science (R0)