Formal and Informal Proofs

It is a great pleasure to take part in this tribute to Woody Bledsoe in celebration of his seventieth birthday. In his 1985 Presidential Address to the American Association for Artificial Intelligence [

2

], Bledsoe describes the vision which came to him in a dream a quarter of a century earlier, in 1960, a vision in which he saw the future wonders which AI could make happen. I for one am very glad that he reacted so boldly and courageously to that dream by deciding

then and there to quit my job and set about spending the rest of my life helping bring this dream to reality … to make machines act in some fundamental ways like people.