← 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 EE, completion strategy, and reduction ordering. Must there be a finite depth NN for EE such that for any n>Nn > N restricting the generation of critical pairs to overlaps at positions that are no deeper than nn in the overlapped left-hand side (but otherwise not changing the strategy) also produces a non-terminating completion sequence?

Coming soon

Organizer

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