Past exam of the computer science course of the University of Oxford / 2015 / Knowledge representation and reasoning / 2 / a

An initial split into an acyclic definition and the remaining general concept inclusions isThe definition of $C$ is suitable for TBox unfolding: its right-hand side does not depend on $C$, and $C$ has only this defining left-hand side. The other displayed general concept inclusions do not initially have an atomic defined left-hand side. In particular, $A\sqcap B⊑\perp$ can be rewritten for TBox absorption, but is not already an atomic definition.

Absorb (4) using the equivalenceThus we can takeHere $A⊑\neg B$ is a primitive inclusion, handled by adding $\neg B$ whenever $A$ labels a node. For literal substitution-based TBox unfolding, introduce a fresh description logic concept $A_0$ and replace the primitive inclusion byThis preserves the original models after forgetting $A_0$: any model of the primitive inclusion extends by taking $A_0=A$, and any model of the new definition satisfies the primitive inclusion. The fresh name is important. Replacing $A$ by $\neg B$ alone would incorrectly assert that every non-$B$ element is an $A$ element.