Simplified Proof of Kruskal’s Tree Theorem
Abstract
There are different versions of proof of Kruskal’s tree theorem. In this paper, we provide a simplified version of proof of Kruskal’s tree theorem. The proof is essentially due to Nash-williams. Though, our proof is similar to the Kruskal’s original proof formulated in terms of well-quasi-orders by Gallier. In our case, we use well-partial-orders and follow the simplified proof of Kruskal’s theorem of Gallier. Kruskal’s tree theorem is the main ingredient to prove well-foundedness of simplification orders for first-order rewriting. It implies that if an order satisfies some simplification property, well-foundedness is obtained for free. This theorem plays a crucial role in computer science, specially, termination of term rewriting systems.
Keywords: Kruskal’s Theorem, Simplification order, Term rewriting, well-foundedness
To list your conference here. Please contact the administrator of this platform.
Paper submission email: MTM@iiste.org
ISSN (Paper)2224-5804 ISSN (Online)2225-0522
Please add our address "contact@iiste.org" into your email contact list.
This journal follows ISO 9001 management standard and licensed under a Creative Commons Attribution 3.0 License.
Copyright © www.iiste.org