Logic in Computer Science (LICS 1990)

Paper: A constructive proof of Higman's lemma (at LICS 1990)

Authors: Murthy, C.R. Russell, J.R.

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

BibTeX

  @InProceedings{MurthyRussell-Aconstructiveproofo,
    author = 	 {Murthy, C.R. and Russell, J.R.},
    title = 	 {A constructive proof of Higman's lemma},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {257--267},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }