Syntax
Symbols
In addition to the sets B = {‘(’, ‘)’, ‘,’, ⊑}, C of atomic concepts, R of roles, and U of individuals, we add the set Cons𝓕𝓛0 = {∀, ⊓, ⊤, ‘.’} that is assumed disjoint from all other sets.
- Symbols of 𝓕𝓛0
- The symbols of 𝓕𝓛0 are Sym𝓕𝓛0 = B ⋃ C ⋃ R ⋃ U ⋃ Cons𝓕𝓛0.
Formulas
Before defining 𝓕𝓛0 formulas, we need to introduce the notion of complex concepts:
- Complex 𝓕𝓛0 concepts
-
The set of complex concepts is the minimal set that contain the following:
- every atomic concept A ∈ C is a complex concept;
- ⊤ is a complex concept;
- for all complex concepts c and d, (c ⊓ d) is a complex concept;
- for all r ∈ R and all complex concepts c, ∀r.c is a complex concept.
Then we can define 𝓕𝓛0 formulas almost exactly as proto-DL formulas except that wherever an atomic concept can be used, so can a complex concept:
- formulas of 𝓕𝓛0
-
The set For𝓕𝓛0 of 𝓕𝓛0 formulas are grouped in three kinds:
- for all complex concept c and d, c ⊑ d ∈ For𝓕𝓛0 (these formulas are called general concept inclusions or GCIs);
- for all complex concept c and a ∈ U, c(a) ∈ For𝓕𝓛0 (these formulas are just called concept assertions as in proto-DL);
- for all r ∈ R and a, b ∈ U, r(a, b) ∈ For𝓕𝓛0 (role assertions as in proto-DL).
We use a light shading on formulas in order to clearly distinguish them from other syntactic constructs.
⊤ ⊑ (C ⊓ ∀P.(D ⊓ D))
Person ⊑ ∀hasParent.Person
Semantics
Interpretations
Interpretations are identical in all description logics, so we simply assume the same definition as in proto-DL. However, given an interpretation (Δ, 𝓘), we can extend the interpretation function 𝓘 to complex concepts:
- 𝓘(⊤) = Δ;
- for all complex concepts c and d, 𝓘(c ⊓ d) = 𝓘(c) ⋂ 𝓘(d);
- for all r ∈ R and all complex concepts c, 𝓘(∀r.c) = {x ∈ Δ | for all y ∈ Δ such that (x, y) ∈ 𝓘(r), y ∈ 𝓘(c)}.
Satisfaction relation
The satisfaction relation in 𝓕𝓛0 is defined almost identical to proto-DL, except that every concept is assumed to be a complex concept:
- Satisfaction relation in 𝓕𝓛0
-
An interpretation (Δ, 𝓘) in 𝓕𝓛0 satisfies:
- a general concept inclusion c ⊑ d if and only if 𝓘(c) ⊆ 𝓘(d);
- a concept assertion c(a) if and only if 𝓘(a) ∈ 𝓘(c);
- a role assertion r(a, b) if and only if (𝓘(a), 𝓘(b)) ∈ 𝓘(r).
Properties of 𝓕𝓛0
- Consistency of 𝓕𝓛0 theories
-
Every 𝓕𝓛0 theory is consistent.
Let Δ denote the singleton {0} and let 𝓘 be the interpretation function such that for all individual c, 𝓘(c) = 0, for all atomic concept c, 𝓘(r) = {0}, and for all role r, 𝓘(r) = {(0,0)}. We can note that for all complex concept C, 𝓘(C) = {0}, and therefore, 𝓘 satisfies every concept inclusion, every concept assertion and every role assertion in 𝓔𝓛.
- Complexity of the entailment problem in 𝓕𝓛0
-
In 𝓕𝓛0, the entailment problem is decidable in exponential time with respect to the size of the input theory and formula.
Extensions of 𝓕𝓛0
Simple description logics can be extended in different ways: by adding more constructors for complex concepts (that is, augmenting the set of symbols ConsL that can be used to create complex concepts); by adding new types of formulas; by adding constructs for complex roles.
The description logic 𝓕𝓛⊥
The logic 𝓕𝓛⊥ = (Sym𝓕𝓛⊥, For𝓕𝓛⊥, Int𝓕𝓛⊥, ⊨𝓕𝓛⊥) is defined as follows:
- Sym𝓕𝓛⊥ = Sym𝓕𝓛0 ⋃ {⊥}, assuming that {⊥} is disjoint from Sym𝓕𝓛0;
- ⊥ is a complex concept and can be used in any syntactic constructions of 𝓕𝓛0 where a complex concept can be used;
- For𝓕𝓛⊥ is defined identically as For𝓕𝓛0, except that complex concepts can be any one of 𝓕𝓛⊥ rather than just those of 𝓕𝓛0;
- Int𝓕𝓛⊥ = Int𝓕𝓛0;
- interpretation functions in 𝓕𝓛⊥ are extended to complex concepts as in 𝓕𝓛0 with the addition that 𝓘(⊥) = ∅ (that is, the complex concept ⊥ is always interpreted as the empty set);
- the satisfaction relation ⊨𝓕𝓛⊥ is defined as in 𝓕𝓛0.
With the new construct ⊥, 𝓕𝓛⊥ can express the disjointness of concepts, such as Star ⊓ Planet ⊑ ⊥. This can lead to inconsistencies: for instance, the formula ⊤ ⊑ ⊥ is unsatisfiable.
The description logic 𝓕𝓛−
The logic 𝓕𝓛− = (Sym𝓕𝓛−, For𝓕𝓛−, Int𝓕𝓛−, ⊨𝓕𝓛−) is defined as follows:
- Sym𝓕𝓛− = Sym𝓕𝓛⊥ ⋃ {¬}, assuming that {¬} is disjoint from Sym𝓕𝓛⊥;
- for any atomic concept A ∈ C, ¬A is a complex concept and can be used in any syntactic constructions of 𝓕𝓛⊥ where a complex concept can be used;
- For𝓕𝓛− is defined identically as For𝓕𝓛⊥, except that complex concepts can be any one of 𝓕𝓛− rather than just those of 𝓕𝓛⊥;
- Int𝓕𝓛− = Int𝓕𝓛⊥;
- interpretation functions in 𝓕𝓛− are extended to complex concepts as in 𝓕𝓛⊥ with the addition that 𝓘(¬A) = Δ \ 𝓘(A) (that is, the complex concept ¬A is interpreted as the complement of 𝓘(A) in Δ);
- the satisfaction relation ⊨𝓕𝓛− is defined as in 𝓕𝓛⊥.
Note that the symbol ¬ can only be used in front of a concept name, not before an arbitrary complex concept. This limits the expressiveness of the logic.
The description logic 𝓐𝓛
The logic 𝓐𝓛 = (Sym𝓐𝓛, For𝓐𝓛, Int𝓐𝓛, ⊨𝓐𝓛) is defined as follows:
- Sym𝓐𝓛 = Sym𝓕𝓛− ⋃ {∃}, assuming that {∃} is disjoint from Sym𝓕𝓛−;
- for any role r ∈ R, ∃r.⊤ is a complex concept and can be used in any syntactic constructions of 𝓕𝓛− where a complex concept can be used;
- For𝓐𝓛 is defined identically as For𝓕𝓛−, except that complex concepts can be any one of 𝓐𝓛 rather than just those of 𝓕𝓛−;
- Int𝓐𝓛 = Int𝓕𝓛−;
- interpretation functions in 𝓐𝓛 are extended to complex concepts as in 𝓕𝓛− with the addition that 𝓘(∃r.⊤) = {x ∈ Δ | there is y ∈ 𝓘(c) such that (x, y) ∈ 𝓘(r)} (that is, the set of things that have a relation with something else via relation 𝓘(r));
- the satisfaction relation ⊨𝓐𝓛 is defined as in 𝓕𝓛−.
𝓐𝓛 is often considered as the archetypical description logic, from which others are defined. Starting from 𝓐𝓛, we can build a large family of DLs by adding selected features in a set of syntactic constructs. Each construct is assigned a letter that can be concatenated to 𝓐𝓛 to form the name of a particular DL (for instance 𝓐𝓛𝓒𝓘𝓞 combines the constructs of 𝓐𝓛 with general concept complement, inverse roles, and nominals).
The table below summarises some classical constructs of the 𝓐𝓛 family, grouped in three categories: concept constructs are new syntactic features that can make new kinds of complex concepts; role constructs are syntactic features than can make complex roles; axiom constructs are new types of formulas. The semantics of concept and role constructs is defined as the interpretation of complex concepts and roles in function of a DL interpretation; the semantics of new types of formulas is given as conditions on interpretations to satisfy the formulas.
| Symbol | Name | Syntax | Semantics |
|---|---|---|---|
| Concept constructs | |||
| 𝓐 | Value restriction (already in 𝓐𝓛) | ∀r.c | {x ∈ Δ | for all y ∈ Δ such that (x, y) ∈ 𝓘(r), y ∈ 𝓘(c)} |
| 𝓔 | General existential quantification | ∃r.c | {x ∈ Δ | there exists y ∈ c such that (x, y) ∈ 𝓘(r)} |
| 𝓤 | Concept disjunction | c ⊔ d | 𝓘(c) ⋃ 𝓘(c) |
| 𝓒 | General concept complement | ¬c | Δ \ 𝓘(c) |
| 𝓞 | Nominal | {a} | {𝓘(a)} |
| 𝓝 | Cardinality restriction | ≤n.r | {x ∈ Δ | card({y ∈ Δ | (x, y) ∈ 𝓘(r)}) ≤ n |
| ≥n.r | {x ∈ Δ | card({y ∈ Δ | (x, y) ∈ 𝓘(r)}) ≥ n | ||
| 𝓠 | Qualified cardinality restriction | ≤n.r.c | {x ∈ Δ | card({y ∈ 𝓘(c) | (x, y) ∈ 𝓘(r)}) ≤ n} |
| ≥n.r.c | {x ∈ Δ | card({y ∈ 𝓘(c) | (x, y) ∈ 𝓘(r)}) ≥ n} | ||
| Role constructs | |||
| 𝓘 | Inverse role | r− | {(x, y) ∈ Δ × Δ | (y, x) ∈ 𝓘(r)} |
| (⋂) | Role conjunction | r ⊓r s | 𝓘(r) ⋂ 𝓘(s) |
| (⋃) | Role disjunction | r ⊔r s | 𝓘(r) ⋃ 𝓘(s) |
| (¬) | Role complement | ¬rr | Δ × Δ \ 𝓘(r) |
| Additional axioms | |||
| 𝓕 | Role functionality | ⊤ ⊑ ≤1.r | if (x, y) ∈ 𝓘(r) and (x, z) ∈ 𝓘(r) then x = z |
| 𝓗 | Role hierarchy | r ⊑r s | 𝓘(r) ⊆ 𝓘(s) |
| 𝓢 | 𝓐𝓛𝓒 + Role transitivity | Trans(r) | if (x, y) ∈ 𝓘(r) and (y, z) ∈ 𝓘(r) then (x, z) ∈ 𝓘(r) |
| 𝓡 | Role chain | r1 ∘ … ∘ rn ⊑r s | if (x, y1) ∈ 𝓘(r1), …, (yi, yi+1) ∈ 𝓘(ri+1), … then (x, yn) ∈ 𝓘(s) |
Note that 𝓢 is used as a shortcut for 𝓐𝓛𝓒 + transitivity, so the logic 𝓢𝓗𝓘 denotes the DL that has general complement, role transitivity, role hierarchy, and role inverse.
Role constructs in parenthesis are added at the end of the name, all in one pair of parentheses: 𝓐𝓛𝓒(⋂,⋃).
Some constructs subsume others. In particular, 𝓠 subsumes 𝓝, 𝓝 subsumes 𝓕, 𝓔𝓒 subsumes 𝓐, 𝓐𝓒 subsumes 𝓔, 𝓐𝓛𝓒 subsumes 𝓤𝓔, 𝓡 subsumes 𝓢𝓗, (¬,⋂) subsumes (⋃), and (¬,⋃) subsumes (⋂).