← All problems
Unverified
For which equational theories is ground reducibility of extended rewriting decidable?
The source page states the original problem together with its recorded qualifications and progress updates as follows.
Ground reducibility of extended rewrite systems, modulo congruence, like
associativity and commutativity (AC), is undecidable [Kapur, 1991]. For
left-linear AC systems, on the other hand, it is decidable [Kapur, 1991].
What can be said more generally about restrictions on extended rewriting that
give decidability? This problem is related to RTALooP entry ac.
Recorded progress.
Progress has been made in [Kapur, 1991], where it is proven that ground reducibility remains undecidable when a single non-constant function symbol is associative.
