Let's now look again at the abstract tree AT1: This abstract tree is valid relative to G1 (it corresponds to a possible complete derivation) but it is not necessarily valid relative to the combination <G1,KB1>; this notion is defined in the following way: because the abstract tree uniquely determines the set of rules which have been used for building the derivation, it also uniquely determines a set of associated KB constraints; thus AT1 is associated with the set of constraints: fdf(diprox,tablet), da(diprox,swallow)g. Now we say that AT1 is valid relative to the combination <G1,KB1> if and only if it is both valid relative to G1 and if its associated set of constraints is compatible with KB1.
we need to show that the addition of the two constraints df(diprox,tablet), da (diprox,swallow) to the ABOX still leads to a satisfiable knowledge base.