Theory

Introduction

An Ontology is a machine-readable representation of things, groups of things, and relationships between things.

ALC DL formalises ontologies as follows:

• Things are referred to as instances
• Groups of things are referred to as classes
• Relationships between things are referred to as relations
• Negation of elements in the domain
• Conjunction and Disjunction of elements in the domain
• Quialifiers: Universal restrictions and Existential Restrictions
• Domain hierarchies (i.e. subclasses)

Syntax

Algorithm

expansion phase

1. Determine if the ontology O is empty
   • if O is empty, then the justification is an empty set.
2. Else, for each premise i in O:
   • Add i to J
   • Test if J entails the Conclusion, if so, go to the contraction phase

contraction phase

1. For each premise i in J:
   • if J without i entails the conclusion, then remove i from J.

Algorithm (brute-force)

1. We start by computing the power set of the ontology O and set it to S.
2. We then test each element ι ∈ S for justifications of η.
3. Then we create a new set J′ = {ι|∀ι ∈ S, ι |= η}.
4. We then remove all duplicate justifications in J′.

Reiter’s Hitting Set Tree

We denote intermediate nodes with v and successor nodes v′, which are connected to v by an edge with a premise α such that α is in the justification contained in v but not in the justification contained in v′ . When v ′ ≡ ∅, then it is a leaf node. Furthermore, for any node v′′, the set of premises that are in the path from the root to the node v′′ do not intersect with the justification in v′′.

1. We begin by choosing a premise α ∈ v which is not in the edges of the children of node v.
2. We then let S be the disjunction of the chosen premises {α} and the set of premises found in the path traced from v to the root node of the tree. Then we set O ′ ← O\S.
3. We test if the new ontology O ′ entails η . If that is the case, we compute a justification J for η using the new ontology O ′ . Whereas if the new ontologyO ′ does not entail η, we set the justification J = ∅
4. We then make a new node v ′ and set its justification to be J
5. We add an edge e between v and v ′ , and we label e with the premise α
6. We reinsert all the premises in S back into O.

The algorithm is repeated until no new successor nodes can be generated. Upon termination, all the intermediate nodes form a new set of all the justifications for the entailment η.

Introduction

We define an explanation Σ(η) of an entailment η to be a
pair (J , {ε_1 , ε_2 , ε_3 , ..., ε_n }), where J is a justification for an entailment η and {ε_1 , ε_2 , ε_3 , ..., ε_n } is a minimal set of intermediate entailments that link the justification J to the entailment η. The minimality of {ε_1 , ε_2 , ε_3 , ..., ε_n } implies that if an entailment β ∈ {ε_1 , ε_2 , ε_3 , ..., ε_n } is removed then {ε_1 , ε_2 , ε_3 , ..., ε_n }\β cannot logically link η with J.

Lemmatization

Suppose we have an ontology O from which we derive a justification J for an entailment η whereby O entails η. The goal is to lemmatise J into J′ such that J′ is “less complex” than J.

Proof Tree Generation

The above figure illustrates what a construction of an explanation for an entailment E looks like. In this case, η = E, J = {ax1, ax2, ax3, ax4, ax5}, and {ε_1 , ε_2 , ε_3 , ..., ε_n } = {le1, le2}. We observe that {ax1, ax2} |= le1, {ax3, ax4, ax5} entails le2, and {le1, le2} entails E. Without le1 and/or le2, it cannot be proven that η entails E.

Example input

Contact us if you have any questions

• Theory: Mr S. Malesa
  mlssol001@myuct.ac.za

• Practical: Mr P.C. Pretorius
  prtpie003@myuct.ac.za

• Supervisor: Prof T. Meyer
  tmeyer@cs.uct.ac.za