Furthermore, both prove the independence property. If a theory T satisfies the independence property, then an algorithm for testing entailment and disentailment in T can be used for deciding the existential fragment of T . Since we can decide the full theories of FT and CFT , it is clear that both the entailment and disentailment test can be performed using our simplification algorithms for these theories. On the other hand, these algorithm apply only to a very limited fragment. Their signatures didn't contain the constant symbols and the predicate symbol , but used sort symbols instead.
Sorts are unary predicate symbols which are interpreted as disjoint sets.
Both also considered feature trees, which were defined slightly differently because of the different signature. The denotation of a sort symbol A in the feature tree interpretation is exactly the set of all feature trees having the root labelled with A . Their results can easily be adapted for our signature. We changed the signature in order to gain a bit more expressivity. However, Maher's proof depends heavily on the structure of first-order terms, since it uses substitutions.