|
|
|
A theorem which plays a fundamental role in computer science because it is one of the main tools for showing that certain orderings on Trees are well-founded. These orderings play a crucial role in proving the termination of rewriting rules and the correctness of the Knuth-Bendix equational completion procedures.
See also Kruskal's Algorithm, Natural Independence Phenomenon, Tree
References
Gallier, J. ``What's so Special about Kruskal's Theorem and the Ordinal Gamma[0]?
A Survey of Some Results in Proof Theory.'' Ann. Pure and Appl. Logic 53, 199-260, 1991.