[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Albert Meyer
Date: April 1991
Summary: 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?
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, [Squ87]); 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) [DMT85], or with a two-phased version of rewriting, wherein normal forms of the first system are inputs to the second [Bau85].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |