Problem #12 (Solved !)
Originator: Wayne Snyder
Date: April 1991
Summary:
What is the complexity of the decision problem for the confluence
of ground term-rewriting systems?
What is the complexity of the decision problem for the confluence of ground
(i.e., variable-free) term-rewriting systems? Decidability was shown in
[DHLT90][Oya87]; see also [DT90].
Remark
The problem is PTIME-complete, as has been shown independently by
[CGN01] and [Tiw02].
References
-
[CGN01]
-
Hubert Comon, Guillem Godoy, and Robert Nieuwenhuis.
The confluence of ground term rewrite systems is decidable in
polynomial time.
In Proceedings of the 42nd Annual IEEE Symposium on Foundations
of Computer Science (FOCS), pages 298–307, Las Vegas, Nevada, USA, 2001.
- [DHLT90]
-
Max Dauchet, Thierry Heuillard, Pierre Lescanne, and Sophie Tison.
Decidability of the confluence of finite ground term rewriting
systems and of other related term rewriting systems.
Information and Computation, 88(2):187–201, October 1990.
- [DT90]
-
Max Dauchet and Sophie Tison.
The theory of ground rewrite systems is decidable.
In John C. Mitchell, editor, Fifth
Symposium on Logic in
Computer Science, pages 242–248, Philadelphia, PA, June 1990.
IEEE.
- [Oya87]
-
Michio Oyamaguchi.
The Church-Rosser property for ground term rewriting systems is
decidable.
Theoretical Computer
Science, 49(1):43–79, 1987.
- [Tiw02]
-
Ashish Tiwari.
Deciding confluence of certain term rewriting systems in polynomial
time.
In Gordon Plotkin, editor, IEEE Symposium on Logic in Computer
Science, LICS 2002, pages 447–456, Copenhagen, Denmark, July 2002.
IEEE.