Entailment Checking Description Logic

Question

I am reading a research paper in Description Logic. Say L be a knowledge base which consists of axioms. Then $C \sqsubseteq D$ is an axiom.

Theorem: L $\vDash C \sqsubseteq D $ iff L $\vDash C \sqcap \neg D $

I know that to check an axiom (A) entails a knowledge base, we have to take negation of the axiom ($\neg$A) and add it to the knowledge base and we have to check whether the new knowledge base is inconsistent or not. If it is inconsistent, then the axiom entails the knowledge base. The above-stated theorem is confusing to me.

Answer 1

Hint

See Description logic. I assume that, for a knowledge base $L$ and an axiom $A$ the definition of entailment is :

$L \vDash A$ iff for any interpretation $\mathcal I$ with domain $\Delta^\mathcal I$, if $\mathcal I \vDash L$, then $\mathcal I \vDash A$.

If so, consider the first "half" of the theorem; we assume that $L \vDash C \sqsubseteq D$, and consider an interpretation $\mathcal I$ such that $\mathcal I \vDash L$.

By the above definition, we have that $\mathcal I \vDash C \sqsubseteq D$ iff $C^{\mathcal I} \subseteq D^{\mathcal I}$ and, by properties of set operations, iff $C^{\mathcal I} \cap (\Delta^\mathcal I \backslash D^{\mathcal I})$ (where $(\Delta^\mathcal I \backslash D^{\mathcal I})$ denotes the complement of $D^{\mathcal I}$).

But $C^{\mathcal I} \cap (\Delta^\mathcal I \backslash D^{\mathcal I})$ implies : $\mathcal I \vDash C \sqcap \lnot D$, and thus we have proved that :

if $\mathcal I \vDash L$, then $\mathcal I \vDash C \sqcap \lnot D$,

i.e. $L \vDash C \sqcap \lnot D$.

In conclusion, we have proved that :

if $L \vDash C \sqsubseteq D$, then $L \vDash C \sqcap \lnot D$.

---

The same approach must be used for the other "half" of the theorem ...