Editing Description logic (section)

====The description logic ALC====
The following definitions follow the treatment in Baader et al.<ref name="DLHB"/>

A ''terminological interpretation'' <math>\mathcal{I}=(\Delta^{\mathcal{I}}, \cdot^{\mathcal{I}})</math> over a ''signature'' <math>(N_C,N_R,N_O)</math> consists of
* a non-empty set <math>\Delta^{\mathcal{I}}</math> called the [[domain of discourse|''domain'']]
* a ''interpretation function'' <math>\cdot^{\mathcal{I}}</math> that maps:
** every ''individual'' <math>a</math> to an element <math>a^{\mathcal{I}} \in \Delta^{\mathcal{I}}</math>
** every ''concept'' to a subset of <math>\Delta^{\mathcal{I}}</math>
** every ''role name'' to a subset of <math>\Delta^{\mathcal{I}}  \times \Delta^{\mathcal{I}}</math>
such that
* <math>\top^{\mathcal{I}} = \Delta^{\mathcal{I}}</math>
* <math>\bot^{\mathcal{I}} = \emptyset</math>
* <math>(C \sqcup D)^{\mathcal{I}} = C^{\mathcal{I}} \cup D^{\mathcal{I}}</math> ''([[union (set theory)|union]] means [[disjunction]])''
* <math>(C \sqcap D)^{\mathcal{I}} = C^{\mathcal{I}} \cap D^{\mathcal{I}}</math> ''([[intersection (set theory)|intersection]] means [[Logical conjunction|conjunction]])''
* <math>(\neg C)^{\mathcal{I}} = \Delta^{\mathcal{I}} \setminus C^{\mathcal{I}} </math> ''([[complement (set theory)|complement]] means [[negation]])''
* <math>(\forall R.C)^{\mathcal{I}} = \{x \in \Delta^{\mathcal{I}} | \text{for} \; \text{every} \; y, (x,y) \in R^{\mathcal{I}} \;  \text{implies} \; y \in C^{\mathcal{I}} \} </math>
* <math>(\exists R.C)^{\mathcal{I}} = \{x \in \Delta^{\mathcal{I}} | \text{there} \; \text{exists} \; y, (x,y) \in R^{\mathcal{I}} \; \text{and} \; y \in C^{\mathcal{I}}\} </math>

Define <math>\mathcal{I} \models</math> (read ''in I holds'') as follows

=====TBox=====
* <math>\mathcal{I} \models C \sqsubseteq D</math> if and only if <math>C^{\mathcal{I}} \subseteq D^{\mathcal{I}}</math>
* <math>\mathcal{I} \models \mathcal{T}</math> if and only if <math>\mathcal{I} \models \Phi</math> for every <math>\Phi \in \mathcal{T}</math>

=====ABox=====
* <math>\mathcal{I} \models a : C</math> if and only if <math>a^{\mathcal{I}} \in C^{\mathcal{I}}</math>
* <math>\mathcal{I} \models (a,b) : R</math> if and only if <math>(a^{\mathcal{I}},b^{\mathcal{I}}) \in R^{\mathcal{I}}</math>
* <math>\mathcal{I} \models \mathcal{A}</math> if and only if <math>\mathcal{I} \models \phi</math> for every <math>\phi \in \mathcal{A}</math>

=====Knowledge base=====
Let <math>\mathcal{K} = (\mathcal{T}, \mathcal{A})</math> be a knowledge base.

* <math>\mathcal{I} \models \mathcal{K}</math> if and only if <math>\mathcal{I} \models \mathcal{T}</math> and <math>\mathcal{I} \models \mathcal{A}</math>