[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |