← All problems
Unverified
Can completion always be made terminating when limiting the depth of occurrences of critical pairs?
The source page states the original problem together with its recorded qualifications and progress updates as follows.
Suppose ordinary completion (as in [Hermann, 1991], for example, is non-terminating for some initial set of equations , completion strategy, and reduction ordering. Must there be a finite depth for such that for any restricting the generation of critical pairs to overlaps at positions that are no deeper than in the overlapped left-hand side (but otherwise not changing the strategy) also produces a non-terminating completion sequence?
