Translation to FOPL

As we have seen, the notation is different from the predicate logic one, but semantically, (some of) the description logics are subsets of first order predicate logic. A concept corresponds to an unary predicate while a role corresponds to a binary predicate. More formally, a concept C corresponds to a predicate logic formula ϕ_C(x) with one free variable x such that for every interpretation I the set of elements of Δ^I satisfying ϕ_C(x) is exactly C^I. An atomic concept A is translated into the formula A(x), the constructors intersection, union, and negation are translated into logical conjunction, disjunction, and negation. If C is translated to ϕ_C(x) and R is an atomic role, then ∃R.C and ∀R.C are translated as

where y is a new variable. For further details of relationship between first order predicate logic and description logics see The Description Logic Handbook.