A new AC-unification algorithm with a new algorithm for solving diophantine equations

Abstract: This paper presents a new AC-unification algorithm. A new combination technique for regular collapse-free theories is provided along the line developped in [1].

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 our 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, compared to [2].

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.

References

[1]

A. Boudet, J.-P. Jouannaud, and M. Schmidt-Schauß. Unification in Boolean rings and Abelian groups. Journal of Symbolic Computation, 8:449–477, 1989.

[2]

F. Fages. Associative-commutative unification. Journal of Symbolic Computation, 3(3), June 1987.

This document was translated from L^AT_EX by H^EV^EA.