Unification in datastructure multisets

In a recent paper A. Herold and J. Siekmann generalize pure AC unification to terms containing additional function symbols. 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 the sequential mode.