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

Using the absorbed TBox with its primitive inclusion, translate description logic concepts as unary predicates and description logic roles as binary predicates. Concept satisfiability means that some element belongs to $A\sqcap C$, while every element satisfies the TBox axioms. The required first-order sentence isOnly ${\mathcal{T}}_u$ is included here, as requested. There is no requirement to satisfy (1), (2) or (3). For instance, one element with $A=C=\{d\}$, $B=\varnothing$ and $P=\{(d,d)\}$ satisfies this first-order sentence.

Alternatively, unfolding the absorbed TBox first gives the existential first-order sentence $\exists x\exists y(A_0(x)\wedge \neg B(x)\wedge P(x,y))$. The interpretation of the eliminated names is then recovered by $A=A_0\setminus B$ and $C=\{x:\exists yP(x,y)\}$.