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
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;
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
DOI :
10.1109/LICS.1990.113752
