A dependency-graph based approach for finding justification in OWL 2 EL 1

2.1 The description logic: ℰ ⁢ ℒ +

We first introduce the syntax and semantics of ℰ ⁢ ℒ + [11] which is the basic description logic (DL) that underpins OWL EL. Let CN and RN be two disjoint sets of atomic concepts and atomic roles respectively. We can further define complex concepts inductively by using the constructors ( ∃ and ⊓ ) shown in the left upper part of Table 1. We use the symbols C ( i ) , D ( i ) and E ( i ) for complex concepts, A ( i ) and B ( i ) for atomic concepts, r ( i ) , s ( i ) and t ( i ) for atomic roles. The symbol ⊤ denotes the top concept (or universal concept). A DL ontology is always defined as a pair 𝒪 = ⟨ 𝒯 , 𝒜 ⟩ where 𝒯 is called a TBox containing a finite set of general concept inclusion (GCI) axioms of the form C ⊑ D , role inclusion (RI) axioms of the form r ⊑ s and role chain (RC) axioms of the form r 1 ∘ r 2 ⊑ s ; 𝒜 is called an ABox that contains assertions about individuals (e.g., 𝚑𝚊𝚜𝙼𝚞𝚖 ⁢ ( 𝙹𝚊𝚌𝚔 , 𝙷𝚎𝚕𝚎𝚗 ) , hasMum is a role, Jack and Helen are individuals). Since individual is not our focus, we assume that an E ⁢ L + ontology is a TBox in this paper.

ℰ ⁢ ℒ + has a Tarski-style semantics. An interpretation ℐ = ( △ ℐ , ⋅ ℐ ) consists of △ ℐ and ⋅ ℐ , where △ ℐ is the domain of ℐ which is a non-empty set, and ⋅ ℐ is a function mapping each atomic concept A (resp. atomic role r ) to a subset A ℐ (resp. a subset r ℐ ) of △ ℐ (resp. △ ℐ × △ ℐ ). The interpretation function can be extended to arbitrary concept or role as shown in right part of Table 1. ℐ is a model of an ontology 𝒪 (written as ℐ ⊧ 𝒪 ) if ℐ satisfies all axioms in 𝒪 . We use 𝒪 ⊧ α for some axiom α if each model of 𝒪 satisfies α . We say that, for an axiom α , if α is occurring in 𝒪 , α is an original axiom; if α is not occurring in 𝒪 but 𝒪 ⊧ α holds, α is an entailment. We also say that a concept C is subsumed by D with respect to 𝒪 if 𝒪 ⊧ C ⊑ D .

A justification is a minimal set of axioms in an ontology that is responsible for a target axiom. Finding all justifications is to compute all such minimal axiom sets with respect to a given axiom. We follow the definition of justification for highly expressive description logics [7], and give the formal definition in our case as follows:

2.3 The classification task

The task of finding justifications is tightly related to the corresponding reasoning task. In this part, we introduce the task of classification which is an important reasoning task of ℰ ⁢ ℒ + . The goal of the classification task is to compute all concept subsumptions. Intuitively, finding justifications can be viewed an inverse process of classification. In other words, for some subsumption A ⊑ B (it is in the classification results), to find justifications of A ⊑ B is actually to obtain the original axioms that entail A ⊑ B .

A state-of-the-art reasoning system (referred as CEL) [12] is given to perform classification of ℰ ⁢ ℒ + ontologies. The classification algorithm used in CEL first transforms the given ontology to a normal form, where all concept inclusions are of the form A 1 ⊓ A 2 ⊑ B , A ⊑ ∃ r . B or ∃ r . B ⊑ A ( A ( i ) , B are atomic concepts), and all role inclusions are of the form r 1 ∘ r 2 ⊑ s or r ⊑ s . The normalization can be done in linear time. In the following, we assume that an input ontology O is in normal form. The classification algorithm then works on a group of rules. We call these rules the CEL rules (see Table 2). The concepts occurring in the CEL rules denote atomic concepts. A set 𝒞 𝒪 is used in the CEL rules. Initially, let 𝒞 𝒪 := 𝒪 ∪ ⋃ ∀ A ∈ 𝐂𝐍 { A ⊑ A , A ⊑ ⊤ } . The classification algorithm then extends 𝒞 𝒪 by exhaustively applying all the CEL rules. After classification, 𝒞 𝒪 contains all subsumptions. We call 𝒞 𝒪 of this stage the set of classification results with respect to 𝒪 . Without special statements, we use 𝒞 𝒪 to denote the set of classification results in following paper.

3.1 Issues

Constructing and maintaining ontologies is a difficult and error-prone process [13, 14, 15]. Logical errors or contradictions are quite common in real ontologies, specially, when the target ontologies are large in scale [14, 16]. At first, logical errors or contradictions denote the problems of incoherence for an ontology. Specifically, a TBox is incoherent[5] whenever there are unsatisfiable concepts: concepts which are interpreted as empty sets in all models of the TBox. The authors of [5] first give the formal definitions of unsatisfiability and propose the notions of MUPS (minimal unsatisfiability-preserving sub-TBoxes) and MIPS (minimal incoherence-preserving sub-TBoxes). A MUPS, with respect to a TBox 𝒯 and an unsatisfiable concept A , is a smallest subset of 𝒯 in which A is unsatisfiable. A MIPS is a smallest subset of an original TBox preserving unsatisfiability of at least one concept. The MIPS is used to identify the smallest sets of TBox that cause the original TBox to be incoherent. Thus, to tackle the problem of incoherence (or to do ontology debugging), an important task is to compute MUPS and MIPS for an incoherent ontology. ‘Justification’ is first used in [17] as a generalized notion of MUPS. It can be computed for any conclusion in addition to the contradicting ones. Actually, in some cases, users or developers wish to know how a conclusion can be obtained from the original ontology, though this ontology is well-constructed and contains no logical error. The techniques of finding justifications can be used in ontology debugging [17, 18, 19], entailment understanding [20, 21, 22] and even verifying reasoner correctness [23, 24].

In the following, we organize the discussion of the major approaches by two lines based on highly-coupled reasoners: black-box and glass-box methods.

3.2 Black-box methods

In black-box methods, a reasoner is used as a black-box (or an oracle) for certain reasoning tasks, e.g., classification, testing satisfiability, and etc. A typical black-box method focus on detecting dependencies between unsatisfiable concepts, i.e., identifying the root concept that causes the incoherence and the concepts derived from it [19, 25, 4]. This method suffers from low performance when computing all justifications (or MUPS). Researchers then adapt the techniques used in the contexts of model-based diagnosis[26] to the case of ontology debugging. Specifically, a diagnose specifies the minimal set of axioms that have to be ignored in order to turn the terminology coherent. Diagnoses can be computed by constructing a tree that is called hitting set tree (HST). HST is first used to compute MUPS in [27]. In [7] and [28], this method is used in highly expressive OWL languages, and evaluated on small ontologies. There is also works that uses HST techniques to translate the problem of ontology debugging to SAT problem [29, 30]. Some other optimizing strategies are further applied to accelerate the computation based on black-box methods, such as module extraction [8, 9] and other heuristic approaches [31, 32, 33].

3.3 Glass-box methods

In glass-box methods, reasoning information from the internals of a reasoner is extracted and presented to the developers for tracing how a conclusion is derived. That is why these methods are called glass-box methods. The work of [5] takes the first attempt to compute MUPS in the description logic 𝒜 ⁢ ℒ ⁢ 𝒞 based on a DL reasoner. The used reasoner is based on a tabular algorithm, which materializes ontologies by obtaining all possible individual assertions. Specifically, the method proposed in [5] requires to modify the implementation of the reasoner RACER such that each assertion is labeled by a set of axioms that are responsible for it. After materialization, these labels are backtracked to compute MUPS. For the tractable fragments of description logics, i.e., ℰ ⁢ ℒ and DL-lite, the similar methods are studied based on high performance reasoners (cf. [6, 34]). Some other techniques are proposed to optimize glass-box methods [35, 36].

3.4 Discussion

In following paragraphs, we discuss the advantages and drawbacks of black-box and glass-box methods. For black-box methods, they have one advantage over glass-box ones: no need for a specialized, explanation generating reasoner. However, to compute MUPS or justifications, a number of calls for reasoners is always necessary. Since reasoning tasks are inherently expensive in terms of running time, black-box methods can hardly work on large ontologies. This is also shown by current experimental results.

For glass-box methods, the biggest difference from black-box ones lies in that they just need single run of reasoners. However, glass-box methods still suffer from some problems: 1) A glass-box method requires to modify the implementation of reasoner. Some optimizations (like pruning techniques, optimized encoding) for reasoners have to be dropped in order to record special information for finding justifications. Furthermore, different modifications are needed when applying different reasoners. 2) Extra data structures should be maintained. This brings additional space and computation consumption. 3) It is hard to introduce some heuristic blocking techniques to speed up the computation of finding justifications. This is because, when backtracking attached tags, it is difficult for us to acquire global information that can guide us to avoid failed branches.

In summary, both of black-box and glass-box methods suffer from a common issue: they are highly-coupled with reasoners, i.e., the performance of finding justifications is highly influenced by that of the utilized reasoner. Thus, some optimizations cannot work as discussed above. In order to tackle this problem, we consider giving a method such that the task of finding justifications can be conducted independently from the utilized reasoner, and thus, cannot be influenced by the performance of the reasoner. In the following sections, we discuss this method in detail.

5.1 Traveling patterns

Recall that deductive dependencies are defined based on the rules in Table 2. This also means that deductive dependencies between explanations can be further distinguished by different rules in Table 2. Consider explanations ( e 2 ) and ( e 4 ) in Example 3. ( e 2 ) deductively depends on ( e 4 ) through Rule R H . Based on the correspondences between deductive dependencies and classification rules, we can construct EDGs by traveling from the root node, and visiting other explanations through different rules. Specifically, we give different traveling patterns based on the rules in Table 2 as follows:

Suppose V ℰ is a node in an EDG, and A ⊑ B is an entailment in ℰ . Since A ⊑ B can be derived by applying rules R ⊑ , R ⊓ or R ∃ - , we have the following patterns to reach a child node V ℰ ′ of V ℰ :

(P 0 )

If B ≡ A , then ℰ ′ = ℰ ∖ { A ⊑ B } ;

(P ⊤ )

If B ≡ ⊤ , then ℰ ′ = ℰ ∖ { A ⊑ B } ;

(P ⊑ )

If there exists a concept X s.t., A ⊑ X ∈ 𝒞 𝒪 and X ⊑ B ∈ 𝒪 , then ℰ ′ = ℰ ∪ { A ⊑ X , X ⊑ B } ∖ { A ⊑ B } ;

(P ⊓ )

If there exists axioms A ⊑ X 1 , A ⊑ X 1 ∈ 𝒞 𝒪 and X 1 ⊓ X 2 ⊑ B ∈ 𝒪 , then ℰ ′ = ℰ ∪ { A ⊑ X 1 , A ⊑ X 1 , X 1 ⊓ X 2 ⊑ B } ∖ { A ⊑ B } ;

(P ∃ - )

If there exists axioms A ⊑ ∃ r . X , X ⊑ Y ∈ 𝒞 𝒪 and ∃ r . Y ⊑ B ∈ 𝒪 , then ℰ ′ = ℰ ∪ { A ⊑ ∃ r . X , X ⊑ Y , ∃ r . Y ⊑ B } ∖ { A ⊑ B } .

In the above patterns, we say that A ⊑ B is a bud in ℰ .

Suppose V ℰ is a node in an EDG, and A ⊑ ∃ r . B is an entailment in ℰ . Since A ⊑ ∃ r . B can derived by applying the rules R ∃ + , R H or R ∘ , we have the following three patterns to reach a child node V ℰ ′ of V ℰ :

(P ∃ + )

If there exists a concept X s.t., A ⊑ X ∈ 𝒞 𝒪 and X ⊑ ∃ r . B ∈ 𝒪 , then ℰ ′ = ℰ ∪ { A ⊑ X , X ⊑ ∃ r . B } ∖ { A ⊑ ∃ r . B } ;

(P H )

If there exists a role s s.t., A ⊑ ∃ s . B ∈ 𝒞 𝒪 and s ⊑ r ∈ 𝒪 , then ℰ ′ = ℰ ∪ { A ⊑ ∃ s . B , s ⊑ r } ∖ { A ⊑ ∃ r . B } ;

(P ∘ )

If there exists axioms A ⊑ ∃ s . X , X ⊑ ∃ t . B ∈ 𝒞 𝒪 and s ∘ t ⊑ r ∈ 𝒪 , then ℰ ′ = ℰ ∪ { A ⊑ ∃ s . X , X ⊑ ∃ t . B , s ∘ t ⊑ r } ∖ { A ⊑ ∃ r . B } .

In the above patterns, we say that A ⊑ ∃ r . B is a bud in ℰ . □

Patterns P 0 –P ∘ are applied when traveling from a node ℰ to one of its child ℰ ′ in an EDG through some bud. Patterns P 0 and P ⊤ say that for an entailment of the form A ⊑ A or A ⊑ ⊤ occurring in ℰ , this entailment is directly eliminated from ℰ , and, ℰ ′ is obtained. This is because that entailments of the form A ⊑ A or A ⊑ ⊤ are tautological axioms which hold in any ontology containing the concept A . Patterns P ⊑ to P ∘ correspond to Rules R ⊑ to R ∘ in Table 2 respectively. Intuitively, these patterns can be viewed as inverse processes of corresponding rules. We take Pattern P ∃ - for an example. Suppose ℰ contains an entailment of the form A ⊑ ∃ r . B , and we also have that two axioms A ⊑ ∃ r . X and X ⊑ Y hold in the set of classification results 𝒞 𝒪 and ∃ r . Y ⊑ B occurs in the original ontology. It also means that A ⊑ ∃ r . B can be derived from A ⊑ ∃ r . X , X ⊑ Y and ∃ r . Y ⊑ B by applying Rule R ∃ - . We get a child node of ℰ : ℰ ′ ( = ℰ ∪ { A ⊑ ∃ r . X , X ⊑ Y , ∃ r . Y ⊑ B } ∖ { A ⊑ ∃ r . B } ) by treating A ⊑ ∃ r . B as a bud. Based on the above discussion, if ℰ is an explanation of the target axiom α , ℰ ′ is also an explanation of α . The other patterns can be explained similarly.

5.2 An algorithm of constructing EDGs

Based on the traveling patterns, we can construct a complete EDG and obtain all explanations for a given entailment α . An intuitive process of constructing EDGs is as follows: the process starts by adding a root node in an empty EDG and iteratively generates child nodes of newly added nodes; since one node in an EDG may contain multiple entailments which can all be selected as buds, there could be multiple child nodes by selecting different buds; when all nodes are generated, the construction of a complete EDG is finished. We give Algorithm 1 to construct a complete EDG.

At the beginning of Algorithm 5.2, the algorithm checks whether the axiom A ⊑ B is in the original ontology 𝒪 . If A ⊑ B is an original axiom, Algorithm 5.2 terminates and returns { A ⊑ B } as the only explanation (lines 1–3). Otherwise an empty queue Q is created and the root node V { A ⊑ B } is put in Q (lines 4 and 5). Then the algorithm uses the queue Q to construct an EDG and obtain the set of explanations of { A ⊑ B } (lines 6–14). The basic procedure is that, if the queue Q is not empty, a new node V ℰ in Q is visited and the function expand( ⋅ ) is called to expand V ℰ and generate new child nodes of V ℰ based on the traveling patterns P 0 –P ∘ . In line 8, a condition BC1 (we discuss it in detail in following paragraphs) is used to guarantee the termination of Algorithm 5.2. The program may not terminate in some cases, where an entailment in one node V ℰ is also in an child node V ℰ ′ of V ℰ . We call this a non-termination problem. We use an example to illustrate this problem.

[H] Constructing a Complete EDG A ⊑ B : an entailment; 𝒪 : a normalized ℰ ⁢ ℒ + ontology; 𝒞 𝒪 : the classification result after classifying 𝒪 . J : the set of explanations for A ⊑ B .

A ⊑ B ∈ 𝒪 put( J , { A ⊑ B } )  return  create a queue Q   put a root node V { A ⊑ B } in Q

Q is not empty V ℰ ← Q .pop()  V ℰ satisfies BC1 skip following procedure and continue the while iteration

ℰ ea is empty put( J , ℰ )  get an entailment α from ℰ 𝚎𝚊   expand( A ⊑ B , V ℰ , Q );

OPEN IN VIEWER

To avoid the non-termination problem, we follow an intuitive idea: if a node V ℰ is generated and there exists an entailment α in ℰ that also appears in one ancestor node of V ℰ , ℰ is blocked for further expanding. As shown in Fig. 2, if the node V ℰ ′′ is blocked, none of its child node can be further generated. Formally, we give the following blocking condition BC1:

BC1

Suppose a node V ℰ is being visited, if there exists an entailment α in ℰ which is also a bud in one ancestor node V ℰ ′ of V ℰ , then V ℰ is blocked.

Intuitively, by applying BC1, in each path of an EDG constructed by Algorithm 5.2, all nodes have different buds. Since the number of entailments with respect to an ontology is fixed in the size of the given ontology, EDGs constructed by Algorithm 5.2 have to be finite in size.

At this point, Step 1 has been finished, i.e., we can use Algorithm 5.2 to obtain all explanations for an entailment. We give the following theorem to show the correctness of Algorithm 5.2,. That is: (1) BC1 guarantees the termination of Algorithm 5.2; (2) Algorithm 5.2 can always construct a complete EDG.

The above theorem can be proved based on Lemmas 2 and 3.

Proof. Since 𝒥 is a justification of α , one can identify a sequence of explanations ( ℰ 1 , ℰ 2 , … , ℰ k - 1 , ℰ k ) ( $k>1$ ) where ℰ 1 = 𝒥 and ℰ k = { α } , such that for 1 ⩽ i ⩽ k - 1 , ℰ i + 1 deductively depends on ℰ i , and these explanations satisfy BC1. It can be easily checked that each node of the form V ℰ i ( 1 ⩽ i ⩽ k ) has to be added to 𝒢 by Algorithm 1. □

Proof. The above lemma can be proved based on the conclusion that 𝒞 𝒪 ′ ⊆ 𝒞 𝒪 where 𝒞 𝒪 ′ (resp., 𝒞 𝒪 ) is the set of classification results of 𝒪 ′ (resp., 𝒪 ). This conclusion can be proved by an induction on the CEL rules in Table 2. It can also be proved by the semantics of ℰ ⁢ ℒ + . That is, for each entailment β , 𝒪 ′ ⊧ β implies 𝒪 ⊧ β . We do not give the details here.

To finish this lemma, we first define the depths of nodes in an EDG ℋ as follows. Let the depth of the root node V r ⁢ o ⁢ o ⁢ t be 0, denoted by d ( V r ⁢ o ⁢ o ⁢ t ) = 0 ; for each node V and its parent V ′ in ℋ , if d ( V ′ ) = k , let d ( V ) = k + 1 . We conduct the proof of this lemma by an induction on the depths of nodes in the EDG ℋ constructed by Algorithm 1.

(Basic case) Suppose α is the target axiom. The root node V α has to exist in both of 𝒢 and 𝒢 ′ . Thus, the basic case holds.

(Inductive cases) We have an induction hypothesis that, for an depth i ( i ⩾ 0 ), each node V of depth j ( 1 ⩽ j ⩽ i ) in 𝒢 ′ is also in 𝒢 . We then need to prove that, for the depth i + 1 , each node V of depth j ′ ( 1 ⩽ j ′ ⩽ i + 1 ) in 𝒢 ′ has to be in 𝒢 . In Algorithm 1, new nodes are generated by just applying the code in line 14 where the function expand( ⋅ ) is called. In the function expand( ⋅ ), the traveling patterns P 0 –P ∘ are applied respectively. In the following, we continue this proof by distinguishing different cases based on different traveling patterns.

Suppose V is in 𝒢 ′ , V ′ is the parent of V , and d ( V ) = j ( 1 ⩽ j ⩽ i + 1 ). We should prove that V is in 𝒢 as well.

(Case P 0 ) Suppose V is generated by using this pattern. We have that V ′ is in the form of V ∪ { A ⊑ B } where A ≡ B . According to the induction hypothesis, V ′ is in 𝒢 . By applying this pattern in Algorithm 1, V can also be generated and added in 𝒢 .

(Case P ⊤ ) This case is similar to the previous case.

(Case P ⊑ ) Suppose V is generated by using this pattern. We have that V ′ is in the form of V ∪ { A ⊑ B } ∖ { A ⊑ X , X ⊑ B } where A ⊑ X ∈ 𝒞 𝒪 ′ and X ⊑ B ∈ 𝒪 ′ . Since we have that 𝒞 𝒪 ′ ⊆ 𝒞 𝒪 and 𝒪 ′ ⊆ 𝒪 , A ⊑ X ∈ 𝒞 𝒪 and X ⊑ B ∈ 𝒪 also hold. According to the induction hypothesis, V ′ is in 𝒢 . By applying this pattern on 𝒪 in Algorithm 1, V can also be generated and added to 𝒢 .

(Case P ⊓ ) Suppose V is generated by using this pattern. We have that V ′ is in the form of V ∪ { A ⊑ B } ∖ { A ⊑ X 1 , A ⊑ X 1 , X 1 ⊓ X 2 ⊑ B } where A ⊑ X 1 , A ⊑ X 1 ∈ 𝒞 𝒪 ′ and X 1 ⊓ X 2 ⊑ B ∈ 𝒪 ′ . Since we have that 𝒞 𝒪 ′ ⊆ 𝒞 𝒪 and 𝒪 ′ ⊆ 𝒪 , A ⊑ X 1 , A ⊑ X 1 ∈ 𝒞 𝒪 and X 1 ⊓ X 2 ⊑ B ∈ 𝒪 also hold. According to the induction hypothesis, V ′ is in 𝒢 . By applying this pattern on 𝒪 in Algorithm 1, V can also be generated and added to 𝒢 .

(Case P ∃ - ) Suppose V is generated by using this pattern. We have that V ′ is in the form of V ∪ { A ⊑ B } ∖ { A ⊑ ∃ r . X , X ⊑ Y , ∃ r . Y ⊑ B } where A ⊑ ∃ r . X , X ⊑ Y ∈ 𝒞 𝒪 ′ and ∃ r . Y ⊑ B ∈ 𝒪 ′ . Since we have that 𝒞 𝒪 ′ ⊆ 𝒞 𝒪 and 𝒪 ′ ⊆ 𝒪 , A ⊑ ∃ r . X , X ⊑ Y ∈ 𝒞 𝒪 and ∃ r . Y ⊑ B ∈ 𝒪 also hold. According to the induction hypothesis, V ′ is in 𝒢 . By applying this pattern on 𝒪 in Algorithm 1, V can also be generated and added to 𝒢 .

(Case P ∃ + ) Suppose V is generated by using this pattern. We have that V ′ is in the form of V ∪ { A ⊑ ∃ r . B } ∖ { A ⊑ X , X ⊑ ∃ r . B } where A ⊑ X ∈ 𝒞 𝒪 ′ and X ⊑ ∃ r . B ∈ 𝒪 ′ . Since we have that 𝒞 𝒪 ′ ⊆ 𝒞 𝒪 and 𝒪 ′ ⊆ 𝒪 , A ⊑ X ∈ 𝒞 𝒪 and X ⊑ ∃ r . B ∈ 𝒪 also hold. According to the induction hypothesis, V ′ is in 𝒢 . By applying this pattern on 𝒪 in Algorithm 1, V can also be generated and added to 𝒢 .

(Case P H ) Suppose V is generated by using this pattern. We have that V ′ is in the form of V ∪ { A ⊑ ∃ r . B } ∖ { A ⊑ ∃ s . B , s ⊑ r } where A ⊑ ∃ s . B ∈ 𝒞 𝒪 ′ and s ⊑ r ∈ 𝒪 ′ . Since we have that 𝒞 𝒪 ′ ⊆ 𝒞 𝒪 and 𝒪 ′ ⊆ 𝒪 , A ⊑ ∃ s . B ∈ 𝒞 𝒪 and s ⊑ r ∈ 𝒪 also hold. According to the induction hypothesis, V ′ is in 𝒢 . By applying this pattern on 𝒪 in Algorithm 1, V can also be generated and added to 𝒢 .

(Case P ∘ ) Suppose V is generated by using this pattern. We have that V ′ is in the form of V ∪ { A ⊑ ∃ r . B } ∖ { A ⊑ ∃ s . X , X ⊑ ∃ t . B , s ∘ t ⊑ r } where A ⊑ ∃ s . X , X ⊑ ∃ t . B ∈ 𝒞 𝒪 ′ and s ∘ t ⊑ r ∈ 𝒪 ′ . Since we have that 𝒞 𝒪 ′ ⊆ 𝒞 𝒪 and 𝒪 ′ ⊆ 𝒪 , A ⊑ ∃ s . X , X ⊑ ∃ t . B ∈ 𝒞 𝒪 and s ∘ t ⊑ r ∈ 𝒪 also hold. According to the induction hypothesis, V ′ is in 𝒢 . By applying this pattern on 𝒪 in Algorithm 1, V can also be generated and added to 𝒢 .

The proof of Lemma 3 is finished. We now prove Theorem 1. For each justification 𝒥 of the entailment A ⊑ B , we have that 𝒥 ⊆ 𝒪 . Let 𝒢 𝒥 be the EDG constructed by Algorithm 1 on 𝒥 and A ⊑ B . There has to be a node V 𝒥 in 𝒢 𝒥 according to Lemma 2. By Lemma 3, 𝒢 𝒥 ⊆ 𝒢 𝒪 holds. Thus, we have that V 𝒥 is in 𝒢 𝒪 . It also indicates that 𝒢 𝒪 is a complete EDG. □

We now discuss the scale of a complete EDG. In the worst cases, a complete EDG may contain exponential number of nodes in the size of the target ontology. Specifically, in the while iteration, Algorithm 5.2 constructs the target EDG by starting from a node V ℰ through the out-edges to all possible child nodes for one bud in ℰ . Suppose ℰ ′ is a newly added explanation. If all axioms in ℰ ′ are from the original ontology, ℰ ′ will be added as a candidate justification in J (see lines 10 and 11). When queue Q is empty, the construction stops. Consider that the worst case is to visit all possible nodes and links between adjacent nodes in the target EDG, the complexity is O ⁢ ( | V | 2 ) . It shows that the complexity of our algorithm depends on the number of nodes in a complete EDG. Since there exists exponential number of justifications in the worst case, there may be exponentially many nodes in an EDG. This also shows the hardness of the problem of finding justifications.

Computing justifications from explanations. Algorithm 5.2 returns explanations that may be supersets of justifications. In order to obtain all justifications, we should further process the outputs of Algorithm 5.2 (corresponding to Step 2). We use Algorithm 3 to compute all justifications which takes the outputs of Algorithm 5.2 as inputs.

[H] Computing All Justifications J : a set of explanations for A ⊑ B (containing only original axioms). J ′ : the set of all justifications for A ⊑ B .

j n ∈ J j m ∈ J j n ⊂ j m Remove( J , j m )  Remove( J , j n )  J ′ ← J

Algorithm 3 computes all justifications for an entailment A ⊑ B by removing all the supersets of each candidate justification in J . The cost of computing in this phase can be negligible compared to the cost of constructing an EDG. This is because that the number of explanations containing only original axioms is far less than the number of nodes generated in an EDG according to our preliminary experiments.

6.1 Blocking conditions

In the work of [7, 8], the authors propose a method of finding justifications based on a kind of tree structure (known as Hitting Set Tree). A simple blocking condition is studied in this work to avoid visiting all branches of a hitting set tree when generating justifications. The basic idea is to use the visited branches to filter out the useless branches. We follow this idea and study the blocking conditions in our case. That is, to give conditions to block the explanations that will not generate justifications during the construction of an EDG. Since an EDG is not a hitting set tree, the blocking condition given in [7, 8] cannot apply in our case. We give our own blocking conditions as follows.

Suppose a node V ℰ is being visited:

BC2

If there exists a node V ℰ ′ which has been visited such that ℰ ′ ⊆ ℰ , then V ℰ is blocked;

BC3

If there exists a candidate justification j such that j ⊆ ℰ oa , then V ℰ is blocked;

BC4

If there exists a child node V ℰ ′ expanded from an entailment α in V ℰ , and ℰ ′ ⊆ ℰ , then the other branches of V ℰ expanded by α are blocked.

The condition BC2 is used to avoid repeated expansion of the same node. BC3 states that when a node V ℰ is visited and its original axiom set has already been a candidate justification, then it is not needed to be expanded further. The meaning of BC4 can be explained similarly. We use Example 6 to illustrate the usage of BC4.

.

In Fig. 3, V ℰ is expanded to V ℰ ′ , V ℰ ′′ and V ℰ ′′′ from X ⊑ B by using Patterns P ⊓ or P ⊑ . After expanding, we have that ℰ ′′ ⊆ ℰ . This means that X ⊑ B holds in ℰ . We also have ℰ ′′ ⊆ ℰ ′ and ℰ ′′ ⊆ ℰ ′′′ . According to BC2, V ℰ ′ and V ℰ ′′′ can be blocked. Thus in this kind of cases, we block the other branches expanded from such entailments since the nodes in those branches will not generate justifications.

OPEN IN VIEWER

Figure 3.

A case of using BC4 to block nodes in an EDG.

6.2 Parallelizing EDG construction

Parallelizing the task of finding justifications is rarely studied due to its inherent high complexity. One parallel method of ontology debugging is given in the work of [37]. This method focus on partitioning the target ontology into smaller pieces and conducting ontology debugging in parallel. Since this method aims at parallelizing the target ontology but not the algorithm, it cannot be used in our case. For parallelizing EDG construction, we give our method based on the observation that the paths in an EDG are independent from each other. This indicates that the generation of each path in an EDG can be performed in a parallel way. This is the basic motivation of our method. Specifically, we give Algorithm 6.2 which parallelizes EDG construction and utilizes the above blocking conditions as well.

[H] Computing justifications in parallel A ⊑ B : an entailment; 𝒪 : a normalized ℰ ⁢ ℒ + ontology; 𝒞 𝒪 : the set of classification result with respect to 𝒪 . J : the set of explanations for A ⊑ B . A ⊑ B ∈ 𝒪 put( J , { A ⊑ B } )  return  create a queue Q   put a root node V { A ⊑ B } in Q   Q is not empty V ℰ ← Q .pop()  allocate V ℰ to a new routine R 1   R 1 .execute(): { V ℰ can be blocked R 1 .stop()  V ℰ ′ ← expand( V ℰ )  ℰ ′ contains no entailment put( J , ℰ ′ )  put( Q , V ℰ ′ )  } J ← computeAllJustifications( J )  The initialization part of Algorithm 6.2 is the same as that of Algorithm 5.2. The difference is that we parallelize the while iteration in Algorithm 6.2. In line 9, when a node V ℰ is generated from Q , the program launches a new routine (or a thread) R 1 to expand the EDG from V ℰ . The execution logic of R 1 is given in lines 10 to 19. R 1 first checks whether V ℰ can be blocked based on the blocking conditions (line 11). If V ℰ can be blocked, R 1 terminates and the traversal in this branch stops. Otherwise, R 1 expands V ℰ using the traveling patterns and a child node of V ℰ denoted by V ℰ ′ is generated. If ℰ ′ consists of original axioms, ℰ ′ will be added to J (line 16); otherwise it will be put in Q (line 18). The program computes all justifications using Algorithm 3 in line 20. We give Theorem 2 to show the correctness of Algorithm 6.2.

Proof. We first construct a new algorithm 𝒜 1 𝚘𝚙𝚝 based on Algorithm 1. Specifically, 𝒜 1 𝚘𝚙𝚝 generates new nodes as same as Algorithm 1, but checks these nodes according to BC2-BC4, i.e., if new generated nodes satisfy BC2, BC3 or BC4, 𝒜 1 𝚘𝚙𝚝 blocks them. It is obvious that 𝒜 1 𝚘𝚙𝚝 constructs complete EDGs, since blocked nodes must not lead to justifications.

We now prove the above theorem by checking that all nodes in the EDG ℋ constructed by 𝒜 1 𝚘𝚙𝚝 have to be generated in the EDG 𝒢 constructed by Algorithm 3 as well. We show this by an induction on the depths of nodes (see the definition of node depths in the proof of Lemma 3) in ℋ .

(Basic case) Suppose α ≡ A ⊑ B is the target axiom. The root node V α has to exist in both of ℋ and 𝒢 . Thus, the basic case holds.

(Inductive cases) We have an induction hypothesis that, for an depth i ( i ⩾ 0 ), each node V of depth j ( 1 ⩽ j ⩽ i ) in ℋ is also in 𝒢 . We then need to prove that, for the depth i + 1 , each node V of depth j ′ ( 1 ⩽ j ′ ⩽ i + 1 ) in ℋ has to be in 𝒢 . This can be proved by two invariants set in 𝒜 1 𝚘𝚙𝚝 and Algorithm 3: (1) each explanation has a total lexicographical order of axioms; (2) each selected bud has the minimum order in an explanation. These two invariants ensure that whenever a node is checked in Algorithm 3, it would generate same child nodes. Based on this observation and the induction hypothesis, the inductive cases can be proved. □

We implemented our algorithms by using Java multithread techniques. Since the queue in Algorithm 1 would be visited concurrently, we implemented it based on a thread-safe datatype ConcurrentLinkedQueue. To classify an ontology, we used jCEL4

We used five real ontologies to perform our experiments: Galen-core (a tailored version of Galen), Galen, NCI, GO and SNOMED CT.5

For Galen-core, NCI and GO, we sampled 20% of all the entailments based on the method of simple random sampling [38]. For Galen and SNMOED CT, we sampled 200 entailments. The above samples do not include the entailments of the form A ⊑ A , A ⊑ ⊤ or ⟂ ⊑ A since they make no sense in the final experimental results. In addition, we set 10 minutes as the time limit for all experiments. One may note that reasoning time is unlimited. This is because that the task of reasoning is supposed to run in an offline way. However, the task of finding justifications is supposed to be a service online. Thus, we set 10 minutes to bond the response time.

We ran our system on the sampled entailments, and collected the experimental results in Table 4. The fourth (resp., seventh) column of Table 4 collected the averagely (resp., maximal) occupied space for storage of a constructed EDG (a kilobyte per unit). From Table 4, we can see that there is no time-out case for Galen-core, NCI and GO due to their small sizes. By comparing the results of different ontologies, we can find that, the average computing time is close. This is similar to the results of the average numbers of expanded nodes. This is because the main proportion of samples tends to be easily handled (we call them the easy samples), i.e., the EDGs of the easy samples contain a handful of nodes, and, can be constructed within a second. On the other hand, the results of the average cases are significantly better than that of the worst cases. This can also be explained by the large proportion for the easy samples.

In order to investigate the effect of the blocking conditions given in Section 6, we give Fig. 4 where five histograms are involved for the tested ontologies respectively. In each histogram, the abscissa axis records the numbers of nodes in an EDG, the vertical axis records the numbers of samples, and, the white bars (resp., the black bars) denote the numbers of samples for which the numbers of finally expanded nodes (resp., the numbers of blocked nodes) fall in the corresponding intervals of the abscissa axis. From Fig. 4 we can find that each histogram has relatively higher bars in its head and shorter bars in its tail. This indicates that the easy samples take a large proportion, i.e., the numbers of finally expanded nodes are small. On the other hand, the areas of black bars are close to that of white bars. This means that, the number of blocked nodes is close to the number of finally expanded nodes. According to Algorithm 1, visiting a node occupies a time unit. Thus, the computing time is actually reduced by nearly 50% compared to a naive algorithm without using the blocking conditions.

OPEN IN VIEWER

In this part, we compare our method to traditional glass-box and black-box methods by evaluating the same samples. Since there is no available implementation of traditional glass-box method for finding justification in OWL EL, we follow the idea given in [6] and implement a system (denoted by Sys-Glass-Box) using Java. For black-box implementation, we choose a well-developed Prot e ´ g e ´ plugin, the Explanation Workbench, which can also handle OWL EL ontologies [39].

We use the sampled entailments in the previous experiment to evaluate Sys-Glass-Box and the Explanation Workbench and collected the results in Tables 5 and 6 respectively. In Table 5, the third (resp., fifth) column collects the averagely (resp., maximal) occupied space for storage of tracing information (a kilobyte per unit). In Table 6, the third (resp., fifth) column collects the average (resp., maximal) number of reasoner calls.

By comparing the results in Tables 4 and 5, we can find that, the occupied space of our method is far less than that of Sys-Glass-Box. This is due to two reasons: 1) our method does not attach extra information to the classification results, while Sys-Glass-Box has to tag each entailment to trace reasoning procedure; 2) an EDG is only constructed for a target entailment. In other words, the unrelated axioms and entailments will not be considered during computing. On the other hand, some optimizing strategies, e.g., pruning techniques, cannot be used in Sys-Glass-Box. This is because that the tracing paths used in [6] are inter-dependent. This kind of inter-dependence makes it impossible to use block conditions and introduce parallelism techniques. The experimental results also show that our method performs better in terms of computing time. Further, the rate of time-out cases of our method stays lower.

From Tables 4 and 6, we can see that for all test ontologies, the proportion of time-out cases in our system is less than that of the Explanation Workbench. The average time of computing justifications of these two systems is close. We observed that the time-out cases occurring in our system and the Explanation Workbench are not always the same. For example, when handling SNOMED CT by the Explanation Workbench, a time-out case is to compute justifications of the subsumption between the concept “Entire inferior process of eleventh thoracic vertebra ” and the concept “Musculoskeletal structure of thoracic spine”, which has 7 justifications, and takes nearly 20 seconds to finish the computation. In contrast, our system gives the results within one second. On the other hand, a time-out case in our system is to compute justifications between the concept “Bisoprolol fumarate 10mg tablet” and the concept “Cardiovascular drug” which has only one justification. For this case, the Explanation Workbench finishes immediately. The difference lies in that the efficiency of the black-box method is decided by the sizes of the target ontologies and the number of reasoner calls, while the efficiency of our method depends on the number of nodes in the constructed EDGs.