[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #46

Originator: Deepak Kapur
Date: December 1991

Summary: For which equational theories is ground reducibility of extended rewriting decidable?

Ground reducibility of extended rewrite systems, modulo congruence, like associativity and commutativity (AC), is undecidable [KNZ87]. For left-linear AC systems, on the other hand, it is decidable [JK89]. What can be said more generally about restrictions on extended rewriting that give decidability? This problem is related to Problem #25.

Remark

Progress has been made in [KR94], where it is proven that ground reducibility remains undecidable when a single non-constant function symbol is associative.

References

[JK89]

Jean-Pierre Jouannaud and Emmanuel Kounalis. Automatic proofs by induction in equational theories without constructors. Information and Computation, 81(1):1–33, 1989.

[KNZ87]

Deepak Kapur, Paliath Narendran, and Hantao Zhang. On sufficient completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395–415, August 1987.

[KR94]

Gregory Kucherov and Michaël Rusinowitch. On the ground reducibility problem for word rewriting systems with variables. Information Processing Letters, 1994. To appear. Earlier version appeared in the Proceedings of 1994 ACM/SIGAPP Symposium on Applied Computing, Phoenix, AZ.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]