Editing Description logic (section)

====The description logic ALC====
The prototypical DL ''Attributive Concept Language with Complements'' (<math>\mathcal{ALC}</math>) was introduced by Manfred Schmidt-Schauß and Gert Smolka in 1991, and is the basis of many more expressive DLs.<ref name="DLHB"/> The following definitions follow the treatment in Baader et al.<ref name="DLHB"/>

Let <math>N_C</math>, <math>N_R</math> and <math>N_O</math>  be (respectively) [[Set (mathematics)|sets]] of ''concept names'' (also known as ''atomic concepts''), ''role names'' and ''individual names'' (also known as ''individuals'', ''nominals'' or ''objects''). Then the ordered triple (<math>N_C</math>, <math>N_R</math>, <math>N_O</math>) is the ''signature''.

=====Concepts=====
The set of <math>\mathcal{ALC}</math> ''concepts'' is the smallest set such that:

* The following are ''concepts'':
** <math>\top</math> (''top'' is a ''concept'')
** <math>\bot</math> (''bottom'' is a ''concept'')
** Every <math>A \in N_C</math> (all ''atomic concepts'' are ''concepts'')
* If <math>C</math> and <math>D</math> are ''concepts'' and <math>R \in N_R</math> then the following are ''concepts'':
** <math>C\sqcap D</math> (the intersection of two ''concepts'' is a ''concept'')
** <math>C\sqcup D</math> (the union of two ''concepts'' is a ''concept'')
** <math>\neg C</math> (the complement of a ''concept'' is a ''concept'')
** <math>\forall R.C</math> (the universal restriction of a ''concept'' by a ''role'' is a ''concept'')
** <math>\exists R.C</math> (the existential restriction of a ''concept'' by a ''role'' is a ''concept'')

=====Terminological axioms=====
A ''general concept inclusion'' (GCI) has the form <math>C \sqsubseteq D</math> where <math>C</math> and <math>D</math> are ''concepts''. Write <math>C \equiv D</math> when <math>C \sqsubseteq D</math> and <math>D \sqsubseteq C</math>. A ''TBox'' is any finite set of GCIs.

=====Assertional axioms=====
{{Anchor|concept_assertion}}
* A ''concept assertion'' is a statement of the form <math>a : C</math> where  <math>a \in N_O</math> and C is a ''concept''.
* A ''role assertion'' is a statement of the form <math>(a,b) : R</math> where <math>a, b \in N_O</math>  and R is a ''role''.

An ''ABox'' is a finite set of assertional axioms.

=====Knowledge base=====
A ''knowledge base'' (KB) is an ordered pair <math>(\mathcal{T}, \mathcal{A})</math> for [[abox|TBox]] <math>\mathcal{T}</math> and [[Abox|ABox]] <math>\mathcal{A}</math>.