[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #100

Originator: Nachum Dershowitz
Date: October 16, 2002

Summary: Design new termination methods based on the gap-embedding theorems of Friedman and Kriz.

Harvey Friedman [Sim85] modified Kruskal’s Tree Theorem to restrict labels that appear along the path between the images of adjacent nodes to what is called gap embedding. Whereas Friedman’s result applied only to labellings with the natural numbers, Igor Kříž [K89] extended it to arbitrary ordinal labellings. See also [Gor90]. The question is whether new and useful termination methods can be based on these gap-embedding theorems. One step in this directions is [Oga95].

This problem is related to Problem #73.

References

[Gor90]

L. Gordeev. Generalizations of the Kruskal-Friedman theorems. Journal of Symbolic Logic, 55(1):157–181, 1990.

[K89]

I. Kříž. Well-quasiordering finite trees with gap-condition. proof of Harvey Friedman’s conjecture. Ann. of Math., 130:215–226, 1989.

[Oga95]

M. Ogawa. Simple gap termination on term graph rewriting systems. In Theory of Rewriting Systems and Its Application, pages 99–108, 1995. Research report 918, RIMS, Kyoto Univ, Kyoto., also available at http://www.brl.ntt.co.jp/people/mizuhito.

[Sim85]

S.G. Simpson. Nonprovability of certain combinatorial properties of finite trees. In L. A. Harrington, editor, Harvey Friedman’s research on the Foundation of Mathematics, pages 87–117. Elsevier Science, 1985.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]