Relation Between Description Logics and First-Order Logic

Many description logics are decidable fragments of first-order logic (FOL), also known as first-order predicate calculus (FOPC), and many of two-variable logic or guarded logic, however, some description logics have more features than first-order logic.

Table 1. Transparent translation between FOL and DL
First-Order Logic Description Logic
A(x) A
C(a) C(a), alternatively a : C
AB A ≡ B
¬C(x) ¬C
C(x) ^ D(x) CD
C(x) ∨ D(x) CD
∀x(C(x) → D(x)) CD
R(a,b) R(a,b), alternatively (a,b) : R
xy(R(x,y) → S(x,y)) RS
∃y(R(x,y) ^ C(y)) R.C
xyz(R(x,y) → R(y,z) → R(x,z)) RRR

Despite of the feasibility of direct translation between FOL and DL, guaranteeing complete and terminating reasoning requires a different transformation, such as the structural transformation. The structural transformation is based on a conjunction normal form, which replaces FOL subformulae with new predicates, for which it also provides definitions. A major advantage of the structural transformation is that it avoids the exponential size growth of the clauses.