Unification of sets and multisets

Abstract

The observation that unification under associativity and commutativity reduces to the solution of certain linear diophantine equations is the basis for a complete and minimal unification algorithm. It is also shown that completeness and minimality is closely related to the notion of a basis for the linear solution space of these equations . Terms under associativity (A) and commutativity (C) closely resemble the datastructure multi sets (sets which may contain multiple occurrences of the same element) , which is used in the matching of patterns (pattern directed invocation) in many Al-languages. The problem was first investigated in [ 40], this paper presents an alternative solution, which is an improvement over [ 40]. Unification under associativity, commutativity and idempotence is shown to behave in an exactly parallel manner to unification under {A, C} with the proviso that the arithmetic equations are replaced by Boolean equations. Terms under associativity, commutativity and idempotence closely resemble the datastructure set, which is also used in the matching of patterns in many Al-languages. The combination of these axioms occur in automatic theorem proving, e.g. set theoretic Intersection and union have these properties.