Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

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

Authors: Boudet, A. Contejean, E. Devie, H.

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 = 	 {Boudet, A. and Contejean, E. and Devie, H.},
    title = 	 {A new AC unification algorithm with an algorithm for solving systems of diophantine equations },
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {289--299},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }