DocumentCode
2717185
Title
A constructive proof of Higman´s lemma
Author
Murthy, Chetan R. ; Russell, James R.
Author_Institution
Dept. of Comput. Sci., Cornell Univ., Ithaca, NY, USA
fYear
1990
fDate
4-7 Jun 1990
Firstpage
257
Lastpage
267
Abstract
G. Higman´s lemma (1952) is a special case of the more general Kruskal´s tree embedding theorem and the graph minor theorem. A direct constructive proof of the lemma with manifest computational content is presented. This is done by reducing the problem to a construction of certain sets of sequential regular expressions. A well-founded order on such sets is exhibited, and the lemma then follows by induction
Keywords
theorem proving; trees (mathematics); Higman´s lemma; constructive proof; direct constructive proof; graph minor theorem; induction; sequential regular expressions; tree embedding theorem; well-founded order; Arithmetic; Computer science; Concrete; History; Logic; Polynomials; Tree graphs;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e
Conference_Location
Philadelphia, PA
Print_ISBN
0-8186-2073-0
Type
conf
DOI
10.1109/LICS.1990.113752
Filename
113752
Link To Document