Subsumption lattice

A subsumption lattice is a mathematical structure used in the theoretical background of automated theorem proving and other symbolic computation applications.

The join and the meet operation in this lattice are called anti-unification and unification, respectively.

1); its appearance prevents the subsumption lattice from being modular and hence also from being distributive.

Join and meet of two proper[3] linear terms, i.e. their anti-unification and unification, corresponds to intersection and union of their path sets, respectively.

Apparently, the subsumption lattice was first investigated by Gordon D. Plotkin, in 1970.

Pic. 1: Non-modular sublattice N 5 in subsumption lattice
Pic. 2: Part of the subsumption lattice showing that the terms f ( a , x ), f ( x , x ), and f ( x , c ) are pairwise unifiable, but not simultaneously. ( f omitted for brevity.)
Pic. 5: Distributive sublattice of linear terms
Pic. 4: M 3 built from linear terms
Pic. 3: N 5 built from linear terms