# abox_abduction_via_forgetting_in_alc__216a232a.pdf

The Thirty-Third AAAI Conference on Artiﬁcial Intelligence (AAAI-19)

ABox Abduction via Forgetting in ALC

Warren Del-Pinto, Renate A. Schmidt School of Computer Science, The University of Manchester Oxford Road, Manchester M13 9PL, United Kingdom

Abductive reasoning generates explanatory hypotheses for new observations using prior knowledge. This paper investigates the use of forgetting, also known as uniform interpolation, to perform ABox abduction in description logic (ALC) ontologies. Non-abducibles are speciﬁed by a forgetting signature which can contain concept, but not role, symbols. The resulting hypotheses are semantically minimal and consist of a disjunction of ABox axioms. These disjuncts are each independent explanations, and are not redundant with respect to the background ontology or the other disjuncts, representing a form of hypothesis space. The observations and hypotheses handled by the method can contain both atomic or complex ALC concepts, excluding role assertions, and are not restricted to Horn clauses. Two approaches to redundancy elimination are explored in practice: full and approximate. Using a prototype implementation, experiments were performed over a corpus of real world ontologies to investigate the practicality of both approaches across several settings.

Introduction The aim of abductive reasoning is to generate explanatory hypotheses for new observations, enabling the discovery of new knowledge. Abduction was identiﬁed as a form of reasoning by (Peirce 1878). It has also become a recurring topic of interest in the ﬁeld of AI, leading to work such as abductive extensions of Prolog for natural language interpretation (Stickel 1991; Hobbs et al. 1993), the integration of abduction with induction in machine learning (Mooney 2000) including work in the ﬁelds of inductive (Muggleton and Bryant 2000) and abductive logic programming (Kakas, Kowalski, and Toni 1992; Ray 2009) and statistical relational AI (Raghavan and Mooney 2010). This paper focuses on abduction in description logic (DL) ontologies. These consist of a TBox of information about general entities known as concepts and roles and an ABox of assertions over instances of these concepts known as individuals. DL ontologies are widely used to express background knowledge and as alternative data models for knowledge management. They are commonly used in ﬁelds such as AI, computational linguistics, bio-informatics and robotics. The need for abductive reasoning in ontologies

Copyright c 2019, Association for the Advancement of Artiﬁcial Intelligence (www.aaai.org). All rights reserved.

was highlighted by (Elsenbroich, Kutz, and Sattler 2006). Use cases include hypothesis generation, diagnostics and belief expansion for which most current reasoning methods for ontologies are not suitable. This has led to work on abduction in DLs, including studies in EL (Bienvenu 2008) and applications such as ontology repair (Lambrix, Dragisic, and Ivanova 2012; Wei-Kleiner, Dragisic, and Lambrix 2014) and query explanation (Calvanese et al. 2013). For ABox abduction, methods in more expressive logics such as ALC and its extensions have been proposed (Klarman, Endriss, and Schlobach 2011; Halland and Britz 2012; Pukancov a and Homola 2017). Similarly, work exists on TBox abduction (Wei-Kleiner, Dragisic, and Lambrix 2014; Halland, Britz, and Klarman 2014). However, few implementations and evaluations are available for abductive reasoning. Exceptions include the ABox abduction method of (Du, Wang, and Shen 2014) in Datalog rewritable ontologies and a TBox abduction method using justiﬁcation patterns (Du, Wan, and Ma 2017). The aim of this paper is to investigate the use of forgetting for ABox abduction in DL ontologies. Forgetting is a non-standard reasoning method that restricts ontologies to a speciﬁed set of symbols, retaining all entailments preservable in the restricted signature. It is also referred to as uniform interpolation or second-order quantiﬁer elimination, and has been proposed as a method for abduction in different contexts (Doherty, Łukaszewicz, and Szałas 2001; Gabbay, Schmidt, and Szałas 2008; Wernhard 2013; Koopmann and Schmidt 2015b). However, so far the forgettingbased approach has been insufﬁciently studied or applied, particularly in terms of preferred characteristics of abductive hypotheses and in the setting of large DL ontologies. This work investigates hypotheses obtained using forgetting-based abductive reasoning. These hypotheses are weakest sufﬁcient conditions (Lin 2001), related to the DL literature notion of semantic minimality (Halland, Britz, and Klarman 2014), meaning that they make the fewest assumptions necessary to explain an observation given the background knowledge. However, without additional steps, these hypotheses are not guaranteed to be consistent and are likely to be mostly redundant when the forgetting based approach is applied to large ontologies. In this work, additional constraints are investigated to capture these redundancies and practical methods for their removal are presented.

The main contributions of this paper are: (1) Forgettingbased ABox abduction in DL ontologies is explored and formalised. The aim is to compute hypotheses that do not contain unnecessary assumptions nor misleading, i.e. redundant, explanations. The need to eliminate redundancies from uniform interpolants is motivated and solved. (2) A practical method for this task is presented for ALC. It computes hypotheses containing only abducible symbols. Nonabducibles are speciﬁed by a forgetting signature consisting of any set of concept, but not role, symbols. Both the observations and hypotheses may contain any atomic or complex ALC (or ALCµ) concepts, but cannot contain role assertions. An efﬁcient annotation-based ﬁltering method is proposed to eliminate redundancies from uniform interpolants. The method uses the forgetting tool LETHE which is shown to be applicable to ABox abduction, thereby answering an open question in (Koopmann and Schmidt 2015b). However, the general framework could use any forgetting method designed for ALC. (3) The method is evaluated empirically over a corpus of real-world ontologies. An approximate and a full approach to redundancy elimination are compared. Proofs and additional examples are in the long version of this paper https://arxiv.org/abs/1811.05420.

Problem Deﬁnition Concepts in the description logic ALC have the following forms: | A | C | C D | C D | r.C | r.D, where A denotes a concept name, C and D are arbitrary ALC concepts and r is a role name. Atomic concepts are concept names, while concepts such as r.(A B) are said to be complex. A knowledge base or ontology O in ALC consists of a TBox and an ABox. The TBox consists of a set of general concept inclusions of the form C D, where C and D are any ALC concept. The ABox contains axioms C(a) and role assertions of the form r(a, b), where C is any ALC concept and a and b are individuals. The signature of X, denoted as sig(X), is the set of all concept and role names occurring in X, where X can be any ontology or axiom. The aim of abduction is to compute a hypothesis to explain a new observation. Our focus is on this problem:

Deﬁnition 1. Abduction in Ontologies. Let O be an ontology and ψ a set of ABox axioms, where ψ does not contain role assertions, such that O |= , O, ψ |= and O |= ψ. Let SA be a set of symbols called abducibles which contains all role symbols in (O, ψ). The abduction problem is to ﬁnd a hypothesis H as a disjunction of ABox axioms, without role assertions, that contains only those symbols speciﬁed in SA such that: (i) O, H |= , (ii) O, H |= ψ, (iii) H does not contain inter-disjunct redundancy i.e., there is no disjunct αi in H such that O, αi |= α1 ... αi 1 αi+1 ... αn and (iv) for any H satisfying conditions (i) (iii) where sig(H ) SA, if O, H |= O, H then O, H |= O, H.

The set of abducibles SA deﬁnes the subset of symbols in the ontology that may appear in the hypothesis H. Here, SA must contain all role symbols in (O, ψ) and both the observation ψ and H may not contain role assertions. For our approach, the language of ALC must be extended to include disjunctive ABox assertions over multiple individuals, and

in some speciﬁc cases ﬁxpoints (Calvanese, De Giacomo, and Lenzerini 1999) to represent cyclic results. These will be discussed alongside the proposed method. The rationale for the problem conditions is to focus efforts on computing informative hypotheses. Otherwise, the search space for hypotheses would be too large. Deﬁning the set of abducibles SA allows a user to focus on explanations containing speciﬁc information represented as symbols, utilising their own knowledge of the problem domain. Conditions (i) and (ii) are standard requirements in most abductive reasoning tasks. Condition (i) requires that all generated hypotheses H are consistent with the background knowledge in the ontology O. Otherwise would be entailed from which everything follows. Condition (ii) ensures that H explains the observation ψ when added to the background knowledge in O. Conditions (iii) and (iv) capture two distinct notions. Condition (iii) ensures that each of the disjuncts in the hypothesis H are independent explanations (Konolige 1992) for the observation ψ. That is, there are no disjuncts in H that express information that is the same or more speciﬁc than that which is already expressed by the other disjuncts in H. This also excludes disjuncts that are simply inconsistent with the background knowledge as a special case, since if for a disjunct α in H we have O, α |= then everything follows. Condition (iii) is referred to as inter-disjunct redundancy. The following example illustrates this, where Brain Drain (BD) is a disease, BDV1 and BDV2 are viruses, p1 is a patient and the acronyms h D, h S and c O stand for has Disease , has Symptom and carrier Of respectively:

Example 1. Let O = { h D.BD h S.Headache, Tired Scientist h S.Headache, c O.(BDV1 BDV2) h D.BD, Tired Accountant h S.Headache, Tired Accountant(p1)}, ψ = { h S.Headache(p1)} and let SA include all symbols in O except Headache. Consider the hypothesis H =( h D.BD Tired Scientist c O.(BDV1 BDV2) Tired Accountant)(p1). This satisﬁes conditions (i), (ii) and (iv). However, there are two redundant disjuncts: Tired Accountant(p1) and c O.(BDV1 BDV2 )(p1). The ﬁrst is inconsistent with the ontology O. The second is not independent: it is simply stronger than the disjunct h D.BD(p1) in H . A user may mistakenly believe that these two redundancies are valid, independent explanations for the symptom. Thus, condition (iii) excludes these redundancies, resulting in the preferred hypothesis H =( h D.BD Tired Scientist)(p1).

As condition (iii) requires that each disjunct be consistent with the ontology O, condition (i) is not strictly needed. However, as consistency is a key condition in most abduction contexts it is useful to emphasise it separately. Condition (iv) captures the notion of semantic minimality (Halland, Britz, and Klarman 2014) under the background knowledge O. It restricts hypotheses to those that make the fewest assumptions necessary to explain the observation ψ given O. This is shown in the example below.

Example 2. Let O = {A B, B C}, ψ = {C(a)} and SA = {A, B}. Consider the hypotheses H1 = B(a) and H2 = A(a). Both satisfy the conditions in Deﬁnition 1(i) and (ii). However, hypothesis H2 does not satisfy (iv), since O, H2 |= O, H1, but the reverse does not hold. Thus, H2 is

a stronger or less minimal hypothesis than H1.

From this, it can be seen that condition (iv) rejects semantically stronger hypotheses. It should be noted that, unlike some other settings such as (Halland, Britz, and Klarman 2014), here H can contain disjunction. Thus, redundant disjuncts must be considered separately, as in condition (iii), since condition (iv) does not account for these. With these conditions, the aim of this work is to compute a semantically minimal hypothesis consisting of all disjuncts that each represent an independent explanation of the observation ψ, none of which overlaps with either the background knowledge or the other disjuncts. Deﬁnition 1 does not remove all choices between or redundancies in the forms taken by each disjunct in H if they are equivalent under O. For example, condition (iv) does not account for conjunctively joined redundancies that follow directly from O. If Example 2 is extended so that the axiom C D is in O and the signature of abducibles SA also contains D, then H3 = (B D)(a) is also a valid hypothesis under conditions (i), (ii) and (iv). While H3 is not stronger than H1, it contains a form of redundancy: D(a). To eliminate these redundancies and simplify the disjuncts themselves may require the use of preference criteria over the disjuncts in H. As there are a variety of methods for deﬁning and realising preference handling (Cialdea Mayer and Pirri 1996; Pino-Per ez and Uzc ategui 2003; Delgrande et al. 2004) we do not discuss this aspect. Here, the focus is on computing the space of independent explanations, rather than ensuring each takes the simplest form.

Forgetting and Uniform Interpolation Forgetting is a process of ﬁnding a compact representation of an ontology by hiding or removing subsets of symbols within it. Here, the term symbols refers to concept and role names present in the ontology. The symbols to be hidden are speciﬁed in the forgetting signature F, which is a subset of symbols in the ontology O. The symbols in F should be removed from O, while preserving all entailments of O that can be represented using the signature sig(O) without F. The result is a new ontology, which is a uniform interpolant:

Deﬁnition 2. Uniform Interpolation in ALC (Lutz and Wolter 2011). Let O be an ALC ontology and F a set of symbols to be forgotten from O. Let SA = sig(O) \ F be the complement of F. The uniform interpolation problem is the task of ﬁnding an ontology V such that the following conditions hold: (i) sig(V) SA, (ii) for any axiom β: O |= β iff V |= β provided that sig(β) SA. The ontology V is a uniform interpolant of O for the signature SA. We also say that V is the result of forgetting F from O.

Uniform interpolants are strongest necessary entailments, in general, it holds that:

Theorem 1. V is a uniform interpolant of ontology O for SA iff V is a strongest necessary entailment of O in SA.

This means that for any ontology V , if sig(V ) SA and V |= V, then V |= V . Of the methods for uniform interpolation in ALC, e.g., (Ludwig and Konev 2014; Koopmann and Schmidt 2015a), our abduction method uses

the resolution-based method developed by Koopmann and Schmidt [2013; 2015a; 2015b]. Here, this method is referred to as Int ALC. Motivations for utilising Int ALC include the fact that it can perform forgetting for ALC with ABoxes (Koopmann and Schmidt 2015a), making it suitable for the setting in this paper. Furthermore, in theory the result of forgetting (and abduction) can involve an inﬁnite chain of axioms. Using Int ALC, such chains can be ﬁnitely represented using ﬁxpoint operators. In practice, these are rarely required: in previous work only 7.2% of uniform interpolants contained cycles (Koopmann and Schmidt 2013). Int ALC can also handle disjunctive ABox assertions which are not representable in pure ALC. These will be needed for some abduction cases involving multiple individuals. In terms of efﬁciency, the size of the forgetting result is constrained to at most a double exponential bound with respect to the input ontology and Int ALC is guaranteed to terminate (Koopmann and Schmidt 2015a). The method Int ALC has two properties that are also essential to the proposed abduction method. (i) Soundness: any ontology O returned by applying Int ALC to an ontology O is a uniform interpolant. (ii) Interpolation Completeness: if there exists a uniform interpolant O of ontology O, then the result of Int ALC is an ontology V such that V O . Thus, for any ALC ontology O and any forgetting signature F, Int ALC always returns a ﬁnite uniform interpolant.

Resolution: C1 A(t1) C2 A(t2) (C1 C2)(σ)

Role Propagation: C1 ( r.D1)(t1) C2 Qr.D2(t2) (C1 C2)σ Qr.D12(t1σ)

-Role Restriction Elimination: C ( r.D)(t) D(x) C

Role Instantiation: C1 ( r.D)(t1) r(t2, b) C1σ D(b) D1 and D2 are deﬁner symbols, Q { , }, σ is the uniﬁer of t1 and t2 if it exists, D12 is a new deﬁner symbol for D1 D2 and no clause contains more than one negative deﬁner literal of the form D(x), and none of the form D(a).

Figure 1: Int ALC rules utilised in our abduction method.

The method Int ALC relies on the transformation of the ontology to a normal form given by a set of clauses of concept literals. The inference rules of the forgetting calculus utilised in Int ALC are shown in Figure 1. Deﬁner symbols are introduced to represent concepts that fall under the scope of a quantiﬁer. Resolution inferences are restricted to concepts in F or deﬁner symbols. Once all possible inferences have been made, any clauses containing symbols in F are removed and the deﬁner symbols are eliminated resulting in an ontology O that is free of all symbols in F. A discussion of this calculus and the associated method, including proofs, can be found in (Koopmann and Schmidt 2015a). We will also need the following notions. Each premise in an application of an inference rule in Int ALC is referred

to as a parent of the conclusion of the rule. The ancestor relation is deﬁned as the reﬂexive, transitive closure of the parent relation. For example, the premises {A B, C A, B(a)} are expressed as the clauses: { A(x) B(x), C(x) A(x), B(a)}. For a forgetting signature F = {B, A}, resolution between A(x) B(x) and B(a) gives A(a). Resolution between A(a) and C(x) A(x) gives C(a). The axioms A B and B(a) are the parents of the axiom A(a) and the ancestors of C(a). In this paper, we focus on ABox abduction where the set of abducibles includes all role symbols. Non-abducibles are speciﬁed by the forgetting signature F which contains only concept symbols occurring in the ontology O or observation ψ. The proposed method utilises Int ALC to compute semantically minimal hypotheses via forgetting and contrapositive reasoning, exploiting: O, H |= ψ iff O, ψ |= H where O is an ontology and ψ, H are (ABox) axioms.

A Forgetting-Based Abduction Method The abduction algorithm takes as input an ALC ontology O, an observation ψ as a set of ABox axioms and a forgetting signature F. Several assumptions are made regarding this input. The method Int ALC does not cater for negated role assertions as can be seen in Figure 1, and the form of role forgetting in Int ALC is not complete for abduction. As a result, ψ cannot contain role assertions and F is restricted to concept symbols in sig(O ψ). Correspondingly, the signature of abducibles SA must contain all role symbols occurring in sig(O ψ). Also, if F does not contain at least one symbol in the observation ψ, the semantically minimal hypothesis will simply be ψ itself, i.e., H = ψ. This is reﬂected in the fact that no inferences would occur between O and ψ under Int ALC. To avoid this trivial hypothesis, F should contain at least one concept symbol in the signature of ψ. In the event that F contains concepts that occur within a cycle in O, the forgetting result obtained using Int ALC may contain greatest ﬁxpoints (Koopmann and Schmidt 2013) to ﬁnitely represent inﬁnite forgetting solutions. For our method, this means that the abduction result may contain least ﬁxpoints due to the negation of greatest ﬁxpoints under contraposition. In these cases, the output language would be ALCµ. The output is a hypothesis H = α1(a1) ... αn(an) containing only the abducible symbols SA = sig(O ψ)\F, that satisﬁes the conditions (i) (iv) in Deﬁnition 1. Note that H may be a disjunctive assertion over several individuals, motivating the need to extend ALC with these. The algorithm reduces the task of computing abductive hypotheses for the observation ψ to the task of forgetting, using the following steps:

(1) Compute the uniform interpolant V = {β1, ..., βn} of (O, ψ) with respect to the forgetting signature F.

(2) Extract the set V V by omitting axioms βi V such that O, β1, ..., βi 1, βi+1, ..., βn |= βi.

(3) Obtain the hypothesis H by negating the set V .

In more detail, the observation ψ takes the form of a set of ABox axioms: ψ = {C1(a1), ..., Ck(ak)} where the Ci are ALC concepts and the ai are individuals. The negation

takes the form ψ = C1(a1) ... Ck(ak). The forgetting method Int ALC is used to compute the uniform interpolant V of (O, ψ) by forgetting the concept names in F, i.e., V = (O, ψ) F. If forgetting was used in isolation, the negation of V would be the hypothesis for ψ under contraposition. However, this is only guaranteed to satisfy conditions (ii) and (iv) of Deﬁnition 1: since V is the strongest necessary entailment of (O, ψ) in SA as in Theorem 1, its negation would be the weakest sufﬁcient condition (Lin 2001; Doherty, Łukaszewicz, and Szałas 2001). Thus the hypothesis would be semantically minimal in SA, but would not necessarily satisfy condition (i), consistency, nor condition (iii), absence of inter-disjunct redundancy. In practice most of the disjuncts will be redundant, as the experimental results show (Table 2). In the case that there is no suitable hypothesis, an inconsistent or false hypothesis will be returned since all of the axioms in V would follow directly from O. Step (2) therefore omits information in V that follows from the background knowledge O together with other axioms in V itself. This check is the dual of Deﬁnition 1(iii), and therefore eliminates inter-disjunct redundancies such as those in Example 1. The result is a reduced uniform interpolant V which takes the form V = {β1(a1), ..., βk(ak)} where each βi is an ALC(µ) concept. If an axiom βi is redundant, it is removed from V immediately. For the following disjuncts, the check is performed against the remaining axioms in V. This avoids discarding too many axioms: if multiple axioms express the same information, i.e. are equivalent under O, one of them should be retained in the ﬁnal hypothesis H. The order in which the axioms are checked can be random, or can be based on some preference relation (Cialdea Mayer and Pirri 1996). In Step (3) the reduced uniform interpolant V is negated, resulting in the hypothesis H. Thus, each disjunct αi in H is the negation of an axiom βi in V , i.e., αi βi. The described method is sound and complete.

Theorem 2. Let O be an ALC ontology, ψ an observation as a set of ABox axioms, excluding role assertions, and SA a set of abducible symbols containing all role symbols in O, ψ and SA sig(O, ψ). (i) Soundness: The hypothesis H returned by the method is a disjunction of ABox axioms such that sig(H) SA and H satisﬁes Deﬁnition 1(i)-(iv). (ii) Completeness: If there exists a hypothesis H such that sig(H ) SA and H satisﬁes Deﬁnition 1(i) (iv), then the method returns a hypothesis H such that O, H O, H .

Theorem 3. In the worst case, computing a hypothesis H using our method has 3EXPTIME upper bound complexity for running time and the size of H can be double exponential in the size of (O, ψ).

Practical Realisation For redundancy elimination, Step (2) requires checking the relation O, V\βi |= βi for every axiom βi in V. Since entailment checking in ALC has exponential complexity and V is in the worst case double exponential in the size of (O, ψ), this step has a 3EXPTIME upper bound which is very expensive particularly for large ontologies. Regardless, Step (2) is

essential; without it there will be a large number of interdisjunct redundancies (Deﬁnition 1(iii)) in the hypotheses obtained. This is reﬂected in the experiments (Table 2). To obtain a computationally feasible implementation of Step (2), the number of entailment checks performed must be reduced. Our implementation of this step begins by tracing the dependency of axioms in V on the negated observation ψ. An axiom β is deﬁned as dependent upon ψ if in the derivation using Int ALC it has at least one ancestor axiom in ψ. The set of axioms dependent on ψ is in general a superset of the reduced uniform interpolant V and is referred to as V app, i.e., an approximation of V . In this paper, dependency tracing is achieved by using annotations, similar to (Kazakov and Sko covsk y 2017; Koopmann and Chen 2017; Penaloza et al. 2017). These take the form of fresh concept names that do not occur in the signature of the ontology nor the observation. Annotations act as labels that are disjunctively appended to existing axioms. They are then used to trace which axioms are the ancestors of inferred axioms. This relies on the fact that the annotation concept is not included in the forgetting signature F. Thus, it will carry over from the parent to the result of any inference in Int ALC, as formalised in the following property:

Theorem 4. Let O be an ontology, ψ an observation as a set of ABox axioms, F a forgetting signature and ℓan annotator concept added as an extra disjunct to each clause in the clausal form of ψ where ℓ sig(O ψ) and ℓ F. For every axiom β in the uniform interpolant V = (O, ψ) F, β is dependent on ψ iff ℓ sig(β).

Therefore, the presence of the annotation concept in the signature of an inferred axiom indicates that the axiom has at least one ancestor in ψ. Since the aim is to trace dependency speciﬁcally on ψ, only clauses that are part of ψ need to be annotated. As it is not important which speciﬁc clauses in ψ were used in the derivation of dependent axioms, only one annotation concept name is required. This will be referred to as ℓ. Using this technique, the process of extracting V app from the uniform interpolant V is a matter of removing all axioms in V that do not contain ℓ. Then, ℓcan be replaced with to obtain the annotation-free set V app. Since this annotation based ﬁltering is sound, i.e., it only removes axioms that are not dependent on ψ, as these are directly derivable from O and are thus guaranteed to be redundant, it can be used at the start of Step (2) to compute V app. To guarantee the computation of the reduced uniform interpolant V , the entailment check in Step (2) must then be performed for each axiom β V app to eliminate any redundancies not captured by the annotation-based ﬁltering. Since some axioms may have multiple derivations, they can contain the annotation concept but still be redundant with respect to Deﬁnition 1. For example:

Example 3. Let O = {A C, B C, A D , D(a)} and ψ = C(a). The annotated form of ψ is ψ = ℓ C(a). Using F = {C}, the result of Step (1) is V = {A D , D(a), (ℓ A)(a), (ℓ B)(a)}. Note: no inference is made with D(a), since D F. In Step (2) extracting all axioms with annotations and setting ℓ= gives the set { A(a), B(a)}. Despite A(a) being deriv-

able using ψ, it follows from the original ontology O and is therefore redundant with respect to Deﬁnition 1(iii). This can now be removed via the entailment check in Step (2). This method of ﬁltering out redundancies has several advantages. First, it is not speciﬁc to ALC and can be applied if the abduction method is later extended to more expressive logics. Second, by removing axioms that are not dependent on ψ, the method reduces the cost of Step (2) as checking the signature of each axiom for the presence of ℓis linear in the size of V. In the worst case V app could be equal to V and a double exponential number of entailment checks would still be required. In practice, this is unlikely as V app is usually a small fraction of V as shown by the experiments (Table 2). In these cases, each redundancy eliminated from V to V app replaces an exponential check with a linear one. The entailment checks that must be performed on V app to compute V may still be costly in the event that many axioms are dependent on ψ in V. Therefore, we propose that in some cases it may be pragmatic to relax the allowed hypotheses by negating V app instead of the reduced uniform interpolant V itself. In this case, an additional check, O, H |= , is required to rule out inconsistent hypotheses if all of the axioms in V app are redundant. This approximate approach results in a hypothesis Happ which satisﬁes conditions (i), (ii) and (iv) in Deﬁnition 1, but not condition (iii). The results in Table 2 illustrate the effect in practice. To summarise, we suggest two realisations of Step (2) of the proposed abduction method: (a) approximate ﬁltering, which computes an approximation of the hypothesis Happ by negating V app, (b) full ﬁltering, which performs the entailment check in Step (2) for each axiom in V app to obtain V and thus H which is guaranteed to fully satisfy Deﬁnition 1. Note that for setting (b), the approximation step is still used to reduce the overall cost of Step (2).

Experimental Evaluation

Ontology DL TBox ABox Num. Num. Name Size Size Concepts Roles BFO EL 52 0 35 0 LUBM EL 87 0 44 24 HOM EL 83 0 66 0 DOID EL 7892 0 11663 15 SYN EL 15352 0 14462 0 ICF ALC 1910 6597 1597 41 Semintec ALC 199 65189 61 16 OBI ALC 28888 196 3691 67 NATPRO ALC 68565 42763 9464 12

Table 1: Characteristics of the experimental corpus.

A Java prototype was implemented using the OWLAPI1 and the forgetting tool LETHE which implements the Int ALC method.2 Using this, two experiments were carried out over a corpus of real world ontologies, which were preprocessed into their ALC fragments. Axioms not representable in ALC, such as number restrictions of the form

1http://owlapi.sourceforge.net/ 2http://www.cs.man.ac.uk/ koopmanp/lethe/index.html

Ont. Mean Time Taken /s Max Time Taken /s Mean Redund. Removed Size H /disjuncts Mean % of Name V app V V no app. V app V V no app. V V app V app V Mean Max Happ Redund. BFO 0.01 0.01 0.09 0.01 0.07 0.14 52 0 1.97 4 0 LUBM 0.02 0.03 0.30 0.11 0.16 1.21 90 0.80 2.73 11 29.30 HOM 0.03 0.05 0.18 0.40 0.54 0.86 82 0.03 2.07 13 1.45 DOID 0.44 1.09 1071.35 1.11 6.98 1095.07 7891 0 7.23 104 0 SYN 0.95 3.92 2421.96 2.33 61.52 2593.13 15351 0.03 20.63 457 0.15 ICF 0.30 0.56 t.o. 0.52 1.58 t.o. 8505 0 2.30 7 0 Semin. 3.13 5.12 t.o. 9.29 15.36 t.o. 72827 0.03 3.60 10 0.83 OBI* 3.82 32.17 t.o. 25.18 95.37 t.o. 29191 6.48 52.48 161 12.35 NATP. 26.54 179.70 t.o. 39.51 544.50 t.o. 111318 0.03 48.70 204 0.06

Table 2: Results for 30 observations using a forgetting signature size of 1. * indicates that LETHE did not terminate within the 300s time limit in at least one case, t.o. indicates that the experiment was terminated after several days runtime. The size of H reported is that obtained via full computation of V . Times shown are the total times taken to return H (or Happ).

nr.C where r is a role symbol and C is a concept symbol, were removed. Others were represented using appropriate ALC axioms where possible. For example, a range restriction r . C is converted to r.C, where r is the inverse role of r. The choice of ontologies was based on several factors. They must be consistent, parsable using LETHE and the OWL API and must vary in size to determine how this impacts performance. Since many realworld ontologies are encoded in less expressive DLs such as EL, the corpus was also split between EL and ALC to determine if the performance over EL suffers as a result of the additional capabilities of the method for ALC. The ﬁnal corpus contains ontologies from the NCBO Bioportal and OBO repositories,34 and the LUBM (Guo, Pan, and Heﬂin 2005) and Semintec ontologies.5 The corpus is summarised in Table 1. The experiments were performed on a machine using a 4.00GHz Intel Core i7-6700K CPU and 16GB RAM. For each ontology, 30 consistent, non-entailed observations were randomly generated using any ALC concepts from the associated ontology, some of which were combined using ALC operators to encourage variety. The aim was to emulate the information that may be observed in practice for each ontology, while adhering to the requirements for ψ expressed in Deﬁnition 1. As the current prototype uses the OWL-API, which does not allow disjunctive assertions over multiple individuals, the experiments here are limited to observations involving one individual. For the ﬁltering in Step (2), the preference relation used in these experiments was simply based on order of appearance of each disjunct. For the ﬁrst experiment, F was set to one random concept symbol from sig(ψ). The assumption was that users may ﬁrst seek the most general hypothesis, i.e., the semantically minimal hypothesis for the largest set of abducibles. This allows the user to pursue stronger hypotheses subsequently by forgetting further symbols from the initial hypothesis. This experiment is therefore also representative of incremental abduction steps using a small F. The second experiment was performed over the DOID, ICF and SYN ontologies to evaluate the performance as the size of F increases. These on-

3https://bioportal.bioontology.org/ 4http://www.obofoundry.org/ 5http://www.cs.put.poznan.pl/alawrynowicz/semintec.htm

tologies were used as they have a sufﬁciently large signature of concepts and LETHE did not time out when forgetting in any case. In all cases, at least one symbol from ψ was present in F to avoid trivial hypotheses. In both experiments, the approaches based on (a) approximate and (b) full ﬁltering were compared for the same observations and same random selection of F. Thus, the tradeoff between the additional time for entailment checking and redundancy in the ﬁnal hypothesis is evaluated. In all cases, LETHE was subject to a 300 second time limit. Table 2 shows the results for the ﬁrst experiment. For the smaller ontologies, the difference in time taken between the approximate and full ﬁltering was small. For the larger ontologies the cost of the full ﬁltering was more pronounced, taking 313%, 742% and 577% longer across the SYN, OBI and NATPRO ontologies respectively. In all cases, it can be seen that the annotation-based ﬁltering eliminated the majority of redundancies. In three cases (BFO, DOID, ICF), for all 30 observations the result of the approximation, V app, contained no redundancies and thus Happ = H. For the other ontologies, in most cases V app contained few redundancies in both absolute terms and relative to the size of the ﬁnal hypothesis. For the LUBM and OBI ontologies, however, these redundancies made up a more signiﬁcant portion of V app. The full ﬁltering setting still uses the annotation-based method as a preprocessing step. To assess the beneﬁt of this preprocessing, results for applying the entailment check in Step (2) directly to V instead of V app were collected and are shown in the V no app. columns. For the largest EL ontologies, the time taken increased signiﬁcantly, e.g., taking almost 1000 times longer for the DOID ontology. For all of the ALC ontologies the experiments were terminated after several days runtime, i.e., it took at least several hours to compute a single hypothesis on average. This indicates that the annotation-based ﬁltering signiﬁcantly reduces the time taken, particularly over large or more expressive ontologies. Figure 2 shows the results of the second experiment. The time taken for the forgetting step, Step (1), increased almost linearly with the size of F. This was expected due to a higher number of inferences needed to compute V. The time taken for ﬁltering, Step (2), did not increase with the size of F. However, for each ontology, maxima were observed for different sizes of F. This implies that including

Figure 2: Mean forgetting and ﬁltering times with varying F signature sizes for the ICF, DOID and SYN ontologies.

certain symbols in F increases the ﬁltering time. Forgetting commonly used concepts results in more inferences and a larger V, which may explain the maxima as the annotationbased ﬁltering depends solely on the number of axioms in V. The size of V app will also increase in these cases, leading to more exponential entailment checks for full ﬁltering. The full ﬁltering took an average of 27, 11 and 70 times longer than the approximate case for the DOID, ICF and SYN ontologies respectively. This indicates that the cost of the full entailment check increased with the size of the ontology, particularly the size of the TBox, not the size of F. In 100% of cases for both experiments the hypotheses were represented without ﬁxpoints, indicating that cyclic, semantically minimal hypotheses seem rare in practice.

Discussion The use of forgetting for abduction has been suggested in classical logics (Doherty, Łukaszewicz, and Szałas 2001; Gabbay, Schmidt, and Szałas 2008; Wernhard 2013), and a form of TBox abduction (Koopmann and Schmidt 2015b). Our work extends on these suggestions in several ways. As the focus is on large DL ontologies, and not small theories in classical logics, an interpretable hypothesis cannot be obtained by negating the forgetting result V as most of it will be redundant (Table 2). Thus, we gain insight into the redundancies in V in terms of abductive notions, such as (Konolige 1992; Halland, Britz, and Klarman 2014), resulting in Deﬁnition 1(iii) and (iv). Efﬁcient redundancy removal is achieved via the annotation-based ﬁltering. The overall approach, including two options emphasising (a) practicality and (b) full redundancy removal, is then evaluated over a corpus of real-world ontologies. This gives us the ﬁrst realisation and evaluation of a practical forgetting-based approach to ABox abduction in DL ontologies. Restricting inferences in Int ALC to axioms dependent on ψ, rather than ﬁltering the output, was considered. However, this would not circumvent the need to perform entailment checking, as illustrated in Example 3. Second, computing the full uniform interpolant V has an interesting use case: iterative abduction. For example: Example 4. Let O = {A C, B C, C D} and ψ = D(a ). In Step (1), using F={D} results in V={A C, B C, C(a )}. Steps (2) (3) result in H = C(a ).

Now, forgetting F2 = {C} from V of the previous iteration results in V2 = { A(a ), B(a )}. Repeating Steps (2) and (3) gives H2 = (A B)(a ), which is stronger than H and is the same as the result of computing the uniform interpolant of (O, ψ) using F = {D, C}, but will be more efﬁcient. This iterative process enables hypothesis reﬁnement, and has potential synergy with induction. Data could inform the selection of new forgetting signatures to ﬁnd stronger hypotheses following from prior likely hypotheses: a cycle of abduction, deduction and induction. Limitations include the lack of role assertions in the observations and hypotheses, due to the inability of Int ALC to handle negated role assertions, and the incompleteness of role forgetting for abduction, as illustrated by the following: Example 5. Let O = {C r.D} and ψ = r.D(a). Using F = {r} the result of Step (1) is V = . This is due to the fact that no inferences are possible on the symbol D, since resolution is restricted to F. Thus, the hypothesis obtained is H = , while the expected result is H = C(a). With the use of nominals, this limitation can be overcome. Options include the use of other forgetting approaches (Zhao and Schmidt 2015; 2016) or the extension of Int ALC. It should be noted that methods such as (Klarman, Endriss, and Schlobach 2011; Pukancov a and Homola 2017) can already handle role assertions. The former is a purely theoretical work, which restricts the abductive observations and solutions to ALE: the fragment of ALC without disjunctions of concepts and allowing only atomic negation. The method of (Pukancov a and Homola 2017) performs abductive reasoning up to ALCHO, restricting observations and hypotheses to atomic and negated atomic concept and role assertions. This method considers syntactic, but not semantic, minimality, though the authors note the importance of semantic minimality in practical applications.

Conclusion and Future Work In this paper, a practical method for ABox abduction in ALC ontologies was presented. The method computes semantically minimal hypotheses with independent disjuncts to explain observations, where both may contain complex ALC concepts but not role assertions, and the set of abducibles must contain all role symbols. The practicality of the method, including the proposed annotation-based ﬁltering, was evaluated over a corpus of real-world ontologies. To the best of our knowledge, this is the ﬁrst method that computes such hypotheses efﬁciently in large ontologies. The ability to produce a semantically minimal space of independent explanations will likely be beneﬁcial in real-world applications as it can, e.g., provide engineers with multiple, non-redundant suggestions for ﬁxing errors in an ontology or explaining negative query results, even over large knowledge bases. For scientiﬁc investigation using ontologies, the ability to produce independent avenues of explanation starting with the least assumptions necessary captures the essence of scientiﬁc hypothesis formation. The ability to reﬁne these hypotheses via repeated forgetting also provides a goal-oriented, potentially data driven, way to derive stronger insights from the hypotheses produced.

Future work will include removing the restriction on role assertions. Also, though forgetting in DLs can be applied to a form of TBox abduction (Koopmann and Schmidt 2015b), the hypotheses take the form α1 ... αn where each α is an ALC concept. Thus, the problem of determining inter-disjunct redundancy and the proposed approach differ in several aspects. This will be investigated, as will the iterative abduction use case.

Bienvenu, M. 2008. Complexity of abduction in the EL family of lightweight description logics. In Proc. KR 08, 220 230. AAAI Press.

Calvanese, D.; Ortiz, M.; Simkus, M.; and Stefanoni, G. 2013. Reasoning about explanations for negative query answers in DLLite. J. Artiﬁcial Intelligence Research 48:635 669.

Calvanese, D.; De Giacomo, G.; and Lenzerini, M. 1999. Reasoning in expressive description logics with ﬁxpoints based on automata on ﬁnite trees. In Proc. IJCAI 99, 84 89. AAAI Press.

Cialdea Mayer, M., and Pirri, F. 1996. Abduction is not deduction in reverse. Journal of the IGPL 4:95 108.

Delgrande, J.; Tompits, H.; Schaub, T.; and Kewen, W. 2004. A classiﬁcation and survey of preference handling approaches in nonmonotonic reasoning. Computational Intelligence 20:308 334.

Doherty, P.; Łukaszewicz, W.; and Szałas, A. 2001. Computing strongest necessary and weakest sufﬁcient conditions of ﬁrst-order formulas. In Proc. IJCAI 01, 145 151. AAAI Press.

Du, J.; Wan, H.; and Ma, H. 2017. Practical TBox abduction based on justiﬁcation patterns. In Proc. AAAI 17, 1100 1106. AAAI Press.

Du, J.; Wang, K.; and Shen, Y. 2014. A tractable approach to ABox abduction over description logic ontologies. In Proc. AAAI 14, 1034 1040. AAAI Press.

Elsenbroich, C.; Kutz, O.; and Sattler, U. 2006. A case for abductive reasoning over ontologies. In Proc. OWL: Experiences and Directions, volume 216. CEUR Workshop Proceedings.

Gabbay, D. M.; Schmidt, R. A.; and Szałas, A. 2008. Second-order quantiﬁer elimination: Foundations, computational aspects and applications. College Publications 12.

Guo, Y.; Pan, Z.; and Heﬂin, J. 2005. LUBM: A benchmark for OWL knowledge base systems. J. Web Semantics 3:158 182.

Halland, K., and Britz, K. 2012. ABox abduction in ALC using a DL tableau. In Proc. SAICSIT 12, 51 58. ACM.

Halland, K.; Britz, K.; and Klarman, S. 2014. TBox abduction in ALC using a DL tableau. In Proc. DL 14, volume 1193, 556 566. CEUR Workshop Proceedings.

Hobbs, J. R.; Stickel, M.; Martin, P.; and Edwards, D. 1993. Interpretation as abduction. Artiﬁcial Intelligence 63:69 142.

Kakas, A.; Kowalski, R.; and Toni, F. 1992. Abductive logic programming. J. Logic and Computation 2 (6):719 770.

Kazakov, Y., and Sko covsk y, P. 2017. Enumerating justiﬁcations using resolution. In Proc. DL 17, volume 1879. CEUR Workshop Proceedings.

Klarman, S.; Endriss, U.; and Schlobach, S. 2011. ABox abduction in the description logic ALC. J. Automated Reasoning 46:43 80.

Konolige, K. 1992. Abduction versus closure in causal theories. Artiﬁcial Intelligence 53:255 272.

Koopmann, P., and Chen, J. 2017. Computing ALCHSubsumption modules using uniform interpolation. In Proc. SOQE 17, volume 2013, 51 66. CEUR Workshop Proceedings. Koopmann, P., and Schmidt, R. A. 2013. Uniform interpolation of ALC ontologies using ﬁxpoints. In Proc. Fro Co S 13, volume 8152 of LNCS, 87 102. Springer. Koopmann, P., and Schmidt, R. A. 2015a. Uniform interpolation and forgetting for ALC ontologies with ABoxes. In Proc. AAAI 15, 175 181. AAAI Press. Koopmann, P., and Schmidt, R. A. 2015b. LETHE: Saturation based reasoning for non-standard reasoning tasks. In Proc. ORE 15, volume 1387, 23 30. CEUR Workshop Proceedings. Lambrix, P.; Dragisic, Z.; and Ivanova, V. 2012. Get my pizza right: Repairing missing is-a relations in ALC ontologies. In Proc. JIST 12, volume 7774 of LNCS, 17 32. Springer. Lin, F. 2001. On strongest necessary and weakest sufﬁcient conditions. Artiﬁcial Intelligence 128:143 159. Ludwig, M., and Konev, B. 2014. Practical uniform interpolation and forgetting for ALC TBoxes with applications to logical difference. In Proc. KR 14, 318 327. AAAI Press. Lutz, C., and Wolter, F. 2011. Foundations for uniform interpolation and forgetting in expressive description logics. In Proc. IJCAI 11, 989 995. AAAI Press. Mooney, R. 2000. Integrating abduction and induction in machine learning. In Abduction and Induction, 181 191. P. A. Flach and A. C. Kakas, Eds. Kluwer. Muggleton, S., and Bryant, C. 2000. Theory completion using inverse entailment. In Proc. ILP 00, volume 1866 of LNCS, 130 146. Springer. Peirce, C. S. 1878. Deduction, induction and hypothesis. Popular Science Monthly 13:470 482. Penaloza, R.; Menc ıa, C.; Ignatiev, A.; and Marques-Silva, J. 2017. Lean kernels in description logics. In Proc. ESWC 17, volume 10249 of LNCS, 518 533. Springer. Pino-Per ez, R., and Uzc ategui, C. 2003. Preferences and explanations. Artiﬁcial Intelligence 149:1 30. Pukancov a, J., and Homola, M. 2017. Tableau-based ABox abduction for the ALCHO description logic. In Proc. DL 17, volume 1879. CEUR Workshop Proceedings. Raghavan, S., and Mooney, R. 2010. Bayesian abductive logic programs. In AAAI 10 Workshop on Statistical Relational AI, 82 87. AAAI Press. Ray, O. 2009. Nonmonotonic abductive inductive learning. J. Applied Logic 7:329 340. Stickel, M. 1991. A Prolog-like inference system for computing minimum-cost abductive explanations in natural-language interpretation. Ann. Math. and Artiﬁcial Intelligence 4:89 106. Wei-Kleiner, F.; Dragisic, Z.; and Lambrix, P. 2014. Abduction framework for repairing incomplete EL ontologies: Complexity results and algorithms. In Proc. AAAI 14, 1120 1127. AAAI Press. Wernhard, C. 2013. Abduction in logic programming as secondorder quantiﬁer elimination. In Proc. Fro Co S 13, volume 8152 of LNCS, 103 119. Springer. Zhao, Y., and Schmidt, R. A. 2015. Concept forgetting in ALCOIontologies using an Ackermann approach. In Proc. ISWC 15, volume 9366 of LNCS, 587 602. Springer. Zhao, Y., and Schmidt, R. A. 2016. Forgetting concept and role symbols in ALCOIHµ+( , )-ontologies. In Proc. IJCAI 16, 1345 1352. AAAI Press.