Properties of substitutions and unifications (Q1074342)

Basic properties of the semigroup of substitutions in first-order logic are proved. The idempotent substitutions are shown to form a complete lattice modulo renaming of variables. Most general unifiers are characterized as suprema of appropriate sets of substitutions. Also weak unifiers are considered, including a criterion for the existence of most general weak unifiers.