[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Miki Hermann
Date: December 1991
Summary: Can completion always be made terminating when limiting the depth of occurrences of critical pairs?
Suppose ordinary completion (as in [DJ90], for example, is non-terminating for some initial set of equations E, completion strategy, and reduction ordering. Must there be a finite depth N for E such that for any n > N restricting the generation of critical pairs to overlaps at positions that are no deeper than n in the overlapped left-hand side (but otherwise not changing the strategy) also produces a non-terminating completion sequence?
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |