Competing for theAC-Unification Race

We describe our implementation of the unification algorithm for terms involving some associative-commutative operators plus free function symbols described by Boudetet al. The first goal of this implementation is efficiency, more precisely competing for theAC Unification Race. Although our implementation has been designed for good performance when applied to non-elementaryAC-unification problems, it is also very efficient on elementary problems. Our implementation, written in C and running on Sun workstations, is to be compared with the implementations in LISP, on Symbolics LIPS machines.