Unification; Computable Set Theory

A unification algorithm is said to be minimal for a unication problem if it generates exactly a (minimal) complete set of most-general unifiers, without instances, and without repetitions. The aim of this paper is to present a combinatorial …