AC-unification race: The system solving approach, implementation and benchmarks

AbstractWe present an Associative-Commutative unification algorithm and its implementation in the C language. The main point is that both the specification and the program are based on solving systems of equations. Benchmarks are proposed for evaluating the performance of the implementation of this algorithm. They demonstrate improvements not only in time and space but also in size of the complete set of unifiers generated