One of the major problems of axiom pinpointing for incoherent terminologies is the precise positioning within the conflict axioms. In this paper we present a formal notion for the entailment-based axiom pinpointing of incoherent terminologies, where the parts of an axiom is defined by atomic entailment. Based on these concepts, we prove the one-to-many relationship between existing axiom pinpointing with the entailment-based axiom pinpointing. For its core task, calculating minimal unsatisfiable entailment, we provide algorithms for OWL DL terminologies using incremental strategy and Hitting Set Tree algorithm. The feasibility of our method is shown by case study and experiment evaluations.
Ontology debugging becomes a challenging task for ontology modelers since the
improvement of expressivity of ontology language and ontology scale[
The rest of this paper is organized as follows. In section 2 we briefly introduce the drawback of MUPS. Then the formal definitions about fine-grained axiom pinpointing, and the link with axiom pinpointing are presented in section 3. Section 4 presents algorithm for calculating the minimal unsatisfiable entailment. Section 5 analyzes the fine-grained axiom pinpointing with a case study and evaluates the algorithm by experimenting with common ontologies. Finally, we conclude the paper in section 6. 2
Axiom pinpointing[
Most existing approaches can obtain the different fine-grained problematic axioms on the basis of axiom pinpointing as none of these approaches define exactly what they mean by parts of axioms. Further, some logic contradictions would be lost with axiom pinpointing since it does not point out the specific location within the axioms of the logic contradiction. Let us use an example to illustrate these limitations. Example 1. A TBox T1 consists of the following axioms (α1 − α6), where A and B are base concepts, A1, ..., A6 are named concepts, and r and s are roles: α1 : A1 v A2 u ∃r.A2 u A3 α2 : A2 v A u B α3 : A3 v ∀r.(¬B u ¬A) α4 : A4 v ∀r.A u ∀s.B u A5 α5 : A5 v ∃r.¬A u A6 α6 : A6 v ∃s.¬B
Consider the above example, by using standard DL TBox reasoning, it can be shown that the concept A1 and A4 are unsatisfiable. Analyzing concept A1, the existing approaches identify {α1, α2, α3} the only MUPS for A1 in T1, but it is not clear whether A2 or ∃r.A2 of α1 contradicts with α3. In addition, it hides crucial information, e.g., that unsatisfiability of A1 depends on all parts of α2 or α3. For A4, {α4, α5} is the only MUPS for A4 in T1, which on behalf of the error caused by ∀r.A of α4 and ∃r.¬A of α5. Actually, ∀s.B of α4, A6 of α5 and ∀s.¬B of α6 also lead to the unsatisfiability of A4, which would not be involved in the reason of unsatisfiability of A4 since MUPS can not pinpoint the location of conflict, i.e., some unsatisfiable (or incoherent) reasons would be ignored by axiom pinpointing. We will use this example to explain our debugging methods. 3
This section presents the main technical contribution of the paper. We would like to provide a framework for entailment-based axiom pinpointing. We will present the formal definitions which involve MUE, then show the relationship between MUPS and MUE. The second subsection is concerned with how to get all components w.r.t. axiom and terminology. 3.1
To compensate the limitations of axiom pinpointing, we introduce the notion of fine-grained axiom pinpointing and link it to description logic-based systems. Whereas the definitions of fine-grained axiom pinpointing are independent of the choice of a particular Description Logic.
Definition 2 (Entailment[
We denote by E (T ) and E (α) the set of all atomic consequences of terminology T and {α}, respectively. If a terminology T is incoherent, then for any axiom β, T β, i.e., a standard entailment is explosive. Thus, we require E (T ) = Sα∈T E (α) if T is incoherent, and E (α) = {α} if the axiom α has no model. Intuitively, an atomic consequence of an axiom is a part of the axiom, and set of all atomic consequences of an axiom contains all parts of the axiom. Definition 4 (MUE). Let C be an unsatisfiable concept in terminology T . A sub-TBox Tc ⊆ E (T ) is a minimal unsatisfiable entailment for C in T if C is unsatisfiable in Tc, and C is satisfiable in every sub-TBox Tc0 ⊂ Tc.
The entailment-based axiom pinpointing inferential service is the problem of computing MUE. We denote by mue(T , C) the set of MUE of C in terminology T . In the terminology of Reiter’s diagnosis each mue(T , C) is a collection of conflict sets. The following are the MUE for our example TBox T1: mue(T1, A1) = {{A1 v ∃r.A2, A1 v A3, A2 v A, A3 v ∀r.¬A},
{A1 v ∃r.A2, A1 v A3, A2 v B, A3 v ∀r.¬B}} mue(T1, A4) = {{A4 v ∀r.A, A4 v A5, A5 v ∃r.¬A},
{A4 v ∀s.B, A4 v A5, A5 v A6, A6 v ∃s.¬B}}
MUE can be regarded as the fine-grained axiom pinpointing for MUPS. The relationship between axiom pinpointing and our pinpointing is established by Theorem 1, i.e., the one-to-many relationship between MUPS and MUE. Theorem 1 (MUPS-to-MUEs relationship). Let C be an unsatisfiable concept in terminology T . Then: (1) If C is unsatisfiable in T , then C is unsatisfiable in E (T ). (2) for every M ∈ mups(T , C), there is a K ∈ mue(T , C) s.t. K ⊆ E (M). (3) for any M1, M2 ∈ mups(T , C) and K1, K2 ∈ mue(T , C) where M1 6= M2, K1 ⊆ E (M1) and K2 ⊆ E (M2), we have K1 6= K2.
Proof. We prove (1), (2) and (3) in order. (1) According to the definition of atomic entailment, If an axiom α ∈ T has no model, E (α)={α}. Otherwise, we can prove {α} and E (α) are equivalent with the axiom decomposition which is described in next subsection. In general, T and E (T ) are equivalent. (2) Since M ⊆ mups(T , C), we have C is unsatisfiable in E (M). Thus, mue(M, C) = mups(E (M), C), and for every K ∈ mue(M, C), we get K ⊆ E (M). (3) Suppose K ∈ mue(T , C), M1, M2 ∈ mups(T , C) (M1 6= M2) s.t. K ⊆ E (M1) and K ⊆ E (M2). Thus, there exists a sub-TBox T 0 ⊆ T s.t. K ⊆ E (T 0) and K * E (T 00) for every T 00 ⊂ T 0. Then C is unsatisfiable in T 0, T 0 ⊆ M1 and T 0 ⊆ M2. Since M1, M2 ∈ mups(T , C), we get T 0 = M1 = M2 which contradicts with the assumption.
It is characteristic of our axiom pinpointing, in the sense to be made more precise, to uniquely identify each logical contradiction. For example, TBox T = {A1 v AuBuA2, A2 v ¬Au¬B}, T is the only MUPS of A1 while mue(T , A1) = {{A1 v A, A1 v A2, A2 v ¬A}, {A1 v B, A1 v A2, A2 v ¬B}}, which a MUPS has two MUE corresponding to. In this regard, entaiment-based axiom pinpointing is an extension of axiom pinpointing that MUE covers also the same unsatisfiable reasons of MUPS.
As previously mentioned, the theory of entailment-based axiom pinpointing is built on atomic entailment. For an incoherent terminology, we need to know the atomic entailments of each axiom instead. We give a syntactic decomposition notion to achieve this goal.
We give an overview of different kind of transformations that calculate the set of atomic entailment for an axiom in a terminology. Given a terminology T and an axiom α : C v D where C is a atomic concept, apply the following transformation rules to α in each step (all rules of each step are correct3): Step 1: (GCIs) Considering all such axioms C1 v D1, ..., Cn v Dn in T where Ci(1 ≤ i ≤ n) is a complex description, let D0 = (¬C1 tD1)u...u(¬Cn tDn), do C0 v D u D0, then transform D and D0, respectively.
Step 2: (Negation normal form, NNF) Push all negation signs as far as possible into the description, using de Morgan’s rules and usual rules for quantifiers4. Step 3: Repeated use of distributive law : C1 t (C2 u C3) = (C1 t C2) u (C1 t C3), ∀R.(C1 t (C2 u C3)) = ∀R.((C1 t C2) u (C1 t C3)), ∃R.(C1 u (C2 t C3)) = ∃R.((C1 u C2) t (C1 u C3)).
Step 4: Repeated use of following rules: ∀R.(C1uC2) = ∀R.C1u∀R.C2, ∃R.(C1t C2) = ∃R.C1 t ∃R.C2.
The transformation process always terminates and we end up with D = D1 u ... u Dm and D0 = D10 u ... u Dn0 where constructor u can only appear in λR.Y of Di(1 ≤ i ≤ m) and Dj0 (1 ≤ j ≤ n) while λ is constructor ∃, ≥ n, or ≤ n. Therefor, for any model I, I {α : C v D} ⇒ I C v Di(1 ≤ i ≤ m), and C v Di has no entailment but itself. Consequently, {C v D1, ..., C v Dm} is the set of atomic entailment of α. Similarly, {C v D1, ..., C v Dm, C v D10, ..., C v Dn0} is the set of atomic entailment of α in terminology T . Both the result of syntactic decomposition and the axiom have the same name and base symbols. Moreover, Since the result is obtained by a sequence of replacement steps, i.e., by replacing equals by equals. Therefore, E (α) and α are syntactically and semantically equivalent, i.e., the result is the set of all atomic entailments of α. The atomic entailments of a terminology can be calculated by merging all axioms’s. In example TBox T1, E (α1) = {A1 v A2, A1 v ∃r.A2, A1 v A3}.
On the other hand, using a rule L = R above, it means R is obtained from
L. We can mark R’s label is L. Thus, keeping track of the transformations that
occur during the processing step i.e. we can pinpoint the position of atomic
entailment in original axiom.
3 All these rules are correct and have been proved in the Description Logic
Handbook[
In this section, we discuss the algorithm for finding all MUE of an unsatisfiable concept. The algorithm we provide is reasoner-independent, in the sense that the DL reasoner is solely used as an oracle to determine concept satisfiability w.r.t a terminology. we provide the formal specification of the algorithm.
The ALL MUE(T , C, M, E) algorithm receives a local terminology T , a concept C, a local conflict M and a set of axioms E related to M directly5, and outputs the set of all minimal subsets T 0 ⊆ E (T ∪E) such that C is unsatisfiable in T 0 ∪ M . The algorithm works in three main steps: first, it utilizes CONFLICT HST to computes all related minimal contradiction of M from E for C; Then recursive call to the algorithm with the new parameters T , M , and E for each related conflict we have obtained in previous step; Finally, combining the consequences of all recursive calls and obtain the final result. The loop in the second step is a main component of algorithm, which calculates the input parameters for next recursive call, it is mainly to do the following tasks: first of all, adding the obtained related conflict m to the original conflict M to get the new local conflict M 0; Then, selecting axioms from T which is only related to the named symbols in m (because m has included all axioms related to M ) dented by the new related axioms set A for the new local conflict M 0; Last, get a new terminology T 00 by removing A from T .
We can get all MUE of C in terminology T by calling ALL MUE(T , C, ∅, ∅). Thus, the algorithm process guarantees three points as follows: (a) Both axioms and named symbols of the input terminologies T , M and E are mutually disjoint. (b) M ⊆ M for every M ∈ mue(T ∪M ∪E, C) if C is unsatisfiable in T ∪M ∪E. (c) C is satisfiable in T ∪ M if M is not a MUE for C in T ∪ M ∪ E. Theorem 2. Given an unsatisfiable concept C in a terminology T , R returned by ALL MUE(T , C, ∅, ∅) is the set of all MUE for C.
Theorem 3. The CONFLICT HST(T , C, M, E) algorithm output all minimal subset E0 ⊆ E such that C is unsatisfiable in T ∪ M ∪ E0, and C is satisfiable in T ∪ M ∪ E00 for every E00 ⊂ E0.
The CONFLICT HST(N, F, HS, C, T , M, E) algorithm generates a Hitting
Set Tree [
A ← {α ∈ T | α has the form C v D}; T 0 ← T − A;
E0 ← E(A); if C is unsatisfiable in M then /* M is a MUE of C */ R ← {M }; return R; H ← ∅; CONFLICT HST(∅, H, ∅, C, T 0, M, E0); if H = ∅ then /* H = ∅ means M is a MUE of C */ R ← {M }; return R; for m ∈ H do
M 0 ← M ∪ m; /* update the current MUE M of C */ S ← Sig(m) − D(M 0) − B(T 0 ∪ M 0);/*Select the related symbols of M 0*/ A ← {α ∈ T 0 | α has the form C0 v D0 where C0 ∈ S}; T 00 ← T 0 − A; R0 ← ALL MUE(T 00, C, M 0, E(A));
R ← R ∪ R0; return R;
/* The algorithm start with M = ∅ */
Two pruning strategy to the algorithm in order to reduce the size of HST and eliminate extraneous satisfiability tests. One is closing, if there exists a Hitting Set h in HS such that the path of N 0 is a superset of h, close node N 0 and the value is not computed for N 0 nor are any succor nodes generated, as indicted by a 0×0. The other one is reusing nodes: if there exists a node value k in F such that k and the path of N 0 are disjoint, set k as the value of N 0 directly without recalculation.
The SINGLE CONFLICT(T , C, M, E) algorithm outputs a subset of E. In the loop, the algorithm removes an axiom from E in each iteration and check whether the concept C is satisfiable w.r.t. T ∪ M ∪ E, in which case the axiom is added to R and reinserted into E. The process continues until all axioms in E have been tested. Finally, R is returned as output.
Theorem 4. The SINGLE CONFLICT(T , C, M, E) algorithm output a minimal subset R ⊆ E such that C is unsatisfiable in T ∪ M ∪ R, and C is satisfiable in T ∪ M ∪ R0 for every R0 ⊂ R.
Proof. Let R be the output of algorithm SINGLE CONFLICT(T , C, M, E). If C is satisfiable in T ∪ M ∪ E, we get R = ∅. Otherwise, C is unsatisfiable in T ∪ M ∪ R upon termination. Suppose there exists a subset R0 ⊂ R such that C is unsatisfiable in T ∪ M ∪ R0. Then, removing the axiom in R − R0 after the Algorithm: CONFLICT HST(N, F, HS, T , C, M, E) Input: a node N , a set of conflict sets F , a set of hitting sets HS,
a terminology T , a concept C, a terminology M , a terminology E Output: input F if N = ∅ then r ←SINGLE CONFLICT(T , C, M, E); if r = ∅ then
return; L(N ) ← r; F ← { }
r ; for α ∈ L(N ) do create a new node N 0 and set L(N 0) ← ∅; create a new edge e =< N, N 0 > with L(e) ← α; if there exists a set h ∈ HS s.t. h ⊆ P(N ) ∪ {α} then
L(N 0) ←0 × 0; continue; else if there exists a set k ∈ F s.t. k ∩ P(N ) = ∅ then
L(N 0) ← k;
CONFLICT HST(N 0, F, HS, T , C, M, E − {α}); else m ← SINGLE CONFLICT(T , C, M, E − {α}); if m = ∅ then
L(N 0) ←0 √ 0; HS ← HS ∪ {P(N ) ∪ {α}}; L(N 0) ← m; F ← F ∪ {m};
CONFLICT HST(N 0, F, HS, T , C, M, E − {α}); removal of R0, we get C is satisfiable in T ∪ M ∪ R0, which contradicts with the assumption.
The problem of finding minimal Hitting Sets is known to be NP-COMPLETE, our algorithm is associated with the size of the element in mue(T , C). In this case, Let n be the cardinality of mue(T , C) and S = {k1, ..., kn} be the value set of the size of its elements, the number of calls to SINGLE CONFLICT and satisfiability tests involved is at most k1 · ... · kn. 5
Our algorithms for fine-grained axiom pinpointing have been realized in JAVA (JDK 1.6)using Pellet as the black-box reasoner. Tests are performed on a standard Windows operating system (Intel(R) Core(TM)i5-3470 CPU @ 3. 20GHz, 8. 00GB).
Before providing an evaluation of our algorithm, we briefly want to discuss a case study from Pizza. Then, we give the experimental results of common ontologies.
Example 2. IceCream is an unsatisfiable concept in ontology P izza. IceCream v F ood u ∃hasT opping.F ruitT opping disjoint(IceCream, P izza) F ruitT opping v P izzaT opping disjoint(IceCream, P izzaT opping) P izzaT opping v F ood role hasT opping : domain P izza IceCream in P izza ontology has only one MUE M: M = {IceCream v ∃hasT opping.F ruitT opping, disjoint(IceCream, P izza), role hasT opping : domain P izza}
For unsatisfiable concept IceCream, taking away any single axiom from M makes IceCream satisfiable, while M is not a MUPS since IceCream v ∃hasT opping.F ruitT opping is only a part of original axiom of IceCream, which pinpoint the accurate component of contradiction within the axioms. As a consequence, the MUE indeed helped in some cases.
We have performed some preliminary experiments. We evaluated the method on five real-life OWL-DL ontologies vary in size, complexity and expressivity: Koala, MadCow, Pizza, MGED, DICE. The basic information of our experimental ontologies are depicted in Table 1, the results of test ontologies are summarized in Table 2.
According to Table 1 and Table 2, the results show that the scale of ontology and number of unsatisfiable concepts introduce an increase in the running time w.r.t. the fine-grained axiom pinpointing procedure. In the case of Koala and MadCow ontology, where the number of axioms related to an unsatisfiable concept are small (less than 10), the program ends in a very short period of time. However, for DICE ontology, where axioms responsible for an unsatisfiable concept are large in number (nearly 100), the running time of procedure is longer. Note. Columns are: the terminology T , the expressivity of termminology (L(T )), number of named symbols (|D(T )|), number of base symbols (|B(T )|), number of roles (|R|), number of axioms (|T |), number of unsatisfiable concepts (|UT |). Note. Rows are: the test terminology (T ), the sum of MUE of all unsatisfiable concepts in terminology (|MUE(T )|), the execution time of ALL MUE algorithm for all unsatisfiable concepts in terminology where the unit is millisecond (Time). 6
In order to pinpoint debugging more accurately, we use the entailments to replace the corresponding axioms, then identify a minimal unsatisfiable subset of entailments for the new terminology. A new formal definition of MUE have be provided in this paper. At the same time, we presented a black-box pinpointing algorithm to solve it. Experimental results on common ontologies show that our axiom pinpointing provides incoherent terminology with more accurate incoherent reasons without losing contradictions masked by MUPS, and the performance of our algorithm is influenced by the size of related axioms directly. For future work, we plan to adopt the dependency between concepts, investigate different kinds of selection function, that hopefully improve the efficiency of entailmentbased axiom pinpointing.
Acknowledgments. This work was supported in part by NSFC under Grant Nos. 61272208, 61133011, 41172294, 61170092; Jilin Province Science and Technology Development Plan under Grant Nos.201201011.