Woody Bledsoe

Bledsoe

Woody Bledsoe (November 12, 1921 – October 4, 1995) was an American mathematician, computer scientist, and prominent educator. He is one of the founders of artificial intelligence (AI), making early contributions in pattern recognition,facial recognition, and automated theorem proving. He continued to make significant contributions to AI throughout his long career. One of his influences was Frank Rosenblatt.

Quotes

• Incidentally my goal wasn't to necessarily press forth AI. It was out of these asides, but AI was used to prove theorems early on. Jerome Simon had one of the first provers that I considered a good AI. Imply was supposed to do the same kind of thing. It was suppose to be an interactive prover and a stand-alone prover at the same time.
  • Could you tell me something about the way the system worked and how it related to the state of AR at the time?

• It was built to partly prove theorems, which is one of the jobs that AI does. [inaudible word] emission, theorem proving, and so forth.
  • When you say it wasn't built to further AI, what do you mean?

• Partly, but partly to see how far we could go with automating the proof of mathematical theorems. That was the intent.
  • What theorems did you want to prove? You used it, you built it, as a tool to further your mathematical research? Is that right?

• Yes, that's fair enough. It's not really what I said, though. I mean my goals were independent of the name. I wouldn't call them mathematics either.
  • In that sense [it wasn't built to further AI, but to explore the boundaries of automatic reasoning?]
• We proved — in the stand-alone mode with heuristics — we proved limit theorems of calculus and that's a good sample
  • What theorems did you prove with Imply?
• No, other AI people who weren't working on theorem provers in particular. I don't know if I can give a lot of references off the top of my head, but that was the state of the art for awhile. It used heuristics and that turned out to be later not as popular amongst the formal automated theorem proving crowd to use heuristics. They wanted to find out what you could do to stand alone heuristics.
  • When you say "they," who do you mean "they"? You mean other researchers in the community?

• Heuristics are ad hoc. They tend [correct word?], you fix up the heuristics for limit theorems. Now when you go to algebra you need some new heuristics. And when you go to functional analysis and you need some new ones. When are you going to stop? This is what we want as a general purpose prover here. It will prove anything. You're in a dilemma. I mean if you get a general purpose prover oftentimes they're too weak.
  • Why was that?

• You get a very special purpose prover that uses heuristics, then they stop at the boundary where they can't work anymore.
  • Why was that?
• I don't think it's too hard in any particular area, although I think people are a little surprised how easy it was in limit theorems. I don't think the average person would do it.
  • Is it difficult to come up with the heuristics to guide the prover?