Minimal Set Unification

A unification algorithm is said to be minimal for a unification problem if it generates exactly a complete set of minimal unifiers, without instances, without repetitions. Aim of this paper is to describe a new set unification algorithm minimal for a significant collection of sample problems that can be used as benchmarks for testing any set unification algorithm. To this end, a deep combinatorial study for such problems has been realized. Moreover, an existing naive set unification algorithm has been also tested in order to show its bad behavior for most of the sample problems.