Knowledge Representation and Reasoning: The EL family of Description Logics

This page defines several description logics that have in common the ability to define concepts (that is, classes of things) based on the existence of some values in relation to the instances of the class (the 𝓔 in 𝓔𝓛 refers to “existential”). We start by defining the logic 𝓔𝓛 as the tuple (Sym_𝓔𝓛, For_𝓔𝓛, Int_𝓔𝓛, ⊨_𝓔𝓛) that we introduce piece by piece in later sections.

We assume all the definitions from the basics of Description Logics are in place, so we only show here the additional or modified definitions.

Syntax

Symbols

In addition to the sets B = {‘(’, ‘)’, ‘,’, ⊑}, C of atomic concepts, R of roles, and U of individuals, we add the set Cons_𝓔𝓛 = {∃, ⊓, ⊤, ‘.’} that is assumed disjoint from all other sets.

Symbols of 𝓔𝓛: The symbols of 𝓔𝓛 are Sym_𝓔𝓛 = B ⋃ C ⋃ R ⋃ U ⋃ Cons_𝓔𝓛.

Formulas

Before defining 𝓔𝓛 formulas, we need to introduce the notion of complex concepts:

Complex 𝓔𝓛 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 𝓔𝓛 formulas almost exactly as proto-DL formulas except that wherever an atomic concept can be used, so can a complex concept:

formulas of 𝓔𝓛

The set For_𝓔𝓛 of _𝓔𝓛 formulas are grouped in three kinds:

for all complex concept c and d, c ⊑ d ∈ For_𝓔𝓛 (these formulas are called general concept inclusions or GCIs);
for all complex concept c and a ∈ U, c(a) ∈ For_𝓔𝓛 (these formulas are just called concept assertions as in proto-DL);
for all r ∈ R and a, b ∈ U, r(a, b) ∈ For_𝓔𝓛 (role assertions as in proto-DL).

We use a light shading on formulas in order to clearly distinguish them from other syntactic constructs.

∃hasParent.Person ⊑ Person

Mother ⊑ (∃hasChild.Person ⊓ Woman)

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 concept:

𝓘(⊤) = Δ;
for all complex concepts c and d, 𝓘(c ⊓ d) = 𝓘(c) ⋂ 𝓘(d);
for all r ∈ R and all complex concepts c, 𝓘(∃r.c) = {x ∈ Δ | there is y ∈ 𝓘(c) such that (x, y) ∈ 𝓘(r)}.

Satisfaction relation

The satisfaction relation in 𝓔𝓛 is defined almost identically to proto-DL, except that every concept is assumed to be a complex concept:

Satisfaction relation in 𝓔𝓛

An interpretation (Δ, 𝓘) in 𝓔𝓛 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 𝓔𝓛

These are a few properties of the logic 𝓔𝓛:

Consistency of 𝓔𝓛 theories

Every 𝓔𝓛 theory is consistent.

Let Δ denotes the singleton {0} and let 𝓘 be the interpretation function such that for all individual a, 𝓘(a) = 0, for all atomic concept A, 𝓘(A) = {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 𝓔𝓛 reasoning

In 𝓔𝓛, the entailment problem is decidable in polynomial time with respect to the size of the input theory and formula.

Todo... this may be quite complicated.

Extensions of 𝓔𝓛

The DL 𝓔𝓛 can be extended in a way similar to the 𝓐𝓛 family using constructors from Table 1. However, to maintain desirable computational properties, there are extensions of 𝓔𝓛 that are worth noting, most particularly 𝓔𝓛++.

The Description Logic 𝓔𝓛 and its extensions