A Set-theoretic Approach to Reasoning Services for the Description Logic DL4,xD

• Autorzy: Cantone Domenico , Nicolosi-Asmundo Marianna , Santamaria Daniele Francesco

Identyfikatory

DOI

10.3233/FI-2020-1977

• Języki publikacji: EN

Abstrakty

EN

In this paper we consider the most common TBox and ABox reasoning services for the description logic 𝒟ℒ〈4LQS^R,x 〉(D) (𝒟 ℒ_D ^4,×, for short) and prove their decidability via a reduction to the satisfiability problem for the set-theoretic fragment 4LQS^R. 𝒟 ℒ_D^4,× is a very expressive description logic. It combines the high scalability and efficiency of rule languages such as the Semantic Web Rule Language (SWRL) with the expressivity of description logics. In fact, among other features, it supports Boolean operations on concepts and roles, role constructs such as the product of concepts and role chains on the left-hand side of inclusion axioms, role properties such as transitivity, symmetry, reflexivity, and irreflexivity, and data types. We further provide a KE-tableau-based procedure that allows one to reason on the main TBox and ABox reasoning tasks for the description logic 𝒟 ℒ _D^4,× . 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 γ-rule. The novel system, called KE^γ -tableau, turns out to be an improvement of the system introduced in [1] and of standard first-order KE-tableaux [2]. Suitable benchmark test sets executed on C++ implementations of the three mentioned systems show that in several cases the performances of the KE^γ -tableau-based reasoner are up to about 400% better than the ones of the other two systems.

Słowa kluczowe

EN

description logics; algorithms; scalability; self-expression; C++

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 176, nr 3/4
• Strony: 349--384
• Opis fizyczny: Bibliogr. 28 poz., rys., tab., wykr.

Twórcy

autor

Cantone Domenico

• Department of Mathematics and Computer Science, University of Catania, Italy

autor

Nicolosi-Asmundo Marianna

• Department of Mathematics and Computer Science, University of Catania, Italy

autor

Santamaria Daniele Francesco

• Department of Mathematics and Computer Science, University of Catania, Italy

Bibliografia

• [1] Cantone D, Nicolosi-Asmundo M, Santamaria DF. A set-theoretic approach to ABox reasoning services. In: Costantini S, Franconi E, Van Woensel W, Kontchakovm R, Sadri F, Roman D (eds.), Rules and Reasoning. RuleML+RR 2017, volume 10364 of Lecture Notes in Computer Science. Springer, 2017 pp.87-102. doi:10.1007/978-3-319-61252-2_7.
• [2] D’Agostino M, Mondadori M. The taming of the cut. Classical refutations with analytic cut. Journal of Logic and Computation, 1994. 4:285-319. doi:10.1093/logcom/4.3.285.
• [3] Cantone D, Ferro A, Omodeo EG. Computable set theory. Number 6 in International Series of Monographs on Computer Science, Oxford Science Publications. Clarendon Press, Oxford, UK, 1989. ISBN:978-0198538073.
• [4] Cantone D, Omodeo E, Policriti A. Set theory for computing: from decision procedures to declarative programming with sets. Monographs in Computer Science. Springer-Verlag, New York, NY, USA, 2001. doi:10.1007/978-1-4757-3452-2.
• [5] Schwartz JT, Cantone D, Omodeo EG. Computational Logic and Set Theory: Applying Formalized Logic to Analysis. Texts in Computer Science. Springer-Verlag New York, Inc., 2011. ISBN:978-0-85729-807-2. doi:10.1007/978-0-85729-808-9.
• [6] Cantone D, Ursino P. An Introduction to the Technique of Formative Processes in Set Theory. Springer International Publishing, 2018. ISBN:978-3-319-74778-1.
• [7] Cantone D, Nicolosi-Asmundo M. On the satisfiability problem for a 4-level quantified syllogistic and some applications to modal logic. Fundamenta Informaticae, 2013. 124(4):427-448. doi:10.3233/FI-2013-842.
• [8] Cantone D, Nicolosi-Asmundo M, Santamaria DF. In: Proc. of ICTCS 2016, Lecce, September 7-9, CEUR Workshop Proceedings, volume 1720 pp. 23-35. ISSN:1613-0073.
• [9] Schaub T, Thielscher M. Skeptical query-answering in Constrained Default Logic. In: Gabbay DM, Ohlbach HJ (eds.), Practical Reasoning. Springer Berlin Heidelberg. ISBN:978-3-540-68454-1, 1996 pp.567-581.
• [10] D’Agostino M. Tableau Methods for Classical Propositional Logic. In: D’Agostino M, Gabbay D, Hähnle R, Posegga J (eds.), Handbook of Tableau Methods, pp. 45-123. Springer 1999. ISBN:978-0-7923-5627-1.
• [11] Cantone D, Nicolosi-Asmundo M, Santamaria DF. A C++ reasoner for the description logic DL4,xD. In: Proceedings of CILC 2017, 26-29 September 2017, Naples, Italy. CEUR Workshop Proceedings, ISSN:1613-0073, vol. 1949. 2017 pp. 276-280. URL http://ceur-ws.org/Vol-1949/CILCpaper03.pdf.
• [12] Cantone D, Nicolosi-Asmundo M, Santamaria DF. A set-based reasoner for the description logic DL4,xD. In: Proc. of SETS 2018 , Southampton, United Kingdom, 5 June 2018. CEUR Workshop Proceedings, volume 2199. 2018 pp. 52-66. ISSN:1613-0073. URL http://ceur-ws.org/Vol-2199/paper5.pdf.
• [13] Dershowitz N, Jouannaud J. Rewrite Systems. In: van Leeuwen J (ed.), Handbook of Theoretical Computer Science (Vol. B), pp. 243-320. MIT Press, Cambridge, MA, USA. 1999. ISBN:0-444-88074-7.
• [14] Cantone D, Longo C, Nicolosi-Asmundo M, Santamaria DF. Web Ontology Representation and Reasoning via Fragments of Set Theory. In: Cate B., Mileo A. (eds) Web Reasoning and Rule Systems. RR 2015. Lecture Notes in Computer Science, vol 9209. Springer, Cham (2015). 2015 pp. 61-76. doi:10.1007/978-3-319-22002-4_6.
• [15] Formisano A, Omodeo EG, Policriti A. Three-variable statements of set-pairing. Theoretical Computer Science, 2004. 322(1):147-173. doi:10.1016/j.tcs.2004.03.028.
• [16] Motik B, Horrocks I. OWL Datatypes: Design and Implementation. In: Proc. of the 7th Int. Semantic Web Conference (ISWC 2008), volume 5318 of LNCS. Springer, 2008 pp. 307-322. doi:10.1007/978-3-540-88564-1_20.
• [17] Horrocks I, Kutz O, Sattler U. The Even More Irresistible SROIQ. In: Proc. 10th Int. Conf. on Princ. of Knowledge Representation and Reasoning, (Doherty, P. and Mylopoulos, J. and Welty, C. A., eds.). AAAI Press, 2006 pp. 57-67. URL https://www.aaai.org/Papers/KR/2006/KR06-009.pdf.
• [18] Krötzsch M. OWL 2 Profiles: An Introduction to Lightweight Ontology Languages. In: Eiter T, Krennwallner T (eds.), Reasoning Web. Semantic Technologies for Advanced Query Answering: 8th International Summer School 2012, Vienna, Austria, September 3-8, 2012. Proceedings, pp. 112-183. Springer Berlin Heidelberg, Berlin, Heidelberg 2012. ISBN:978-3-642-33158-9.
• [19] Cantone D, Nicolosi-Asmundo M, Santamaria DF. Conjunctive Query Answering via a Fragment of Set Theory. CoRR, 2016. abs/1606.07337. Extended version, URL http://arxiv.org/abs/1606.07337.
• [20] Smullyan RM. First-order Logic. Dover books on advanced Math. Dover, 1995. ISBN:9780486683706.
• [21] Cantone D, Nicolosi-Asmundo M, Santamaria DF. A set-theoretic approach to ABox reasoning services. CoRR, 2017. 1702.03096. Extended version, URL http://arxiv.org/abs/1702.03096.
• [22] Ortiz M, Sebastian R, Šimkus M. Query Answering in the Horn Fragments of the Description Logics SHOIQ and SROIQ. In: Proc. of the 22th Int. Joint Conf. on Artificial Intell. - Vol. Two, IJCAI’11. AAAI Press 2011 pp. 1039-1044. ISBN:978-1-57735-514-4.
• [23] Cantone D, Nicolosi-Asmundo M, Santamaria DF, Trapani F. Ontoceramic: an OWL ontology for ceramics classification. In: Proc. of CILC 2015, CEUR Workshop Proceedings, ISSN 1613-0073, vol. 1459. 2015 pp. 122-127. URL http://ceur-ws.org/Vol-1459/paper5.pdf.
• [24] Cantale C, Cantone D, Nicolosi-Asmundo M, Santamaria DF. Distant Reading Through Ontologies: The Case Study of Catania’s Benedictines Monastery. In Italian Journal of Library, Archives, and Information Science (JLIS.it), 8,3 (September 2017), 2017. doi:http://dx.doi.org/10.4403/jlis.it-12342.
• [25] Motik B. On the Properties of Metamodeling in OWL. In: 4th Int. Semantic Web Conf. ISWC 2005. 2005 pp. 548-562. doi:10.1093/logcom/exm027.
• [26] Glimm B, Horrocks I, Motik B, Stoilos G, Wang Z. Hermi T: An OWL 2 Reasoner. Journal of Automated Reasoning, 2014. 53(3):245-269. doi:10.1007/s10817-014-9305-1.
• [27] Sirin E, Parsia B, Grau BC, Kalyanpur A, Katz Y. Pellet: A practical OWL-DL reasoner. J. Web Sem., 2007. 5(2):51-53. doi:10.1016/j.websem.2007.03.004.
• [28] World Wide Web Consortium. OWL 2 Web Ontology Language Structural Specification and Functional-Style Syntax (Second Edition). URL https://www.w3.org/2007/OWL/draft/ED-owl2-syntax-20081128/.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).