# «1 Motivation The Ontology Engineering community widely agrees on the importance of helping the user understand the output of a DL reasoner. The most ...»

Beyond Asserted Axioms: Fine-Grain

Justiﬁcations for OWL-DL Entailments

Aditya Kalyanpur1 and Bijan Parsia1 and Bernardo Cuenca Grau2

University of Maryland, USA1, University of Manchester, UK2

aditya@cs.umd.edu, bparsia@isr.umd.edu, bcg@cs.man.ac.uk

1 Motivation

The Ontology Engineering community widely agrees on the importance of helping

the user understand the output of a DL reasoner. The most recent approaches to the

problem [4] [3] are based on the notion of a Minimal Unsatisﬁability Preserving SubTBoxes (MUPS). Roughly, a MUPS for an atomic concept A is a minimal fragment T ⊆ T of a TBox T in which A is unsatisﬁable.

**For example, given the TBox:**

B ∃R.D E ¬B, 2: C ≥ 1.R 1: A C F ∀R.¬D, 4: B ¬D E 3: A E where the concept A is unsatisﬁable, the TBox T = {1} is a MUPS for A in T.

In our earlier work [2], we extended the notion of a MUPS to arbitrary entailments in SHOIN and devised a non-standard inference service, axiom pinpointing, which, given T any of its logical consequences α, determines the minimal fragments of T in which α holds.

However, these services, though useful for debugging and explanation purposes, suffer from a fundamental granularity problem: since they work at the asserted axiom level, they fail to determine which parts of the asserted axioms are irrelevant for the particular entailment under consideration to hold. For instance, in our example, the conjunct E in axiom 1 is irrelevant for the unsatisﬁability of A. Moreover, additional parts of axioms that could contribute to the entailment are masked, e.g., the axioms ∃R.D and A ∀R.¬D which also entail the 1, 3 can be broken down into A unsatisﬁability of A, however, this condition cannot be captured.

In this paper, we aim at extending the axiom pinpointing service to capture precise justiﬁcations, which are at a ﬁner granularity level than the original asserted axioms.

In this context, we provide a formal notion of precise justiﬁcation and propose a decision procedure for the problem. We discuss implementation details of the service and show that it is feasible in practice. Our results are applicable to SHOIN and hence to OWL-DL.

2 Precise Justiﬁcations Since we aim at identifying relevant parts of axioms, we deﬁne a function that splits the axioms in a TBox T into “smaller” axioms to obtain an equivalent TBox Ts that contains as many axioms as possible.

Deﬁnition 1 (split KB) Given a SHOIN concept C in negation normal form (NNF),

**the function split(C) returns a set of concepts, inductively deﬁned as follows:**

split(C) ← C, if C is A, ¬A, ≥ n.R, ≤ n.R, = n.R,, ⊥ or a nominal node {o} split(C D) ← split(C) ∪ split(D) split(C D) ← (split(C) ⊗ split(D)) split(∀R.C) ← ∀R. (split(C)) split(∃R.C ) – we get two cases depending on C if C is of the form C D, split(∃R.C ) ← ∃R.E ∪ split(¬E C) ∪ split(¬E D) ∪ split((¬C ¬D) E), where E is a fresh concept else, split(∃R.C ) ← ∃R. split(C ) Given a KB = {α1, α2,...αn }, where each axiom αi is of the form Ci Di, let Cα be the concept representing α, i.e., ¬Ci Di, converted to NNF. Then, Ts = Cs for each concept Cs ∈ split(¬C1 D1 ) ∪ split(¬C2 split KB() = D2 )..split(¬Cn Dn ).

**A justiﬁcation is a generalization of the notion of a MUPS for arbitrary entailments:**

Deﬁnition 2 (Justiﬁcation) Let T |= α where α is an axiom. A fragment T ⊆ T is a justiﬁcation for α in T if T |= α, and T |= α for every T ⊂ T.

We denote by JUST(α, T ) the set of all justiﬁcations for α in T.

**Finer-grained justiﬁcations can be deﬁned as follows:**

Deﬁnition 3 (Precise Justiﬁcation) Let T |= α. A TBox T is a precise justiﬁcation for α in T if T ∈ JUST(α, split TBox(T )).

We denote by JUSTp (α, T ) the set of all precise justiﬁcations for α in T.

In SHOIN, entailment can be reduced to concept unsatisﬁability. As a consequence, it is easy to show that the problem of ﬁnding all the justiﬁcations for an unsatisﬁable concept and the problem of ﬁnding all the justiﬁcations for a given entailment can be reduced to each other. In what follows, we shall restrict our attention, without loss of generality, to the problem of ﬁnding all the precise justiﬁcations for an unsatisﬁable concept w.r.t to a SHOIN TBox.

3 Finding Precise Justiﬁcations The problem of ﬁnding all precise justiﬁcations for an entailment α of a TBox T now reduces to the problem of ﬁnding all justiﬁcations for α in the split T Box(T ). Thus, we can use the algorithm listed in Table 1 to split a TBox, and then apply any decision procedure to ﬁnd all justiﬁcations for the entailment in the split version of the TBox.

We brieﬂy sketch the algorithm we have developed in our earlier work to ﬁnd all justiﬁcations for an arbitrary entailment in a TBox. For details, we refer the reader to the technical report [2].

The ﬁrst part of the algorithm is based on the decision procedure for concept satisability in SHOIN [1], and it ﬁnds any one arbitrary justiﬁcation for the entailment.

It keeps track of the axioms from the TBox responsible for each change in the completion graph, namely, the addition of a particular concept (or role) to the label of a speciﬁc node (or edge), the addition of an equality (merge) or inequality relation between nodes, or the detection of a contradiction (clash) in the label of a node.

In order to ensure correctness, our algorithm imposes an ordering among the deterministic rules: the unfolding and CE rules are only applied when no other deterministic rule is applicable. The rationale for this strategy relies on the deﬁnition of justiﬁcation that establishes minimality w.r.t. the number of axioms considered; the new rules cause new axioms to be considered in the tracing process and additional axioms should only be considered if strictly necessary.

The algorithm works on a tree T of completion graphs. that is incrementally built using the set of available expansion rules, and the traces for the events triggered by the rules are updated on the ﬂy. For a full speciﬁcation of the expansion rules, we refer the reader to [2]. The application of non-deterministic rules results in the addition of new completion graphs as leaves of T, one for each different non-deterministic choice. However, since C is unsatisﬁable w.r.t. T, the algorithm detects a clash in each of the leaves. Upon termination, the trace of the detected clash (or clashes) in the leaves of T yields a justiﬁcation.

Once a single justiﬁcation has been found, we ﬁnd the remaining justiﬁcations by employing a variation of the classical Hitting Set Tree (HST) algorithm.

Given a collection S of conﬂict sets, Reiter’s algorithm constructs a labeled tree

**called Hitting Set Tree (HST). Nodes in an HST are labeled with a set s ∈ S and:**

1) if H(v) is the set of edge labels on the path from the root to the node v, then L(v) ∩ H(v) = ∅; 2) for each σ ∈ L(v), v has a successor w and L( v, w ) = σ; 3) if L(v) = ∅, then H(v) is a hitting set for S.

In our approach, we form an HST where nodes correspond to single justiﬁcation sets (computed on the ﬂy), edges correspond to the removal of axioms from the KB, and in building the tree to compute all the minimal hitting sets, we in turn obtain all the justiﬁcation sets as well. The correctness and completeness of this approach is provided in [2].

4 Implementation Issues We have shown in [3], [2] that the axiom pinpointing service used to ﬁnd all justications for an entailment of a SHOIN KB performs reasonably well on a lot of real-world OWL-DL ontologies.

The main additional overhead incurred for capturing precise justiﬁcations is due to the pre-processing phase where we split the KB. The concern here, from a reasoning point of view, is the introduction of GCIs during the splitting process, e.g. A ≡ B C is replaced by (among other things) B C A. Even though these GCIs are absorbed, they still manifest as disjunctions and hence adversely affect the tableau reasoning process. 2 Alternately, a more optimal implementation is the following: instead of splitting the entire KB beforehand, we can perform a lazy splitting of certain speciﬁc axioms (on the ﬂy) in order to improve the performance of the algorithm. The modiﬁed

**algorithm with lazy splitting becomes:**

• Given A unsatisﬁable w.r.t T, ﬁnd a single justiﬁcation set, J ∈ JUST(A ≡ ⊥, T )

• Split axioms in J to give Js. Prune Js to arrive at a minimal precise justiﬁcation set Jp In this case, it is possible to introduce a new absorption rule in the reasoner which would transform axioms of the form B A, C A, B C A to A ≡ B C internally. This obviously seems odd given that we split the KB initially and re-combine axioms back in the reasoner, but note that the goal here is ﬁnding precise justiﬁcations.

• Replace J by Js in T.

• Form Reiter’s HST using Jp as a node, with each outgoing edge being an axiom α ∈ Jp that is removed from T The advantage of this approach is that it only splits axioms in the intermediate justiﬁcation sets in order to arrive at precise justiﬁcations, and re-inserts split axioms back into the KB dynamically. For details of the procedure, see [2] 5 Conclusion and Future Work We have implemented the axiom pinpointing service in the OWL-DL reasoner, Pellet, and exposed it in the OWL Ontology Editor, Swoop. We are in the process of extending it to capture precise justiﬁcations.

From a UI perspective, maintaining the correspondence between the subaxioms in the precise justiﬁcation and the original asserted axioms is useful, as it allows us to strike out irrelevant parts of the axioms directly, which is helpful to understand the entailment better. (see Figure 5).

As future work, we plan to optimize the implementation and do a thorough performance and usability evaluation.

Figure 1: Justiﬁcation for MaleStudentWith3Daughters Person in the Koala OWL Ontology References [1] Ian Horrocks and Ulrike Sattler. A tableaux decision procedure for SHOIQ. In Proc. of IJCAI 2005, 2005.

[2] Aditya Kalyanpur, Bijan Parsia, Bernardo Cuenca, and Evren Sirin. Axiom pinpointing: Finding (precise) justiﬁcations for arbitrary entailments in OWL-DL, 2006. Available at http://www.mindswap.org/papers/2006/AxiomPinpointing.pdf.

[3] Aditya Kalyanpur, Bijan Parsia, Evren Sirin, and James Hendler. Debugging unsatisﬁable classes in OWL ontologies. J. of Web Semantics, Vol 3, Issue 4, 2005.

[4] S. Schlobach and R. Cornet. Non-standard reasoning services for the debugging