← 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.

Coming soon

Organizer

Boyuan Wang portraitBoyuan Wang
Minghan Wang portraitMinghan Wang
Bochao Li portraitBochao Li
Hongwei Hu portraitHongwei Hu