Forgetting-Based Abduction in ALC-Ontologies (Extended Abstract)

Abstract

This paper presents a method for abduction in description logic ontologies. The method is based on forgetting and contrapositive reasoning and can produce semantically minimal hypotheses for TBox and ABox abduction in the description logic ALC. The method is not restricted to Horn clauses or atomic observations and hypotheses. Key considerations when using forgetting for abduction are addressed. A Java prototype has been implemented, making use of the resolution-based forgetting method implemented in the tool LETHE. Experimental results over a corpus of ontologies show the practicality of the method across a number of scenarios.

Introduction

The aim of abduction is to compute a hypothesis to explain a new observation. This task is usually split into the tasks of TBox and ABox abduction, for which the observation ψ and the hypothesis H take the form of sets of TBox axioms and ABox axioms respectively [ 2 ]. Two of the most common requirements are expressed in conditions (i) and (ii) of Definition 1 [ 13, 5 ], which is the form of the abduction problem considered in this paper.

Definition 1. Abduction in Ontologies. Let O be an ontology, SA be a set of abducible symbols, and ψ an ABox or TBox axiom such that O, ψ 6|=⊥ and O 6|= ψ. The abduction problem is to find a hypothesis H in the form of a set of axioms, consisting only of symbols in SA, such that: (i) O, H 6|=⊥, (ii) O, H |= ψ and (iii) there is no other hypothesis H0 such that sig(H0) ⊆ SA, O, H0 |= ψ and H |= H0, unless O, H0 ≡ O, H.

The condition O, ψ 6|=⊥ ensures that neither the ontology itself nor the ontology with the observation entail false, otherwise everything follows. The condition O 6|= ψ imposes the constraint that the observation should not already follow from the original ontology, otherwise the problem is deductive and the abduction solution is simply H = >. For ALC, it is also worth noting that for ABox abduction both ψ and H must take the form of ABox axioms, while in the case of TBox abduction both must take the form of TBox axioms.

Even with these conditions, the number of possible hypotheses is often intractably large. There is also the problem of finding the preferred hypotheses among these possible solutions. Thus, a variety of additional constraints are often considered to further restrict the space of abductive hypotheses [ 2 ].

The proposed method computes consistent, explanatory and semantically minimal hypotheses in accordance with Definition 1. The semantic minimality constraint in condition (iii) restricts the hypotheses to those that make the fewest assumptions, and is the “strong” semantic minimality constraint in [ 4 ]. This is a desirable characteristic for comparing hypotheses in many applications [ 14 ].

A set of abducibles is usually defined to further restrict the abductive hypotheses. The set of abducibles defines a subset of symbols in O that may appear in the hypothesis H. Here, the abducibles are defined by a forgetting signature, as the proposed method utilises forgetting to compute hypotheses that satisfy the conditions outlined for the abduction task in Definition 1. 3

Forgetting and Uniform Interpolation

Forgetting, also known as uniform interpolation, is a process of finding 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 in the signature of the ontology. The symbols to be hidden are defined by a forgetting signature F , which consists of 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 restricted signature sig(O)\F , resulting in a new ontology. Definition 2. Uniform Interpolation in ALC. Let O be an ALC-ontology and F a signature of symbols to be forgotten from O. Let SA = sig(O) \ F be the complement of F . The uniform interpolation problem [ 12 ] is the task of finding an ontology V such that the following conditions hold: (i) sig(V) ⊆ SA, (ii) for any set of axioms β: O |= β iff V |= β provided that sig(β) ⊆ SA. The ontology V is a uniform interpolant of O for the signature SA.

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

It is not necessarily the case that the source and target languages are the same. In [ 9 ] the uniform interpolant (or forgetting solution) of an ontology in ALC may need to be expressed in an extension of ALC, which includes the following additions: (i) fixpoint operators or definer symbols for representing cycles and (ii) disjunctions of ABox axioms. Here, “definer symbols” refer to new symbols that are not present in the original ontology. “Cycles” refer to uniform interpolants that are not finitely representable in ALC. However, evaluations on real-world ontologies have shown that the majority of uniform interpolants can be represented in pure ALC. In the case where the result does contain cycles, we represent this result using fixpoints. Thus, definer symbols do not appear in any of the uniform interpolants computed.

The proposed abduction method utilises the resolution-based forgetting method developed in [ 7–10 ], which can compute uniform interpolants of ALC ontologies by forgetting both concept and role symbols in the original ontology. Here, this method is referred to as IntALC . Two key characteristics for computing uniform interpolants that are essential to the proposed abduction method are as follows. Theorem 2. The uniform interpolation method has the following properties: (1) Soundness: any ontology O0 returned by applying IntALC to an ontology O is a uniform interpolant and hence satisfies criteria (i) and (ii) in Definition 2. (2) Interpolation Completeness: if there exists a uniform interpolant O0 of ontology O, then IntALC returns an ontology V such that V ≡ O0.

For any combination of an ALC ontology O and forgetting signature F , IntALC returns a finite uniform interpolant [ 9, 6 ].

The method IntALC relies on the transformation of the ontology to a normal form given by a set of clauses of concept literals. The rules of the forgetting calculus utilised in IntALC can be found in [ 9 ]. Definer symbols are introduced to represent concepts that occur under the scope of a quantifier. Resolution inferences are then made on literals including the symbols present in F and the definer symbols. Once all possible inferences have been made, any clauses containing symbols in F are removed and the definer symbols are eliminated resulting in an ontology O0 that is free of all symbols in F . 4

A Forgetting-Based Abduction Method

The resolution-based nature of the IntALC makes it well suited to abduction via contrapositive reasoning. The calculus is applicable not only to TBox abduction [ 10 ], but also to ABox abduction in a single unified framework. Algorithm 1 below outlines our forgetting-based method which utilises IntALC to compute semantically minimal abductive hypotheses by exploiting contrapositive reasoning as shown in the following theorem.

Theorem 3. Let O be an ontology, ψ an observation and H a hypothesis. Then the following holds: O, H |= ψ iff O, ¬ψ |= ¬H.

Algorithm 1 Forgetting-Based Abduction. The algorithm computes hypothesis H for an observation ψ relative to ontology O. It is assumed that ψ is a single axiom, which can also be a conjunction of assertions over a single individual “a” which does not occur in the ontology O. Two cases are considered: (i) ψ is an ABox axiom C(a) or (ii) ψ is a TBox axiom C v D where C and D can be any atomic or complex ALC concepts. The steps for both cases (i) and (ii) are as follows: 1. Negate the observation to obtain ¬ψ. In case (i) ¬ψ = ¬C(a), while in case (ii) ¬ψ = (C u ¬D)(a). 2. Choose a forgetting signature set F such that F ∩ sig(¬ψ) 6= ∅, where at least one of the symbols in both F and ¬ψ occurs with opposite polarity in the ontology O. Let SA = sig(O) \ F . 3. Use IntALC to compute a uniform interpolant of (O, ¬ψ) for SA by forgetting the symbols in F . 4. Let V be the uniform interpolant computed. Apply filtering to V to obtain the set of axioms V∗ ⊆ V that are dependent on ¬ψ. This means that the axioms in V∗ are conclusions of inferences in IntALC with clauses from ¬ψ. 5. Assuming V∗ = {α1(a), ..., αk(a)}, let (i) HI = (α1 t ... t αk)(a) when ψ is an ABox axiom, and (ii) HI = > v (α1 t ... t αk) when ψ is a TBox axiom, where αi ≡ ¬αi for any 1 ≤ i ≤ k. 6. In the case (i) of ABox abduction, let Hf = HI . In the case (ii) of TBox abduction, an additional check is needed to ensure consistency of the hypothesis: O, HI 6|=⊥. If this succeeds, then Hf = HI .

This procedure can be performed iteratively over a set of observations. In the event that cycles involving definer symbols occur in V, these will be represented using fixpoint operators. It is important to note that F must contain at least one symbol in the observation ψ, as described in step 2. This enables the computation of inferences between the ontology O and the negated observation ¬ψ using IntALC , ensuring that the set of axioms V∗ is computed. Otherwise, the trivial hypothesis Hf = ψ will be obtained. It is also worth noting the choice of representation for the negated observation ¬ψ. For ABox abduction, the negation of an ABox axiom ψ = C(a) is simply ¬ψ = ¬C(a). For TBox abduction, the negation of a TBox axiom ψ = C v D can be represented in several ways [ 10 ]: we choose to include a fresh individual name a and represent as an ABox axiom ¬ψ = (C u ¬D)(a). Thus, for both TBox and ABox abduction ¬ψ takes the form of an ABox axiom. This choice is exploited in the extraction of V∗ from the uniform interpolant V, as described in the next section.

The exclusion of role assertions is due to the fact that the method IntALC does not cater directly for negated role assertions. As a result, observations containing role assertions cannot currently be handled by our abduction method. 5

Extraction of V ∗ from V Many of the entailments in V do not involve inferences with the negated observation ¬ψ. These entailments do not contribute towards an explanation for ψ, and must be removed to reduce redundancy and guarantee consistency of the hypothesis returned. This leaves the set of axioms V∗, which consists of axioms obtained by inferences in IntALC with either clauses in ¬ψ or with clauses previously derived by inferences with ¬ψ.

There are several ways to remove the unnecessary axioms in V∗. These include checking the consistency of each disjunct in HI with the ontology O with an external reasoner or performing subsumption deletion between axioms in V and those in O. Both of these methods are computationally expensive, particularly as there are often a large number of axioms in V. A third possibility is to trace the dependency on ¬ψ as the inferences are performed in IntALC . However, an alternate method was devised to eliminate these guaranteed redundancies without relying on an external reasoner, subsumption deletion or dependency tracing. This method utilises a property of the forgetting calculus IntALC . Theorem 4. Efficient Filtering of V. Let O, ψ and V be defined as in Algorithm 1, where ¬ψ is an ABox axiom ¬C(a). For any α in the uniform interpolant V, α ∈ V∗ iff the signature sigI (α) of individuals contains a.

After computing the set of axioms V∗, this set is negated to obtain a hypothesis HI , exploiting contrapositive reasoning as in Theorem 3. This is outlined in step 5 of Algorithm 1. We have that O, ¬ψ |= V∗ iff O, HI |= ψ where ¬V∗ ≡ HI .

In the ABox abduction case, the unnecessary axioms in V \ V∗ account for all possible inconsistencies in HI , and no further processing is required. This was confirmed empirically by the lack of any difference between HI and Hf in the experimental evaluations in Tables 2 and 3. HI represents the hypothesis prior to the following additional check of O, HI 6|=⊥. For TBox abduction, this test is needed to ensure that the hypothesis returned by the system is not inconsistent with the original ontology. This is due to the transformation from an ABox assertion to a TBox axiom > v (α1 t ... t αk) described in step 5 of Algorithm 1. This transformation is necessary as in ALC, if the observation ψ is a TBox axiom then the hypothesis must also be a TBox axiom to ensure the condition in Definition 1(ii) is satisfied. 6

Properties of Method

Key properties of the abduction method are presented here. These properties hold for consistent ALC ontologies and the characteristics of the computed hypotheses are relative to the signature defined by eliminating the symbols contained within the chosen forgetting signature F . If cycles occur in uniform interpolants, these are represented using fixpoint operators.

The proposed abduction method computes semantically minimal hypotheses. This can be seen in terms of strongest necessary and weakest sufficient conditions [ 11, 1 ]. The uniform interpolant computed by IntALC is the strongest necessary set of entailments of the original ontology, as in Theorem 1. Thus, the axioms V∗ can be seen as a set of strongest necessary entailments of (O, ¬ψ) that depend upon the observation ψ. As discussed in [ 11 ], strongest necessary and weakest sufficient conditions are dual conditions. Thus, by negating the set of axioms V∗ under contrapositive reasoning, a weakest sufficient hypothesis Hf is obtained. Theorem 5. Let O, ψ, HI and Hf be defined as in Algorithm 1. The following conditions hold for the hypothesis Hf : (i) O, Hf 6|=⊥, (ii) O, Hf |= ψ and (iii) Hf is a weakest sufficient explanation, i.e, if there is a H such that (i) and (ii) hold and Hf |= H, then O, Hf ≡ O, H.

Theorem 6. Completeness with respect to SA. For an ontology O and observation ψ, if there exists a consistent, semantically minimal hypothesis H0 within the signature SA = sig(O) \ F such that (O, H0) |= ψ, then the proposed method returns a hypothesis Hf such that Hf ≡ H0.

Several other properties of the method are worth noting. Firstly, in the case that ψ is an ABox axiom, each disjunct αi(a) in the final hypothesis Hf is also a hypothesis since O, αi(a) |= O, (α1 t ... t αk)(a) for 1 ≤ i ≤ k. Secondly, it is possible to iteratively compute semantically stronger hypotheses due to the fact that symbols are iteratively eliminated in the forgetting loop of IntALC .

Below is an example of an ABox abduction problem by [ 14, 15 ], used to illustrate the abduction procedure given by Algorithm 1 and the semantic minimality of the hypothesis returned.

Example 1. Consider the following ontology O, consisting of two TBox axioms β1 and β2, and the observation ψ: β1: Professor t Scientist v Academic β2: AssocProfessor v Professor ψ : Academic(Jack) The steps in applying the proposed method are as follows: (1) Negate ψ to obtain ¬Academic(Jack). (2) Choose a forgetting signature F such that F ∩sig(¬ψ) 6= ∅, in this case: F = {Academic}. (3) Obtain the uniform interpolant V by applying IntALC to (O, ¬ψ) with the forgetting signature F . Using F = {Academic}, the following uniform interpolant V is obtained with IntALC : α1: AssocProfessor v Professor α2: ¬ Professor(Jack) α3: ¬ Scientist(Jack) (4) Obtain the set of axioms V∗ that are dependent on ¬ψ by applying the filtering described in Theorem 4 to the uniform interpolant V. The first entailment α1 is filtered out as it follows directly from the ontology O and does not contain the individual observed: Jack. The entailments α2 and α3 are dependent on ¬ψ and are retained. (5) Negate V∗ to obtain a hypothesis HI :

HI = (Professor t Scientist)(Jack). (6) In this case, ψ is an ABox axiom as in case (i) of Algorithm 1. Thus, no further checks are required and HI = Hf .

The disjuncts of the hypothesis in this example are also (stronger) hypotheses: Professor(Jack) and Scientist(Jack), as is the conjunction of these two. 7

Experimental Evaluation

A Java prototype was implemented using the OWL-API1 and the library of the utilised forgetting method: LETHE2. A set of experiments was then carried out over ontologies from the NCBO BioPortal3 and OBO 4 repositories, plus the LUBM benchmark [ 3 ] and Semintec 5 financial ontologies. The ontologies were converted to their ALC fragments: axioms not representable in ALC were deleted while others, such as domain and range restrictions, were replaced by equivalent ALC axioms. The characteristics of the resulting corpus are shown in Table 1. The experiments were performed on a machine using a 4.00GHz Intel Core i7-6700K CPU with 16GB of RAM.

For each ontology, 30 observations were generated. For TBox abduction, each set of observations contained random TBox axioms from the associated ontology, consisting of atomic or complex concepts. For each individual test, the TBox axiom was first removed from the ontology then used as an observation. For ABox abduction, observations were randomly generated using assertions or arbitrary concepts in the ontology. This was done to emulate information that may be observed in practice. F was limited to the smallest possible signature: a randomly 1 http://owlapi.sourceforge.net/ 2 http://www.cs.man.ac.uk/∼koopmanp/lethe/index.html 3 https://bioportal.bioontology.org/ 4 http://www.obofoundry.org/ 5 http://www.cs.put.poznan.pl/alawrynowicz/semintec.htm selected concept symbol from ψ. The assumption was that a user may begin by finding the most general hypotheses, which has the benefit that stronger hypotheses can be found using the iterative abduction process described earlier.

The results are shown in Table 2. In almost all cases a semantically minimal hypothesis was computed within the time limit on LETHE. For the OBI ontology, for two TBox and five ABox cases, LETHE timed out before a uniform interpolant was computed. Given more time a uniform interpolant would be found. The time taken to compute Hf varied considerably with the ontology size, as did the size of Hf . The difference between the number of axioms filtered and the size of Hf , particularly for the larger ontologies, supports the need for efficient filtering such as the proposal in Theorem 4. The sizes of HI and Hf were equal for the ABox abduction results, indicating that all unnecessary entailments in the uniform interpolants were removed by the proposed filtering. For TBox abduction the two values were different in all cases, leaving room for improvement in the filtering used to avoid the need for additional checks on HI . In this paper, a method for performing both TBox and ABox abduction in ALC ontologies was presented. The method uses forgetting and can compute complex hypotheses to explain both atomic and complex observations. The computed hypotheses were shown to be semantically minimal within a specified set of symbols. The practicality of the method was illustrated empirically across a corpus of real-world ontologies.

The method will be extended to perform abduction in more expressive description logics and to handle statements involving role assertions. These aims will likely be achieved by extending the IntALC calculus [ 9 ] to handle negated role assertions. Another option would be to investigate other methods for forgetting [ 16 ]. Another aim is to investigate the use of the iterative abduction procedure described earlier to compute increasingly stronger hypotheses.

References

1. Doherty , P. , Lukaszewicz , W. , Szalas , A. : Computing strongest necessary and weakest sufficient conditions of first-order formulas . In: Proc. IJCAI'01 . pp. 145 - 151 . AAAI Press ( 2001 )

2. Elsenbroich , C. , Kutz , O. , Sattler , U. : A case for abductive reasoning over ontologies . In: Proc. OWL: Experiences and Directions ( 2006 )

3. Guo , Y. , Pan , Z. , Heflin , J.: LUBM: A benchmark for OWL knowledge base systems . Journal of Web Semantics: Science, Services and Agents on the World Wide Web 3 , 158 - 182 ( 2005 )

4. Halland , K. , Britz , A. , Klarman , S. : Tbox abduction in ALC using a DL tableau . In: Proc. DL'14 . pp. 556 - 566 . CEUR-WS.org ( 2014 )

5. Klarman , S. , Endriss , U. , Schlobach , S. : Abox abduction in the description logic ALC . Journal of Automated Reasoning 46 , 43 - 80 ( 2011 )

6. Koopmann , P. : Practical Uniform Interpolation for Expressive Description Logics . Ph.D. thesis , The University of Manchester, UK ( 2015 )

7. Koopmann , P. , Schmidt , R.A. : Forgetting concept and role symbols in ALCHontologies . In: LPAR'13. LNCS , vol. 8312 , pp. 552 - 567 . Springer ( 2013 )

8. Koopmann , P. , Schmidt , R.A. : Uniform interpolation of ALC ontologies using fixpoints . In: Proc. FroCoS13. LNCS , vol. 8152 , pp. 87 - 102 . Springer ( 2013 )

9. Koopmann , P. , Schmidt , R.A. : Uniform interpolation and forgetting for ALC ontologies with ABoxes . In: Proc. AAAI'15 . pp. 175 - 181 . AAAI Press ( 2015 )

10. Koopmann , P. , Schmidt , R.A. : LETHE: Saturation based reasoning for nonstandard reasoning tasks . In: Proc. ORE'15 . pp. 23 - 30 . CEUR-WS.org ( 2015 )

11. Lin , F. : On strongest necessary and weakest sufficient conditions . Artificial Intelligence 128 pp. 143 - 159 ( 2001 )

12. Lutz , C. , Wolter , F. : Foundations for uniform interpolation and forgetting in expressive description logics . In: Proc. IJCAI'11 . pp. 989 - 995 . AAAI Press ( 2011 )

13. Mooney , R.J.: Integrating abduction and induction in machine learning . In: Abduction and Induction . pp. 181 - 191 . P. A. Flach and A. C. Kakas , Eds. Applied Logic Series. Kluwer ( 2000 )

14. Pukancova´, J. , Homola , M. : Tableau-based ABox abduction for description logics: preliminary report . In: Proc. DL'16. CEUR-WS.org ( 2016 )

15. Pukancova´, J. , Homola , M. : Tableau-based ABox abduction for the ALCHO description logic . In: Proc. DL ' 17 ,. CEUR-WS.org ( 2017 )

16. Zhao , Y. , Schmidt , R.: Forgetting concept and role symbols in ALCOIHμ+(∇, u)- ontologies . In: Proc. IJCAI'16 . AAAI Press ( 2016 )