Paper: A new AC unification algorithm with an algorithm for solving systems of diophantine equations (at LICS 1990)

Authors: Alexandre Boudet Evelyne Contejean Hervé Devie

Abstract

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

BibTeX

  @InProceedings{BoudetContejeanDevi-AnewACunificational,
    author = 	 {Alexandre Boudet and Evelyne Contejean and Hervé Devie},
    title = 	 {A new AC unification algorithm with an algorithm for solving systems of diophantine equations },
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {289--299},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }