English Dictionary

5.7.T ( Unification theorem ) For any two terms or formulas

without quantifiers X and Y, the following holds.

(i) The unification algorithm UNIF₁, applied to X, Y,

terminates after a finite number of steps.

(ii) {X, Y} is unifiable iff UNIF₁ so indicates upon ter-

mination. Moreover, the substitution σ then available as out-

5.7.T ( Unification theorem ) For any two terms or formulas without quantifiers X and Y, the following holds. (i) The unification algorithm UNIF₁, applied to X, Y, terminates after a finite number of steps. (ii) {X, Y} is unifiable iff UNIF₁ so indicates upon ter- mination. Moreover, the substitution σ then available as out- put is a most general unifier of {X, Y}.