Unification in the Datastructure Multisets

Abstract

In a forthcoming paper A. Herold and J. Siekmann generalize "pure" AC-unification ([ST 75], [LS 76]) to terms containing additional function symbols (see also [ST 81], [FA 84]). Generalized AC-unification thus attains practical relevance for a broad range of applications. Pure AC-unification is used as a basic mechanism and it is this key role that has motivated our research. We have improved upon earlier approaches by basing (pure) AC-unification on a firm theoretical basis and presenting algorithms which fully exploit the properties of the underlying mathematical structure. In particular, the high degree of parallelism for AC-unification will become apparent. Our algorithms have been designed for parallel hardware but still yield significant improvements over earlier algorithms when used in sequential mode.