S ROI Q Syntax Approximation by Using Nominal Schemas

Abstract

Nominal schemas is a recently introduced extension of description logics which makes it possible to express rules which generalize DL-safe ones. A tractable description logic, ELROVn, has been identied. This leads us to the question: can we improve approximate reasoning results by employing nominal schemas? In this paper, we investigate how to approximately cast SROIQ into ELROVn. Using a datalog-based tractable algorithm, a preliminary evaluation shows that our approach can indeed do approximate SROIQ-reasoning with a high recall.

Introduction

Reasoning with large or complex terminology is computationally di cult and is one of the bottlenecks for Semantic Web applications. Most reasoning tasks for ontologies underlying OWL [11] are intractable. Even with small ontologies, sound and complete reasoning is practically infeasible, in particular for applications where quick responses are critical.

This fundamental insight that expressive ontology reasoning is often necessarily of high computational complexity has triggered a line of research which aims at utilizing approximate algorithms, i.e. algorithms which are (provably) not sound and complete, but which nevertheless provide answers which are good enough for practical purposes [ 6,9,10,24 ]. This general idea of approximate reasoning is not new and to a certain extent had been studied already before the advent of the Semantic Web [ 4,25,26 ]. But the Semantic Web e ort with its increased requirements for scalability has recently put this into a focus which this branch of reasoning research has never had before [ 7,8,12,20,21,22,23,27 ].

One of the prominent general approaches to approximate reasoning is known as language weakening. Language weakening refers to the idea of rewriting a knowledge base into a language which can be handled more e ciently. Obviously, if the target language has a lower complexity class, this rewriting in general cannot be done without a loss, resulting in an approximate reasoning procedure. In order to limit loss in the translation, it is of advantage if the target language be as expressive as possible while still being of low computational complexity, and hence languages which push expressivity while retaining tractability are natural choices for a language weakening approach.

In this paper, we use E LROV n for approximate reasoning over SROIQ++usi[n2]g, language weakening. E LROV n is essentially a tractable extension of E L a.k.a. OWL 2 EL [18], by nominal schemas [17].1 As such, E LROVn incorporates DL-safe Datalog under Herbrand semantics [14]. We have recently described an e cient procedure to reasoning with E LROVn [ 5 ] on which we base the evaluations in this paper.

The plan of this paper is as follows. In Section 2 we recall the languages SROIQ and E LROVn. In Section 3 we describe our approximate compilation of SROIQ into E LROVn. In Section 4 we recall our E LROVn reasoning approach from [ 5 ]. In Section 5 we describe our implementation and evaluation results. In Section 6 we conclude. 2

Preliminaries

In this section, we introduce the description logics (DLs) SROIQ and E LROVn. The latter includes the new constructor from [17], nominal schemas, which we use to approximate some features of SROIQ.

A signature = h I ; C ; R; S i consists of mutually disjoint nite sets of atomic roles role names R, atomic concepts C , and individuals individual

I , together with a distinguished subset S R of simple atomic roles. The set of roles (over ) is R := R [ fR jR 2 Rg; the set of simple roles is S := S [ fS jS 2 S g. A role chain is an expression of the from R1 : : : Rn with n 1 and each Ri 2 R. The function inv( ) is de ned on roles by inv(R) := R and inv(R ) := R where R 2 R, and extended to role chains by inv(R1 : : : Rn) :=inv(Rn) : : : inv(R1).

The set C of SROIQ concepts (over ) is de ned recursively as follows: C :=

C jf I gjC u CjC t Cj:Cj9R:Cj8R:Cj nS:Cj nS:Cj9S:Self

A TBox is a nite set of general concept inclusions (GCIs) of the form C v D where C; D 2 C. A SROIQ TBox can be normalized such that it only contains the normal forms in Table 1 [ 1 ].

Satis ability checking of SROIQ ontologies is in N2ExpTime [13]. Given a disjunctive assertion (C t D)(s), the tableau algorithm [13] nondeterministically guesses that either C(s) or D(s) holds, which can give rise to exponential behavior. Although the absorption technique and the hypertableaux approach [19] reduce the cost of this nondeterminism, it is still a considerable performance bottleneck. 1 It was called SROELVn in [17].

SROIQ de nes simple roles and role regularity to ensure decidability [13]. However, since we will later approximately cast SROIQ into E LROV n, which is free of these restrictions, we do not have to concern ourselves with them for the purposes of this paper. E LROV n extends E L++ with nominal schemas (see [ 5,17 ] for details). To deal with the new constructor, we extend the signature to = h I ; C ; R; V i, where V is a set of variables. A nominal schema is a concept of the form fxg where x 2 V . Semantically, these variables can only bind to known individuals. The n in E LROV nis a global bound on the number of di erent nominal schemas which can occur in any axiom in a knowledge base| this restriction guarantees tractability. The set of C of E LROV n concepts is de ned as follows:

C :=

C jf I gjf V gjC u Cj9R:Cj9S:Self

To give an example, consider the rst-order rule

R1(x; y) ^ R2(y; z) ^ R3(x; z) ! R(x; z) which cannot be translated faithfully into SROIQ. By limiting the variable z in the sense that it can bind only to known individuals (such variables are called DL-safe [16]), we can express this rule in E LROV n as

9R1:9R2:fzg u 9R3:fzg v 9R:fzg: If a1; : : : ; ak are all the known individuals in the knowledge base, then this axiom can also be expressed using the k SROIQ-axoims

9R1:9R2:faig u 9R3:faig v 9R:faig where i ranges from 1 to k. This kind of conversion, called full or naive grounding, of nominal schemas into classical description logics is, however, computationally infeasible [ 5 ] even for E LROV n, which is of PTime complexity [17]. In [ 5 ], we thus presented a datalog-based algorithm for E LROV n which avoids full grounding, and have also shown experimentally that the algorithm is e cient. 3

Approximation

For our approximation of SROIQ by E LROV n, we use a number of di erent techniques, some of which are borrowed from existing literature. The key ideas are as follows.

{ We rewrite mincardinality restrictions into maxcardinality restrictions or approximate using an existential. { We rewrite universal quanti cation into existential quanti cation. { We approximate maxcardinality restrictions using functionality. { We approximate inverse roles and functionality using nominal schemas. { We approximate negation using class disjointness.

Algorithm 1 Approximation Algorithm { We approximate disjunction using conjunction.

A pseudocode description is given in Algorithm 1, we explain the relevant parts in more detail below. Role chain axioms are left untouched, as are axioms which can already directly be expressed in E LROV n. We drop the soundness proof, since one can easily nd out that our approach is sound but incomplete. 3.1

Approximation of Inverse Role and Functionality

Since E LROV n can express DL-safe Datalog rules, all rule-like axioms in SROIQ can be approximated easily in E LROV n.

For role inclusion axioms of the form R v S , the rst-order logic rule is R(x; y) ! S(y; x). By restricting the variables to nominals, we obtain nom(x) ^ nom(y) ^ R(x; y) ! S(y; x), where nom(x) is de ned by the collection of facts nom(ai) for each individual ai. The latter rule can be expressed by means of the nominal schema axiom,

fxg u 9R:fyg v fyg u 9S:fxg where x and y are nominal schemas. This axiom will be later translated into datalog rule,

nom(x); nom(y); triple(x; R; y) ! triple(y; S; x) where we can clearly see that the rule expresses the inverse role with restricting variable bounded to known individuals.

Similarly, for a functionality axiom C v 1R:D, we can cast it into

C u 9R:(fz1g u D) u 9R:(fz2g u D) v 9U:(fz1g u fz2g) where U is the universal role. This axiom will be translated into two datalog rules: nom(z1); nom(z2); inst(x; C); inst(x; D); triple(x; R; z1); triple(x; R; z2) ! inst(z1; z2) nom(z1); nom(z2); inst(x; C); inst(x; D); triple(x; R; z1); triple(x; R; z2) ! inst(z2; z1) Brie y, it means if there are two triples triple(x; R; z1) and triple(x; R; z2), then z1 and z2 must be same. (See details of translation in [ 5 ].)

Since A v 8R:C is the same as 9R :A v C, we can approximate A v 8R:C by adding and

9inv(R):A v C fxg u 9R:fyg v fyg u 9inv(R):fxg: Furthermore, for each axiom A v nR:C, we reduce it to A v that it can be approximated through the nominal schema axiom

1R:C, such

A u 9R:(fxg u C) u 9R:(fyg u C) v 9U:(fxg u fyg): 3.2

Approximation of Negation and Disjunction

Our approach for approximating negation is derived from [23]. In brief, we add a fresh concept neg(C) for each concept C in KB, and add the axiom neg(C)uC v ? to express that the negation of C and C are disjoint. Furthermore, we rewrite the following axioms by using their De Morgan equivalent axioms and replace :C by the fresh concept neg(C).

(1) A v B t C ) :B u :C v :A ) neg(C) v neg(A) (2) A v 8R:C ) 9R::C v :A ) 9R:neg(C) v neg(A) (3) 8R:A v C ) :C v 9R::A ) neg(C) v 9R:neg(A) (4) nR:A v C ) :C v> nR:A ) neg(C) v> nR:A (5) nR:A v C ) :C v< nR:A ) neg(C) v< nR:A

Ontology Classes Annotation P. Data P. Object P.

Rex3 552 10 0 6 Spatial4 106 13 0 13

Xenopus5 710 19 0 5

Note that we can always reduce C v nR:A to C v 9R:A. Then, for the last two axioms (4) and (5), we reduce them to neg(C) v 9R:A and neg(C) v< 1R:A. Following the ideas in [12,27], for A v B t C, it can be reduced to A v B u C, i.e., A v B and A v C, falling into unsound but complete results. We will attempt to combine this idea with the approach in the paper. Brie y, combining unsound results and incomplete results to achieve higher precise and recall. 4

Reasoning over E LROV n We brie y recall the algorithm for reasoning over ELROVn presented in [ 5 ], and the evaluation results presented therein. The algorithm actually imposes some restrictions on ELROVn which are described in detail in [ 5 ] and which cause no problem for our approximation approach.

The algorithm itself is based on results presented in [15]. Following this approach, for every ELROVn knowledge base KB we can construct a Datalog program PKB that can be used for reasoning over KB. The Datalog program PKB contains facts which are translated from all the DL normal forms (Figure 1) and rules (Figure 2). [ 5 ] contains a correctness proof.

The evaluation reported in [ 5 ] was performed using the Java-based Datalog reasoner IRIS2 [ 3 ], and we compared it to a full grounding approach for which we also used IRIS. We used suitable ontologies from the TONES repository, see Table 2 for some basic metrics, and arti cially added named individuals and axioms using nominal schemas. Results are listed in Table 3. In our approach, the number of nominal schemas per axioms had almost no e ect on the runtime, thus indicating that the approach performs very well indeed. 2 http://iris-reasoner.org/ 3 http://obo.cvs.sourceforge.net/checkout/obo/obo/ontology/

physicochemical/rex.obo 4 http://obo.cvs.sourceforge.net/checkout/obo/obo/ontology/anatomy/caro/ spatial.obo 5 http://obo.cvs.sourceforge.net/checkout/obo/obo/ontology/anatomy/gross_ anatomy/animal_gross_anatomy/frog/xenopus_anatomy.obo

5 Implementation and Evaluation

We realized the implementation based on the ELROVndatalog-based reasoner [ 5 ]. All experiments were conducted on a laptop with a 2.4GHz Intel CoreTM i7-3630QM processor and 8GB RAM operated by Windows 7 64-bit system with Java VM v.1.7.0. We set time out of 1 hour and Java heap space of 1GB. The ontologies were chose from Oxford Ontologies Repository 6, in Table Table 4. To evaluate the performance in practice, we also compared with mainstream reasoners Pellet 2.3.07, FaCT++ 1.6.28 and HermiT 1.3.79. The reasoning task is classi cation, therefore recall equals the number of subsumption relations between concepts divides its correct number. Since our approach needs some individual to re the datalog rules, we add one unique dummy individual for each concepts if the testing ontology does not contain individuals. Therefore, we can check subsumption relations by tracking those dummy individuals.

The experiment, Table 5 , shows our approach has good recalls but fails when conducting very large ontologies. The reason is that IRIS reasoner has a di culty to run with large number of rules or facts. However, with a quicker datalog reasoner or a more e cient reasoner that supports nominal schemas, we believe it will achieve a better result. Also, since the number of rules (Figure 2) are xed, we do not need a full powerful Datalog reasoner. We can speci cally program the rules to improve the e ciency.

To be noticed, the approximation in this paper can be done by HermiT reasoner since HermiT can handle DL-safe rules and the rules can directly be 6 http://www.cs.ox.ac.uk/isg/ontologies/ 7 http://clarkparsia.com/pellet/ 8 http://owl.man.ac.uk/factplusplus/ 9 http://www.hermit-reasoner.com/

C(a) 7! fsubClass(a; D)g > v C 7! ftop(C)g fag v C 7! fsubClass(a; C)g

A v C 7! fsubclass(A; C)g 9R:Self v C 7! fsubSelf(R; C)g 9R:A v C 7! fsubEx(R; A; C)g

R v T 7! fsubRole(R; T )g R v C

D 7! fsupProd(R; C; D)g R 2 NR 7! frol(R)g

R(a; b) 7! fsubEx(a; R; b; b)g

A v ? 7! fbot(A)g

A v fcg 7! fsubClass(A, c)g A u B v C 7! fsubConj(A; B; C)g A v 9R:Self 7! fsupSelf(A; R)g

A v 9R:C 7! fsupEx(A; R; B; auxAv9R:C)g R S v T 7! fsubRChain(R; S; T )g

A 2 NC 7! fcls(A)g a 2 NI 7! fnom(a)g added to the input ontology in functional style. But, HermiT doesn't have speci c reasoning procedure for EL-families, such that reasoning for EL is not its advantage. Moreover, there are ELROVnaxioms which cannot be expressed as DL-safe rules, e.g., 9R:fzg v 9T:9S:fzg. Moreover, 6

Conclusions and Future Work

We have described an approximate reasoning procedure for SROIQ which utilizes the tractable nominal-schemas-based ELROVn using a language weakening approach. We have also provided an experimental evaluation which shows the feasibility of this setting.

Going forward, there are several directions which we intend to explore. On the one hand, we will be looking into variants on how to obtain the weakened language, in the spirit of [27], and will attempt to further tweak and optimize our approach. On the one hand, we will be looking into incremental methods which use the approximate reasoning results as starting point and subsequently compute correct results in all or at least most cases.

Acknowledgements This work was supported by the National Science Foundation under award 1017225 III: Small: TROn { Tractable Reasoning with Ontologies. Semantic Web: Research and Applications, Second European Semantic Web Conference, ESWC 2005, Heraklion, Crete, Greece, May 29 { June 1, 2005, Proceedings.

Lecture Notes in Computer Science, vol. 3532, pp. 318{332. Springer (2005) 9. Hitzler, P.: Towards reasoning pragmatics. In: Janowicz, K., Raubal, M., Levashkin, S. (eds.) GeoSpatial Semantics, Third International Conference, GeoS 2009, Mexico City, Mexico, December 3{4, 2009. Proceedings. pp. 9{25. Lecture Notes in Computer Science, Springer (2009) 10. Hitzler, P., van Harmelen, F.: A reasonable semantic web. Semantic Web 1(1{2), 39{44 (2010) 11. Hitzler, P., Krotzsch, M., Parsia, B., Patel-Schneider, P.F., Rudolph, S. (eds.): OWL 2 Web Ontology Language: Primer. W3C Recommendation (27 October 2009), available at http://www.w3.org/TR/owl2-primer/ 12. Hitzler, P., Vrandecic, D.: Resolution-based approximate reasoning for OWL DL.

In: Gil, Y., et al. (eds.) Proceedings of the 4th International Semantic Web Conference, Galway, Ireland, November 2005. Lecture Notes in Computer Science, vol. 3729, pp. 383{397. Springer, Berlin (2005) 13. Horrocks, I., Kutz, O., Sattler, U.: The even more irresistible SROIQ. In: Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2006). pp. 57{67. AAAI Press (2006) 14. Knorr, M., Hitzler, P., Maier, F.: Reconciling OWL and non-monotonic rules for the Semantic Web. In: De Raedt, L., Bessiere, C., Dubois, D., Doherty, P., Frasconi, P., Heintz, F., Lucas, P. (eds.) ECAI 2012, 20th European Conference on Arti cial Intelligence, 27-31 August 2012, Montpellier, France. Frontiers in Articial Intelligence and Applications, vol. 242, pp. 474{479. IOS Press, Amsterdam (2012) 15. Krotzsch, M.: E cient inferencing for OWL EL. In: Janhunen, T., Niemela, I. (eds.) Proc. 12th European Conf. on Logics in Arti cial Intelligence (JELIA'10).

LNAI, vol. 6341, pp. 234{246. Springer (2010) 16. Krotzsch, M., Rudolph, S., Hitzler, P.: ELP: Tractable rules for OWL 2. In: Sheth, A., Staab, S., Dean, M., Paolucci, M., Maynard, D., Finin, T., Thirunarayan, K. (eds.) Proceedings of the 7th International Semantic Web Conference (ISWC-08).

Lecture Notes in Computer Science, vol. 5318, pp. 649{664. Springer (2008) 17. Krotzsch, M., Maier, F., Krisnadhi, A.A., Hitzler, P.: A better uncle for OWL: Nominal schemas for integrating rules and ontologies. In: Proceedings of the 20th International Conference on World Wide Web (WWW'11). pp. 645{654. ACM (2011) 18. Motik, B., Cuenca Grau, B., Horrocks, I., Wu, Z., Fokoue, A., Lutz, C. (eds.): OWL 2 Web Ontology Language: Pro les. W3C Recommendation (27 October 2009), available at http://www.w3.org/TR/owl2-profiles/ 19. Motik, B., Shearer, R., Horrocks, I.: Hypertableau reasoning for description logics.

J. of Arti cial Intelligence Research 36(1), 165{228 (2009) 20. Pan, J.Z., Thomas, E.: Approximating OWL-DL ontologies. In: Proceedings of the Twenty-Second AAAI Conference on Arti cial Intelligence, July 22-26, 2007, Vancouver, British Columbia, Canada. pp. 1434{1439. AAAI Press (2007) 21. Pan, J.Z., Thomas, E., Zhao, Y.: Completeness guaranteed approximations for OWL-DL query answering. In: Grau, B.C., Horrocks, I., Motik, B., Sattler, U. (eds.) Proceedings of the DL Home 22nd International Workshop on Description Logics (DL 2009), Oxford, UK, July 27-30, 2009. CEUR Workshop Proceedings, vol. 477 (2009) 22. Ren, Y., Pan, J.Z., Zhao, Y.: Soundness preserving approximation for TBox reasoning in R. In: Grau, B.C., Horrocks, I., Motik, B., Sattler, U. (eds.) Proceedings of the DL Home 22nd International Workshop on Description Logics (DL 2009), Oxford, UK, July 27-30, 2009. CEUR Workshop Proceedings, vol. 477 (2009) 23. Ren, Y., Pan, J.Z., Zhao, Y.: Towards soundness preserving approximation for abox reasoning of owl2. In: Haarslev, V., Toman, D., Weddell, G.E. (eds.) Proceedings of the 23rd International Workshop on Description Logics (DL 2010), Waterloo, Ontario, Canada, May 4-7, 2010. CEUR Workshop Proceedings, vol. 573. CEURWS.org (2010) 24. Rudolph, S., Tserendorj, T., Hitzler, P.: What is approximate reasoning? In: Calvanese, D., Lausen, G. (eds.) Proceedings of the 2nd International Conference on Web Reasoning and Rule Systems (RR2008). Lecture Notes in Computer Science, vol. 5341, pp. 150{164. Springer (2008) 25. Schaerf, M., Cadoli, M.: Tractable reasoning via approximation. Arti cial Intelligence 74, 249{310 (1995) 26. Selman, B., Kautz, H.A.: Knowledge compilation using Horn approximations. In: Proceedings of the Ninth National Conference on Arti cial Intelligence (AAAI-91). pp. 904{909 (1991) 27. Tserendorj, T., Rudolph, S., Krotzsch, M., Hitzler, P.: Approximate OWLreasoning with Screech. In: Calvanese, D., Lausen, G. (eds.) Web Reasoning and Rule Systems, Second International Conference, RR 2008, Karlsruhe, Germany, October 31-November 1, 2008. Proceedings. Lecture Notes in Computer Science, vol. 5341, pp. 165{180 (2008)

References

1. Baader , F. , Calvanese , D. , McGuinness , D. , Nardi , D. , Patel-Schneider , P . (eds.): The Description Logic Handbook: Theory, Implementation, and Applications . Cambridge University Press, second edn. ( 2007 )

2. Baader , F. , Brandt , S. , Lutz , C. : Pushing the EL envelope . In: Proc. 19th Int. Joint Conf. on Arti cial Intelligence (IJCAI-05) . pp. 364 { 369 . Morgan-Kaufmann Publishers, Edinburgh, UK ( 2005 )

3. Bishop , B. , Fischer , F. : IRIS { Integrated Rule Inference System . In: van Harmelen, F. , Herzig , A. , Hitzler , P. , Lin , Z. , Piskac , R. , Qi , G . (eds.) ARea2008, Workshop on Advancing Reasoning on the Web: Scalability and Commonsense. Proceedings of the Workshop on Advancing Reasoning on the Web: Scalability and Commonsense Tenerife , Spain, June 2, 2008 . CEUR Wrokshop Proceedings , vol. 350 . CEURWS.org ( 2008 )

4. Cadoli , M. , Schaerf , M. : Approximate inference in default reasoning and circumscription . Fundamenta Informaticae 23 , 123 { 143 ( 1995 )

5. Carral , D. , Wang , C. , Hitzler , P. : Towards an e cient algorithm to reason over description logics extended with nominal schemas . Tech. rep., Kno .e.sis Center, Wright State University ( 2013 ), available at http://www.pascal-hitzler.de/ pub/elrov13.pdf

6. Fensel , D., van Harmelen , F. : Unifying reasoning and search to web scale . IEEE Internet Computing 11 ( 2 ), 96 , 94{ 95 ( 2007 )

7. Grau , B.C. , Motik , B. , Stoilos , G. , Horrocks , I. : Completeness guarantees for incomplete ontology reasoners: Theory and practice . J. Artif. Intell. Res. (JAIR) 43 , 419 { 476 ( 2012 )

8. Groot , P. , Stuckenschmidt , H. , Wache , H.: Approximating description logic classication for semantic web reasoning . In: Gomez-Perez , A. , Euzenat , J . (eds.) The