info prev up next book cdrom email home

Kruskal's Tree Theorem

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


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.

© 1996-9 Eric W. Weisstein