Editing Description logic (section)

===Syntax===
The syntax of a member of the description logic family is characterized by its recursive definition, in which the constructors that can be used to form concept terms are stated. Some constructors are related to logical constructors in [[first-order logic]] (FOL) such as ''[[intersection (set theory)|intersection]]'' or ''[[logical conjunction|conjunction]]'' of concepts, ''[[union (set theory)|union]]'' or ''[[disjunction]]'' of concepts, ''[[negation]]'' or ''[[complement (set theory)|complement]]'' of concepts, ''[[Universal quantifier|universal restriction]]'' and ''[[Existential quantifier|existential restriction]]''. Other constructors have no corresponding construction in FOL including restrictions on roles for example, inverse, [[transitive relation|transitivity]] and functionality.

====Notation====
Let C and D be concepts, a and b be individuals, and R be a role.

If a is R-related to b, then b is called an R-successor of a.

{| style="width:100%;"  class="wikitable sortable"
|+ Conventional Notation
|-
! Symbol
! Description
! Example
! Read
|-
| <math>\top</math>
| ⊤ is a special concept with every individual as an instance
| <math>\top</math>
| top
|-
| <math>\bot</math>
| [[empty set|empty]] concept
| <math>\bot</math>
| bottom
|-
| <math>\sqcap</math>
| ''[[intersection (set theory)|intersection]]'' or ''[[logical conjunction|conjunction]]'' of concepts
| <math>C \sqcap D</math>
| C and D
|-
| <math>\sqcup</math>
| ''[[union (set theory)|union]]'' or ''[[disjunction]]'' of concepts
| <math>C \sqcup D</math>
| C or D
|-
| <math>\neg </math>
| ''[[negation]]'' or ''[[complement (set theory)|complement]]'' of concepts
| <math>\neg C</math>
| not C
|-
| <math>\forall </math>
| ''[[Universal quantifier|universal restriction]]''
| <math>\forall R.C</math>
| all R-successors are in C
|-
| <math>\exists </math>
| ''[[Existential quantifier|existential restriction]]''
| <math>\exists R.C</math>
| an R-successor exists in C
|-
| <math>\sqsubseteq</math>
| Concept ''inclusion''
| <math>C \sqsubseteq D</math>
| all C are D
|-
| <math>\equiv </math>
| Concept ''equivalence''
| <math>C \equiv D</math>
| C is equivalent to D
|-
| <math>\dot = </math>
| Concept ''definition''
| <math>C \dot = D</math>
| C is defined to be equal to D
|-
| <math> : </math>
| Concept ''assertion''
| <math>a : C</math>
| a is a C
|-
| <math> : </math>
| Role ''assertion''
| <math>(a,b) : R</math>
| a is R-related to b
|}

====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>.