Properties of substitutions and unifications

In this paper the set of first order substitutions with a partial ordering “more general than” is investigated. It is proved that the set of equivalence classes of idempotent substitutions together with an added greatest element is a complete lattice. A simultaneous unification of finitely many finite sets of terms can be reduced to unifying each of the sets of terms separately and to building the supremum of the most general unifiers in this lattice afterwards. This saves time in an automatic proof procedure when combined with the concept of weak unification also introduced in this paper