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.
| First-Order Logic | Description Logic |
|---|---|
| A(x) | A |
| C(a) | C(a), alternatively a : C |
| A ≈ B | A ≡ B |
| ¬C(x) | ¬C |
| C(x) ^ D(x) | C ⊓ D |
| C(x) ∨ D(x) | C ⊔ D |
| ∀x(C(x) → D(x)) | C ⊑ D |
| R(a,b) | R(a,b), alternatively (a,b) : R |
| ∀x∀y(R(x,y) → S(x,y)) | R ⊑ S |
| ∃y(R(x,y) ^ C(y)) | ∃R.C |
| ∀x∀y∀z(R(x,y) → R(y,z) → R(x,z)) | R ◦ R ⊑ R |
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.