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


Problem #33 (Solved !)

Originator: Jean-Pierre Jouannaud
Date: April 1991

Summary: How can completion modulo ACUI be made effective?

Completion modulo associativity and commutativity (AC) [PS81] is probably the most important case of extended completion; the general case of finite congruence classes is treated in [JK86]. Adding an axiom (U) for an identity element (x+0=x) gives rise to infinite classes. This case was viewed as conditional completion in [BPW89], and solved completely in [JM90]. The techniques, however, do not carry over to completion with idempotence (I) added (x+x=x). How to handle ACUI-completion effectively is open.

Remark

Normalized Rewriting as introduced by Claude Marché in [Mar96] is the right way of handling axiom systems like ACUI.

References

[BPW89]
Timothy Baird, Gerald Peterson, and Ralph Wilkerson. Complete sets of reductions modulo Associativity, Commutativity and Identity. In Nachum Dershowitz, editor, Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 29–44, Chapel Hill, NC, USA, April 1989. Springer-Verlag.
[JK86]
Jean-Pierre Jouannaud and Hélène Kirchner. Completion of a set of rules modulo a set of equations. SIAM Journal on Computing, 15:1155–1194, November 1986.
[JM90]
Jean-Pierre Jouannaud and Claude Marché. Completion modulo associativity, commutativity and identity. In Alfonso Miola, editor, Proceedings of the International Symposium on the Design and Implementation of Symbolic Computation Systems (Capri, Italy), volume 429 of Lecture Notes in Computer Science, pages 111–120, Berlin, April 1990. Springer-Verlag.
[Mar96]
Claude Marché. Normalized rewriting: an alternative to rewriting modulo a set of equations. Journal of Symbolic Computation, 21(3):253–288, March 1996.
[PS81]
Gerald E. Peterson and Mark E. Stickel. Complete sets of reductions for some equational theories. J. of the Association for Computing Machinery, 28(2):233–264, April 1981.

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