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.