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 CI. 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.