← All problems
Unverified

Is there a decidable uniform word problem for which there is no variant on the rewriting theme that can decide it---without adding new symbols?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Is there a decidable uniform word problem for which there is no variant on the rewriting theme (for example, rewriting modulo a congruence with a decidable matching problem, or ordered rewriting) that can decide it---without adding new symbols to the vocabulary? There are decidable theories that cannot be decided with ordinary rewriting (see, for example, [Meyer, 1991]); on the other hand, any theory with decidable word problem can be solved by ordered-rewriting with some ordered system for some conservative extension of the theory (that is, with new symbols) [Meyer, 1991], or with a two-phased version of rewriting, wherein normal forms of the first system are inputs to the second [Meyer, 1991].

Coming soon

Organizer

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