ince, by assumption, the temporal constraint networks are minimal, the temporal relation cannot be further restricted. 0, for ea variable mapping and ea temporal interpretation t we can build an assignment V* such that V*
while
. Now, we can extend the assignment V* in such a way that V*
while V* / M T M T T This contradicts the assumption that V*
=M
Definition 6.16 (S-mapping) An s-mapping from a conceptual temporal constraint netto a conceptual temporal constraint network work O
D
is a 一 →    such that the non-temporal concept labeling each node variable mapping in     subsumes the non-temporal concept labeling the corresponding node in
, and コs The algorithm for checking subsumption between temporal concept expressions reduces the subsumer and the subsumee in essential graph form, then it looks for an s-mapping between the essential graphs by exhaustive search. To prove the completeness of the overall s subsumption procedure it will be showed that the introduction of LCS s preserves the subsumption. A model-theoretic characterization of the LCS will be given for showing this property. et s start to build an erbrand model for an F concept. et '
denote the first order formula corresponding to a concept see proposition . . . while the functionality of features can be expressed with a set of formul F. y syntax induction it easy to show that ' is an existentially uantified formula with one free variable. oreover, the matrices of such formula is a con unction of positive predicates.  F
-
is logically e uivalent to F      "       where the functionality axioms allow to map every subformula into 3! . f        Then  "    is such that all the existential  uantifiers in A,
which come from the first order conversion of features  are replaced by :!   uantifiers.

Now, F
lll where is a constant substituting the free variable and iii is obtained by skolemizing the ::! uantified variables is a set of definite orn clauses.

Definition 6.17 (Herbrand model) Let   be an F concept expression. Then we define its inimal erbrand odel c as the inimal erbrand odel of the above mentioned ss III
Lemma 6.18 ( F concept subsumption) Let      be F concept expressions, and D
their minimal Herbrand models obtained by skolemizing the first order set F
Th en, C
l
, i F
where " and Proof i F
are obtained by applying the functionality axioms to the set ie., unifying the variables in the functional predicates and then replacing all the existential uantifiers by f!  uantifiers.  Now,       and 3! uantified variables in the following way let "
m n and let
"
m m k the formula m m indicate its skolemized form. Then, let
. Now, and since every existential   uantification in   "
l was of type ∇ヨ! then the thesis is true