I =  AZ
true I =
false
 (  C') T  =
Fc(y)
(C D) Z = C X
D
FC(Y) FD(Y)
(C D) T = C T D T
FC(Y) FD(Y)
(P.C) x =   {a ∈ Δ x |  b.(a, b) ∈ P x   b ∈ C x }  
x.Fp(y, x)  Fc(x)
( P .C ) x =   {a ∈ Δ x |  b (a, b) ∈ P x ⇒ b ∈ C x }
x.Fp(y,x) ⇒ Fc(x)
(p: C) x =   {a ∈ dom px | px(a) ∈ Cx }
x.Fp(y,x) Fc(x)
p q x =   {a ∈ dom p x    dom q x | p x (a) = q x (a)}     (x . F p (γ, x)    F q (γ, x))
p q x =  {a ∈ dom p x   dom q x | p x (a) ≠ q x (a)}    ( x, y.F p (γ, x)   F q (γ, y))
(p) x = 
x.Fp(y,x)
(p q) x = p x q x
(x,y,Fp(y,x) Fq(y,y) → x ≠ y)

| x.F p (α, x)    F q ( x, β)   |
|-------------------------------|

respectively. It is worth noting that the extensional semantics of the left column gives also an interpretation for the formulas of the right column so that the following proposition holds.

Proposition 2.1 (Concepts vs. fol formulæ) Let   be an ALCF concept expression.

Then the transformational semantics of Figure 2 maps    into a logically equivalent first order formula.

A terminology or TBox is a finite set of terminological axioms.   or an atomic concept called defined concept , and a  possibly complex  concept   , a terminological axiom is of the form . An atomic concept not appearing on the left-hand side of any terminological axiom is called a primitive concept. Acyclic simple T  oxes only are considered  a defined concept may appear at most once as the left-hand side of an axiom, and no terminological cycles are allowed, i.e., no defined concept may occur   neither directly nor indirectly within its own definition  Nebel, As an example, consider the unary relation  i.e., a concept  denoting the class of happy fathers, defined using the atomic predicates Man, Doctor, Rich, Famous concepts and CHILD, FRIEND roles HappyFather    Man Π   ΞCHILD.

i.e., the men whose children are doctors having some rich or famous friend.

 An ABox is a finite set of assertional axioms, i.e. predications on individual ob ects.    et be the alphabet of symbols denoting individuals an assertion is an axiom of the form or         , where   and   denote individuals in interpretation I i is satisfied
, and by I i