xg o...oxg of op : C
↑
*g o...o*g of op ↓g og
↑
*g o...o*g ↓*f o...o*f
↑
*g o . . . o *g o g o p ↓ *f o . . . o *f o f o g 
↑
xg o...o*g ↑*f o...o*f
↑
xg t
↑
*g o...o*g : *g + †
*g o...o*g of op tg og
*g o . . . o *g o g o p ↑ *f o . . . o *f o f o g 
↑
*g o...oxg : .

*g o...o*g : .

*g o...o*g ↓*f o...o*f .

*g o...oxg :  n
*f o... o*f : .

*g o...o*g ↑*f o...o*f .

xg t .

-   *g  o...o*g  :  *g  +  ↑  .

- 
*g o...o*g :  n
*f o... o*f : .

igure 2. For each  j j , on compute its time invariant part (let us indicate this particular concept expression as   j). This gives   j by computing for each disjunct  j  in  j  its time-invariant information  j   If  j    ALCF   , then
. Otherwise, rewrite every conjunct in  j  as showed in Figure 15, while the conjuncts not considered there are rewrote to    Now, unless there is an j must be conjunctively added to all the other nodes.

s i s Proposition 7.7 (Equivalence of CEF) Every concept in existential form can be reduced into an equivalent completed existential concept.

As for the TL-F case, both covering and parameter introduction can be computed independently. As a conse uence of the above normalization phase, the proposition .

node independence is now true for TL-ALCF concepts in E . bserve that, to obtain a E
concept, the steps of the normalization procedure re  uire the computation of the transitive closure of the temporal relations   which is an N -complete problem  van   eek and the computation of ALCF subsumption   which is a      A  E-complete hen, problem   ollunder   Nutt, efore the presentation of the last normalization phase, which will eliminate redundant nodes, it is now possible to check whether a concept expression is satisfiable. Proposition 7.8 (Concept satisfiability) ATL-ALCF concept in CEF, T
is satisfiable (with the proviso that the temporal constraints are satisfiable) if and only if the n-temporal concepts labeling each node in - are satisfiable. Checking satisfiability of a TL-ALCF concept in CEF is a PSPACE-complete problem.

Proof. Is a direct conse uence of the node independence established by proposition . .

which is true also for TL-ALCF concepts in E
The normalization procedure now goes on by rewriting unsatisfiable concepts to and then computing the essential graph form for satisfiable concepts. This last phase is more