ABox Abduction Solver Exploiting Multiple DL Reasoners

Abstract

We have implemented an ABox abduction solver based on Reiter's minimal hitting set algorithm. Our solver runs a DL reasoner as a black box, similarly to the existing AAA solver. The advantage of the current work is the use of OWL API, which allows to plug-in a number of di erent DL reasoners. In this paper we describe our implementation and present an evaluation results comparing AAA, which is tightly coupled with Pellet, and the current implementation running with three di erent reasoners: Pellet, JFact, and HermiT. The latter combination showed the most promising results.

Keywords

• description logics
• abduction
• implementation
• evaluation

Introduction

Abduction, originally introduced by Peirce [ 18 ], is non-standard reasoning problem whose goal is to provide explanations why some observation does not follow from a knowledge base. Abduction in DL naturally distinguishes between TBox and ABox abduction [ 5 ] the former working with observations and explanations on the TBox level, the latter assuming that observations and explanations are ABox assertions. We focus on ABox abduction which has interesting applications, e.g. in diagnostic reasoning [ 13,5,19 ] or in multimedia-interpretation [ 6,2 ]. A number of theoretical algorithms for ABox abduction were presented [ 14,10,9 ], and some were also implemented into abduction solvers [ 4,15,6,2,3 ].

In this paper, we extend the AAA solver [ 20 ] which focuses on expressive DLs. Compared to previous works, this solver is able to handle any DL expressivity up to SROIQ, due to using a DL reasoner as a black box, and it is sound and complete. However, the main disadvantage of AAA is that it is tightly coupled with Pellet 2 [ 23 ] which is an outdated reasoner and it makes AAA less e ective.

We describe a reimplementation of AAA, dubbed B, and report on our rst experimental results, providing the following contributions: (a) B exploits OWL API [ 11 ] and thus it is able to modularly plugin di erent DL reasoners; (b) it includes more extensive pruning and an additional optimization technique called caching of inconsistent hitting-set candidates; (c) we report on rst empirical results comparing AAA and B combined with Pellet 2, JFact [ 17 ], and HermiT [ 22,7 ] reasoners.

We plan to continue our experiments with B, especially testing it with additional DL reasoners. In the future it will serve as a base for next versions of AAA. 2

ABox Abduction in DL

We build on top of the ALCHO [ 1 ]. A vocabulary consists of countably in nite mutually disjoint sets of individuals NI = fa; b; : : :g, roles NR = fP; R; : : :g, and atomic concepts NC = fA; B; : : :g. Concepts are recursively built using constructors :, u, 9, fag, as shown in Table 1. Additional concepts union C t D := :(:C u:D) and value restriction 8R:C := :9R::C are de ned as syntactic sugar; and also ::C := C by de nition. A knowledge base K = (T ; A) consists of a TBox T , a nite set of GCI and RIA axioms, and an ABox A, a nite set of assertions as given in Table 1.

An interpretation is a pair I = ( I ; I ), where I 6= ; is a domain, and the interpretation function I maps each individual a 2 NI to aI 2 I , each atomic concept A 2 NC to AI I , each role R 2 NR to RI I I in such a way that the constraints on the right-hand side of Table 1 are satis ed.

An interpretation I satis es an axiom ' (denoted I j= ') if the respective constraint in Table 1 is satis ed. It is a model of a knowledge base K = (T ; A) (denoted I j= K) if I j= ' for all ' 2 T [ A. A knowledge base is consistent, if there is at least one interpretation I such that I j= K. A knowledge base entails an axiom ' (denoted K j= ') if I j= ' for each I j= K.

We de ne :' := :C(a) for a concept assertion ' = C(a). Thanks to presence of nominals in ALCHO [ 12,10 ] we are also able to de ne :' := :R(a; b) := 8R::fbg(a) for a role assertion ' = R(a; b), and :' := R(a; b) for ' = :R(a; b). In addition, :A = f:' j ' 2 Ag for any set of ABox assertions A. The ABox encoding of an interpretation I is MI = fC(a) j I j= C(a); C2 fA; :Ag; A 2 NC; a 2 NIg [ fR(a; b) j I j= R(a; b); R 2 NR; a; b 2 NIg [ f:R(a; b) j I j= :R(a; b); R 2 NR; a; b 2 NIg. Note that ABox encodings obtained from models of nite knowledge base which has a nite signature are assumed to be nite. The are in no way homomorphic with the original models, as they ignore the anonymous part of the model. A negation :MI of the ABox encoding of a model I of K is called an antimodel K.

In ABox abduction, we are given a knowledge base K and an observation O consisting of ABox assertions, that is, some evidence we have observed. The task is to nd an explanation E , again, consisting of ABox assertions, such that K [ E j= O.

De nition 1 (ABox Abduction Problem [ 5 ]). An ABox abduction problem is a pair P = (K; O) such that K is a knowledge base in DL and O is a set of ABox assertions. A solution of P (also called explanation) is any nite set E of ABox assertions such that K [ E j= O.

While De nition 1 establishes the basic reasoning mechanism of abduction, some of the explanations it permits are clearly undesired. The explanations should, at minimum, ful l some basic sanity requirements.

De nition 2 ([ 5 ]). Given an ABox abduction problem P = (K; O) and its solution E we say that: 1. E is consistent if E [ K 6j= ?, i.e. E is consistent w.r.t. K; 2. E is relevant if E 6j= Oi for each Oi 2 O, i.e. E does not entail each Oi; 3. E is explanatory if K 6j= O, i.e. K does not entail O.

An explanation should be consistent, as anything follows from inconsistency; and so, an explanation that makes K inconsistent does not really explain the observation. It should be relevant { it should not imply the observation directly without requiring the knowledge base K at all. And it should be explanatory, that is, we should not be able to explain the observation without it.

Hereafter, when we say explanation we always mean a consistent, relevant, and explanatory explanation, unless indicated otherwise. In addition, in order to avoid excess hypothesizing, minimality is required.

De nition 3 (Syntactic Minimality). Assume an ABox abduction problem P = (K; O). Given two solutions E and E 0 of P, we say that E is (syntactically) smaller than E 0 if E E 0.1 We further say that a solution E of P is syntactically minimal if there is no other solution E 0 of P that is smaller than E . 1 Note that before we compare two solutions E and E0 of P syntactically, we typically normalize the assertions w.r.t. (outermost) concept conjunction: as C u D(a) is equivalent to the pair of assertions C(a) and D(a), we replace the former form by the latter while possible.

Our Approach

We have implemented an ABox abduction solver based on the approach of Pukancova and Homola [ 20 ] which implements the Reiter's minimal hitting set algorithm [ 21 ]. Likewise to the original AAA solver [ 20 ], the input observations can be any (also complex) concept and role assertions. The explanations are limited to sets of atomic and negated atomic concept and role assertions.

For a single observation O, a solution of an abduction problem P = (K; O) according to De nition 1 can be obtained as any E s.t. K[E [f:Og is inconsistent As showed by Reiter [ 21 ], we can compute the minimal explanations of P by nding all minimal hitting sets for all antimodels of K [ f:Og.

We do this by searching through the candidate hitting sets breadth- rst. For details see the report of Pukancova and Homola [ 20 ], on which we base our implementation. The algorithm SingleAbduction is listed below. Algorithm 1 SingleAbduction(K, O , Dmax, O) Require: knowledge base K, single observation O, maximum depth Dmax, minimal inconsistent candidates S?, set of observations O Ensure: set of all explanations S, set of all minimal inconsistent candidates S? 1: if K [ fOg is inconsistent then 2: return ; . no consistent explanations as K j= :O 3: else if K [ f:Og is inconsistent then 4: return "nothing to explain" 5: end if 6: D 1; C f;g; S ; 7: while C 6= ; and D Dmax do 8: Cnext ; . hitting set candidates for the next iteration 9: for all c 2 C do 10: if s 6 c for all s 2 S and c 6j= O for all O 2 O and memCons(K [ O, c, S?) and K [ f:Og [ c is inconsistent then

S S [ fcg . c is a hitting set (explanation) else if D 6= Dmax then for all 2 redAntiModel(K, O, O, c) do

Cnext [ fc [ g 11: 12: 13: 14: 15: 16: 17: 18: C Cnext 19: D D + 1 20: end while 21: return S, S?

Cnext end for end if end for

The rst three parameters are the input knowledge base K, the observation O, and the maximum depth Dmax which allows to limit the maximal length of explanations to search for. The remaining two parameters are auxiliary and they are important when SingleAbduction is called repeatedly to nd explanations for multiple observations. For the single observation case the algorithm is called as SingleAbduction(K; O; Dmax; ;; fOg).

The algorithm initializes the set of candidate explanations to f;g. Then we loop through the candidates c breadth- rst, and process each candidate by either removing (pruning [ 20 ]) the candidate if it is not minimal, relevant, or consistent ( rst three if-conditions in line 10) or adding it to the set of explanations if K [ f:Og [ c is inconsistent, i.e. K [ c j= O (the last if-condition in line 10). Finally, if K [ f:Og [ c was consistent (and Dmax is not yet reached) then we obtain the respective antimodel and populate the candidates for the next level of search.

The algorithm features two additional optimizations. Firstly, we do not store only explanations (i.e., minimal hitting sets) found so far, but we also store all minimal candidates which are inconsistent (the set S?). This allows for additional pruning which is implemented in the memCons function. 2: 3: 4: 5: 6: 7: S? S? [ fcg 8: return false 9: end if 10: end function 1: function memCons( Knowledge base K, hitting set candidate c, minimum inconsistent candidates S?) if s c for some s 2 S? then

return false else if K [ c is consistent then

return true else

Consecutively, we further extend pruning by reducing all antimodels by removing assertions if or : is present in K [ f:Og [ c. It's straightforward to observe that all such candidates would be inconsistent, irrelevant, or not minimal. This is implemented in the redAntiModel function but also in the check in line 1 of SingleAbduction.

To nd solutions for multiple-observation abduction problem, we rely on the approach based on solving separate single-observation problems and combining the results [ 20 ]. The only minor improvement is in passing the set S? between the SingleAbduction calls. The algorithm is called MultipleAbduction.

The main advantage of our approach compared to previous works [ 20,9 ] is that DL reasoner is not tightly integrated, but instead called using OWL API. This allows modular pairing with di erent reasoners. The reasoner is called from SingleAbduction and memCons whenever consistency or inconsistency checks are made. The function redAntiModel does not run reasoning again but merely extracts the model from last successful consistency check calling getTypes and getObjectPropertyValues from OWL API. 1: function redAntiModel( Knowledge base K, observation O, observations O, hitting set candidate c ) Experimental evaluation was conducted with implementations of AAA and B, B paired with three di erent DL reasoners { Pellet, HermiT, and JFact. Two di erent experiments were conducted, one with a single observation and one with a multiple observation. The main goal was to compare the execution times. It is also interesting to trace the di erences between the computation of the two implementations AAA and B, especially how is the search space pruned.

The source code of both implementations is available at http://dai.fmph. uniba.sk/~pukancova/aaa/. We have chosen three ontologies for the evaluation: Family ontology (Our own small ontology of family relations)2, Co ee ontology by Carlos Mendes3, and LUBM (Lehigh University Benchmark [ 8 ]). The parameters of the ontologies are stated in Table 2.

In all experiments, explanations for an observation are computed through both AAA and B, whilst B is run three times { once with Pellet, once with HermiT, and once with JFact. All experiments were done on a 6-core 3.2 GHz AMD PhenomTM II X6 1090T Processor, 8 GB RAM, running Ubuntu 17.10, Linux 4.13.0, while the maximum Java heap size was set to 4GB. We have used the GNU time utility to measure the CPU time consumed by AAA while running in user mode, summed over all threads.

In the single observation experiment, the experiments are conducted iteratively for the maximal length of explanations from 1 to 5. In the multiple observation experiment, the iterations are only up to the maximal length of 3. For each experimental setting, the run is repeated for 10 times. From now on, all execution times are computed as the average values from 10 runs with the same experimental setting.

All experiments were executed while disallowing explanations with loops (i.e., re exive role assertions), an optional feature of both solvers. As mentioned above, the single observation experiment was conducted for all the three ontologies: Family, Co ee and LUBM. For each ontology, one single observation was chosen: for Family ontology Mother(jane), for Co ee ontology Macchiato(a), and for LUBM Person(jack).

The experiment was conducted iteratively for the maximal length of explanations from 1 to 5 with AAA and B paired with each reasoner.

The average execution times are plotted in Figure 1. The deviations computed for each set of 10 runs with the same experimental setting were quite low 2.504 % on average. The times for the four experiments { LUBM ontology for the maximal lengths 4 and 5 through implementation B with Pellet and JFact { actually do 2 http://dai.fmph.uniba.sk/~pukancova/aaa/ont/ 3 https://gist.githubcom/cmendesce/56e1e16aee5a556a186f512eda8dabf3

AAA B-Pellet B-Hermit B-JFact Fig. 2. Proportion of pruned nodes, reused models and TA calls for multiple observations not correspond to the times when explanations were computed but the times when Java memory was exceeded.

The search space is pruned according to the implementation used. The proportion of non-pruned nodes (nodes for which tableau algorithm TA for consistency check is called) and pruned nodes is showed in Figure 2. Note that, AAA implements also model reuse, whilst B does not. The results for B are the same in cases when Java did not run out of memory for all three reasoners. For this reason there is always just one plot in case of B.

In this experiment, the implementation B using HermiT achieves the lowest times except in two cases { Family ontology with the maximal lengths 1 and 2. On the other hand, in 8 cases (from the overall 15 cases) AAA has the highest times. Let us remind, that B with Pellet and JFact reasoners ran out of memory in case of the LUBM ontology with the maximal lengths 4 and 5, so these times are not relevant. 4.3

Multiple Observation Experiment The multiple observation experiment was conducted analogously. The only di erence is that the observations are in the form of a set of ABox assertions, namely: for Family ontology fFather(jack); Mother(eva); Person(fred)g, for Co ee ontology fMilk(a); Co ee(b); Pure(c)g, and for LUBM fPerson(jack); Employee(jack); Publication(a)g.

For each ontology with the respective observation, explanations were computed iteratively with the maximal length from 1 to 3 through AAA, and trough B using Pellet, HermiT, and JFact. The average times are plotted in Figure 3. The average deviation was 7.06 %. The following experiments ran out of memory: Family ontology through B using Pellet and JFact with the maximal length 3, Co ee ontology through B using Pellet with the maximal length 3 and using JFact with the maximal lengths 2 and 3, LUBM through AAA with the maximal length 3, and through B using Pellet and JFact with the maximal lengths 1, 2, and 3. Note that, the only reasoner that did not run out of memory is HermiT.

Also in this experiment, the numbers of pruned nodes and non-pruned nodes were computed. The respective proportions are captured in Figure 4. In case of B, the proportions are the same with the three di erent reasoners (out-of-memory cases are ignored).

In this experiment, the times with HermiT were always the lowest. Also, while a number of experiments ran out of memory this was never the case with B combined with HermiT. 5

Conclusions

We have reimplemented the AAA ABox abduction solver [ 20 ]. The new implementation, called B, used OWL API [ 11 ] and thus can be run with di erent reasoner. In the evaluation we have compared AAA and B combined with Pellet 2 [ 23 ], JFact [ 17 ], and HermiT [ 22,7 ]. 106 105 104 103 102 101

AAA B-Pellet B-Hermit

B-JFact 1 3 1 3 Fig. 4. Proportion of pruned nodes, reused models and TA calls for multiple observations

Not only that in the most cases HermiT achieved the best time, but it is also the only reasoner that did not exceed the memory. The combination of B and HermiT seems to be currently the best option for our abduction solver. Moreover, the evaluation has also showed that B, applying additional pruning techniques, processes the search space in a more optimal way.

On the other hand, B has exceeded the memory a couple more times than AAA, a problem that we would like to tune in the future. We would also like extend this evaluation with additional reasoners.

Acknowledgements. This work presents the results of the Master's thesis by Drahom r Mrozek [ 16 ]. It was supported by the Slovak national project VEGA 1/0778/18. Julia Pukancova is also supported by an extraordinary scholarship awarded by Faculty of Mathematics, Physics, and Informatics, Comenius University in Bratislava, and by the Comenius University grant no. UK/266/2018. We would like to thank to anonymous reviewers from previous DL workshops for valuable suggestions.

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 ( 2003 )

2. Castano , S. , Espinosa Perald , I.S. , Ferrara , A. , Karkaletsis , V. , Kaya , A. , Moller, R., Montanelli , S. , Petasis , G. , Wessel , M. : Multimedia interpretation for dynamic ontology evolution . J. Log. Comput . 19 ( 5 ), 859 { 897 ( 2009 )

3. Del-Pinto , W. , Schmidt , R.A. : Forgetting-based abduction in ALC . In: Proceedings of the Workshop on Second-Order Quanti er Elimination and Related Topics (SOQE 2017 ), Dresden, Germany. CEUR-WS , vol. 2013 , pp. 27 { 35 ( 2017 )

4. Du , J. , Qi , G. , Shen , Y. , Pan , J.Z. : Towards practical ABox abduction in large description logic ontologies . Int. J. Semantic Web Inf. Syst . 8 ( 2 ), 1 { 33 ( 2012 )

5. Elsenbroich , C. , Kutz , O. , Sattler , U. : A case for abductive reasoning over ontologies . In: Proceedings of the OWLED*06 Workshop on OWL: Experiences and Directions , Athens, GA, USA. CEUR-WS, vol. 216 ( 2006 )

6. Espinosa Perald , I.S. , Kaya , A. , Moller, R.: Formalizing multimedia interpretation based on abduction over description logic ABoxes . In: Proceedings of the 22nd International Workshop on Description Logics (DL 2009 ), Oxford, UK. CEURWS, vol. 477 ( 2009 )

7. Glimm , B. , Horrocks , I. , Motik , B. , Stoilos , G. , Wang , Z. : Hermit: An OWL 2 reasoner . Journal of Automated Reasoning 53 ( 3 ), 245 { 269 ( 2014 )

8. Guo , Y. , Pan , Z. , He in, J.: LUBM: A benchmark for OWL knowledge base systems . Journal of Web Semantics 3 ( 2-3 ), 158 { 182 ( 2005 )

9. Halland , K. , Britz , K. : Abox abduction in ALC using a DL tableau . In: 2012 South African Institute of Computer Scientists and Information Technologists Conference, SAICSIT '12, Pretoria , South Africa. pp. 51 { 58 ( 2012 )

10. Halland , K. , Britz , K. : Nave ABox abduction in ALC using a DL tableau . In: Proceedings of the 2012 International Workshop on Description Logics , DL 2012 , Rome, Italy. CEUR-WS , vol. 846 ( 2012 )

11. Horridge , M. , Bechhofer , S.: The OWL API: A java API for OWL ontologies . Semantic Web 2 ( 1 ), 11 { 21 ( 2011 )

12. Horrocks , I. , Kutz , O. , Sattler , U. : The even more irresistible SROIQ . In: Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning , Lake District of the United Kingdom . pp. 57 { 67 . AAAI ( 2006 )

13. Hubauer , T. , Legat , C. , Seitz , C. : Empowering adaptive manufacturing with interactive diagnostics: A multi-agent approach . In: Advances on Practical Applications of Agents and Multiagent Systems { 9th International Conference on Practical Applications of Agents and Multiagent Systems, PAAMS 2011 , Salamanca, Spain. pp. 47 { 56 ( 2011 )

14. Klarman , S. , Endriss , U. , Schlobach , S.: ABox abduction in the description logic ALC . Journal of Automated Reasoning 46 ( 1 ), 43 { 80 ( 2011 )

15. Ma , Y. , Gu , T. , Xu , B. , Chang , L. : An ABox abduction algorithm for the description logic ALCI . In: Intelligent Information Processing VI { 7th IFIP TC 12 International Conference, IIP 2012 , Guilin, China . Proceedings. IFIP AICT , vol. 385 , pp. 125 { 130 . Springer ( 2012 )

16. Mrozek , D. : Abduction Solver Exploiting Multiple DL Reasoners. Master's thesis , Comenius University in Bratislava ( 2018 )

17. Palmisano , I. : Jfact dl reasoner . http://jfact.sourceforge.net/

18. Peirce , C.S. : Deduction, induction, and hypothesis . Popular science monthly 13 , 470 { 482 ( 1878 )

19. Pukancova , J. , Homola , M. : Abductive reasoning with description logics: Use case in medical diagnosis . In: Proceedings of the 28th International Workshop on Description Logics (DL 2015 ), Athens, Greece. CEUR-WS , vol. 1350 ( 2015 )

20. Pukancova , J. , Homola , M. : Tableau-based ABox abduction for the ALCHO description logic . In: Proceedings of the 30th International Workshop on Description Logics , Montpellier, France. CEUR-WS , vol. 1879 ( 2017 )

21. Reiter , R.: A theory of diagnosis from rst principles . Arti cial intelligence 32 ( 1 ), 57 { 95 ( 1987 )

22. Shearer , R. , Motik , B. , Horrocks , I. : Hermit: A highly-e cient OWL reasoner . In: Proceedings of the Fifth OWLED Workshop on OWL: Experiences and Directions , Karlsruhe, Germany. CEUR-WS , vol. 432 ( 2008 )

23. Sirin , E. , Parsia , B. , Cuenca Grau , B. , Kalyanpur , A. , Katz , Y. : Pellet: A practical OWL-DL reasoner . Journal of Web Semantics 5 ( 2 ), 51 { 53 ( 2007 )