Properties of substitutions and unifications
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.
semigroup of substitutions in first-order logic
scientific article; zbMATH DE number 3947653
scientific article