Unification in commutative idempotent monoids

AbstractEmbedding sets as a datastructure into resolution-based deduction requires a unification algorithm respecting associativity, commutativity and idempotence of the constructor function union. We shall present such an algorithm and prove its correctness and termination. Although this algorithm is very simple, the enormous proliferation of unifiers restricts its value to theoretical considerations. For practical purposes, the more special, unitary theory of boolean expressions seem to be better suited