Editing Description logic (section)

==Formal description==
Like [[first-order logic]] (FOL), a [[Syntax (logic)|syntax]] defines which collections of symbols are legal expressions in a description logic, and [[semantics]] determine meaning. Unlike FOL, a DL may have several well known syntactic variants.<ref name="HS"/>

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

===Semantics===
The [[semantics]] of description logics are defined by interpreting concepts as sets of individuals and roles as sets of ordered pairs of individuals. Those individuals are typically assumed from a given domain. The semantics of non-atomic concepts and roles is then defined in terms of atomic concepts and roles. This is done by using a recursive definition similar to the syntax.

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