Simplified Proof of Kruskal’s Tree Theorem

D. Singh, Ali Mainguwa Shuaibu, Ndayawo, M.S.

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


Full Text: PDF
Download the IISTE publication guideline!

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