[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #40

Originator: Participants at Unif Val d’Ajol
Date: April 1991

Summary: Does AC unification terminate under more flexible control?

Fages [Fag87] proved that associative-commutative unification terminates when “variable replacement” is made after each step. Boudet, et al. [BCD90] have proven that it terminates when variable replacement is postponed to the end. Does the same (or similar) set of transformation rules terminate with more flexible control?


Alexandre Boudet, Evelyne Contejean, and Hervé Devie. A new AC unification algorithm with an algorithm for solving diophantine equations. In John C. Mitchell, editor, Fifth Symposium on Logic in Computer Science, pages 289–299, Philadelphia, PA, June 1990. IEEE.
François Fages. Associative-commutative unification. Journal of Symbolic Computation, 3(3):257–275, June 1987. Previous version in the Proceedings of the Seventh International Conference on Automated Deduction, Napa, CA, pp. 194-208 [May 1984].

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]