[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?

References

[BCD90]

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.

[Fag87]

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]