A new AC unification algorithm with an algorithm for solving systems of diophantine equations

A novel AC-unification algorithm is presented. A combination technique for regular collapse-free theories is provided along the line developed by A. Boudet et al. (1989). The number of calls to the diophantine equations solver is bounded by the number of AC symbols times the number of shared variables. The rest of the algorithm being linear, this gives a much better idea of how the complexity of AC unification is related to the complexity of solving linear diophantine equations. The termination proof is surprisingly easy. Finally, systems of constraint linear diophantine equations can be solved, rather than one equation at a time, using an algorithm which extends Fortenbacher´s algorithm to an arbitrary dimension. This allows a much more efficient use of the constraints than in the standard case