Oral-History:Woodrow Wilson Bledsoe
About Woodrow Wilson Bledsoe
Woodrow Wilson Bledsoe played a key role in keeping automated theorem proving alive as a field during the 1970s. Born in Oklahoma in 1921, Bledsoe served as a captain in the US Army Corps of Engineers before taking his Ph.D. in mathematics from the University of California. By the late 1950s, he was the manager of the Systems Analysis Department of the Sandia nuclear weapons laboratory in Albuquerque, New Mexico. However, he developed an interest in artificial intelligence that caused him to leave Sandia in 1960 to help found one of the earliest commercial firms in artificial intelligence, Panoramic Research Inc. In 1966, Bledsoe became professor of mathematics at the University of Texas at Austin and played a major role in the development of computer science and artificial intelligence there.
In the interview, Bledsoe discusses the development of his various theorem provers, including Imply, Setvar, Str+ve and Analogy. He discusses the difference between resolution and non-resolution theorem proving, the advantages and disadvantages of heuristic techniques, the use of AI theories in Analogy, the limitations of Prologue-style compilation, and the importance of NSF funding to his work.
About the Interview
Woodrow Wilson Bledsoe: An Interview Conducted by Andrew Goldstein, IEEE History Center, October 21, 1991
Interview #134 for the IEEE History Center, The Institute of Electrical and Electronics Engineers, Inc.
Copyright Statement
This manuscript is being made available for research purposes only. All literary rights in the manuscript, including the right to publish, are reserved to the IEEE History Center. No part of the manuscript may be quoted for publication without the written permission of the Director of IEEE History Center.
Request for permission to quote for publication should be addressed to the IEEE History Center Oral History Program, IEEE History Center, 445 Hoes Lane, Piscataway, NJ 08854 USA or ieee-history@ieee.org. It should include identification of the specific passages to be quoted, anticipated use of the passages, and identification of the user.
It is recommended that this oral history be cited as follows:
Woodrow Wilson Bledsoe, an oral history conducted in 1991 by Andrew Goldstein, IEEE History Center, Piscataway, NJ, USA.
Interview
INTERVIEW: Woodrow W. Bledsoe
INTERVIEWER: Andy Goldstein
DATE: 21 October 1991
PLACE: Telephone interview
Shift to Automatic Reasoning
Goldstein:
You write in your cover letter that we are seeing a shift in interest in artificial intelligence to automatic reasoning, and I want to talk about that general trend. Can you talk about that some?
Bledsoe:
I think the whole trend is worth talking about for a minute. It may not be others' opinion, but I believe it is a trend. I didn't press it because even I didn't believe in it at the beginning. From the mathematical end of this business, I didn't really think that kind of formality would be as dominant as it has become or as important. And so it's a trend, it seems to me.
Goldstein:
What prompted the trend?
Bledsoe:
When you first start a science you have to be somewhat ad hoc in order to get anything out. Once you begin to get results, you find that this is part of a formal reasoning process, and in order to get very far with you've got to engineer it up a little bit for consistency. It seemed to me then that you were forever proving little theorems inside of some program. Therefore you tended to get formal about that.
Theorem Provers
Goldstein:
I want to talk about your work. I have an early proposal of yours where you write about a system called prover. Can you tell me the story of that?
Bledsoe:
Unfortunately I've had two or three provers. Can you tell me the title or something?
Goldstein:
There is no reason we don't cover all of them. I know that you were working with the STR + VE. Was that one of them?
Bledsoe:
Yes. I just called that Str+ve.
Goldstein:
Right. I wasn't sure it if was supposed to be "Strive." I thought I was looking at a misprint.
Bledsoe:
We put a plus instead of an "i" in. Before that I had a prover we called Imply, I-m-p-l-y. That is what I normally called the natural education type prover.
Goldstein:
Was that the beginning of your work?
Bledsoe:
I was doing [inaudible word] back in the beginning. This is talking and automates theorem proving. I think Imply is one of just two or three main provers, and I don't think you want to talk much about the others, or maybe not even this. But Imply is the first one, Str+ve is the second, and Setver is the third.
Imply
Goldstein:
When did you produce Imply?
Bledsoe:
I started in about 1970 and didn't get published until '73.
Goldstein:
1970. Was that done with NSF support, or some other means?
Bledsoe:
That really started about '73 with NSF.
Goldstein:
So Imply was done and supported by someone else.
Bledsoe:
In the beginning, yes, but you don't [inaudible word] whose [inaudible word] when you work, right? In '73 the first paper about it came out, that's when it really got in the business. Before that is was just the early versions.
Goldstein:
Could you tell me something about the way the system worked and how it related to the state of AR at the time?
Bledsoe:
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.
Goldstein:
When you say it wasn't built to further AI, what do you mean?
Bledsoe:
It was built to partly prove theorems, which is one of the jobs that AI does. [inaudible word] emission, theorem proving, and so forth.
Goldstein:
What theorems did you want to prove? You used it, you built it, as a tool to further your mathematical research? Is that right?
Bledsoe:
Partly, but partly to see how far we could go with automating the proof of mathematical theorems. That was the intent.
Goldstein:
In that sense [it] wasn't built to further AI, but to explore the boundaries of automatic reasoning?
Bledsoe:
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.
Goldstein:
What theorems did you prove with Imply?
Bledsoe:
We proved — in the stand-alone mode with heuristics — we proved limit theorems of calculus and that's a good sample.
Goldstein:
Yes. Now, when you say the stand-alone mode you mean it would function independently? You wouldn't prompt it or guide it?
Bledsoe:
Right.
Use of Heuristics
Goldstein:
But, and you also say it worked by heuristics. Can you describe that?
Bledsoe:
We had what was called a limit heuristic. When it saw what it thought was a limit theorem it would use that heuristic and often it got the proof.
Goldstein:
Now did that represent the cutting edge of automatic reasoning at the time? I wonder if you could describe the development of that sub-field of artificial intelligence in 1970.
Bledsoe:
There wasn't anyone that had a prover that could do that then, and incidentally I didn't say they immediately took that up and said, we'll work on the basis of that. I'd love to say that, but it was widely thought to be a power prover like that.
Goldstein:
When you say "they," who do you mean "they"? You mean other researchers in the community?
Bledsoe:
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.
Goldstein:
Why was that?
Bledsoe:
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.
Goldstein:
Right.
Bledsoe:
You get a very special purpose prover that uses heuristics, then they stop at the boundary where they can't work anymore.
Goldstein:
Is it difficult to come up with the heuristics to guide the prover?
Bledsoe:
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.
Goldstein:
When you say the other researchers were cautious about the heuristic systems, who are those people?
Bledsoe:
Let's see, Jay Robinson. By the way he didn't verbally say that, and he and I are dear friends, and he took [inaudible word] for resolution.
Goldstein:
Was it implicit in their research?
Bledsoe:
Absolutely. That was the way the research was going. There was no bashing. In fact they were pretty friendly interactions. But that's the way it went, they didn't go much for special heuristics in special areas.
Goldstein:
Yes. Could you repeat the name please?
Bledsoe:
Jay Allen Robinson.
Resolution and Non-resolution Techniques
Goldstein:
You say he introduced resolution, which you also mention in some of the materials you sent. I don't know what that means.
Bledsoe:
Well then, without talking about resolution, you really aren't being fair to automated theorem proving. I didn't mean you personally, but in a report it wouldn't be. We might talk about that.
Goldstein:
Yes.
Bledsoe:
Another very major researcher in this area is Larry Wass . His work tended to be a little more heuristic, but mainly general purpose. He has a bunch of people after him, and I don't think you necessarily want to get into all of them, but if you do, there are other names.
Goldstein:
Let's talk about resolution and how it's distinguished from heuristic.
Bledsoe:
Yes. Now, you understand that were two streams that were coming together here. There was the stream of AI and there was the stream of automated reasoning. One area of automated reasoning didn't even think it had anything to do with AI, because it didn't use any of the concepts of knowledge and heuristics and stuff. But I was in the middle. And yes, resolutions are a general purpose theorem proving system that packs any term and first order logic.
Goldstein:
I spoke with Virgil Marfiel for a while, and he discussed some of his work, so I've looked at it.
Bledsoe:
How does it do it? It refutes the theorem, I mean negates the theorem, and then tries to get a refutation?.
Goldstein:
Right.
Bledsoe:
It does so by the so-called resolution technique, and it's the widest known method in all of theorem proving now. And then when my Imply came along, it was called a counter to that. I even wrote a paper called "Non-resolution Theorem Proving" about it.
Goldstein:
Could you describe in broad terms how Imply would go about a problem?
Bledsoe:
A matter of taking the negation and finding a refutation?. I'd leave it in the form it was and then try to prove it straight away.
Goldstein:
You have written that it was effective for programs that had a small sample space and could be searched quickly. Would it trial and error different proof techniques?
Bledsoe:
Well, it had a set of rules and it'd apply those rules to the formula. I wouldn't make it say true, I mean the whole formula is proved, but more often it would break it up into sub-goals. These have been called sub-goal provers. They worked on the sub-goal, and then keep going, hopefully without an infinite regress. I always had a cut-off point, you know, because you might eat up all the pieces.
Goldstein:
Yes.
Bledsoe:
It keeps it going itself and finally comes up.
AI and Theorem Proving
Goldstein:
Now you sat in the middle of these two streams. There were AI people and there are automated reasoning people. What in your training or background put you in this middle position? Why did you want to approach it by heuristics rather than resolution?
Bledsoe:
Well, I felt right off that resolution couldn't succeed on hard problems. It seemed to me to be too sympactic . Incidentally, now you understand my earlier remark, it's the most important process we've got. Right?
Goldstein:
Yes.
Bledsoe:
- Audio File
- MP3 Audio
(134 - bledsoe - clip 1.mp3)
It doesn't send much criticism, but I didn't think it could. Also it seemed unnatural to me. I wanted something like Imply, which was forward and natural. I'm a mathematician and I said, "How do I do it?" I might say, why do I like AI? Is it just a fad? They used knowledge that has been gained over the ages stored in a knowledge bank. That's the basic notion of AI to me, and mathematicians do the same thing. I'm not talking about logicians.
I was a mathematician out of Berkeley. We used knowledge that we've stored to solve new problems. Imply had a natural setting where you could use knowledge easily. You can store it onto there and use it solving problems. So I thought that was very important. I'm an AI type of a theorem prover, although I was also head of that improving [theorem proving?] community and still very much involved in it. I don't know if you know, but I got the Milestone Prize in that area this last January.
Goldstein:
Yes, you sent the clipping for that, and I'm using that as the source for much of the biographical information.
Bledsoe:
Right along with that, which was from the formal end and then I got this service award this last August from EESKYE , which is the international AI group. I've been in both camps.
Goldstein:
The people who were working in artificial intelligence were part of the artificial intelligence community. But you're saying they were different. How so?
Bledsoe:
There were some that were different. Like Robinson and Wass and Koos — they weren't enemies but they didn't come out of there like I did. I started over in [inaudible word] recognition and got into it later. So I had come out of a different strain. I don't know where Carl Yurick, another area worker, came from. Have you got anything on him?
Goldstein:
No. He may not have received a lot of funding from the foundation.
Bledsoe:
True. They were from DARPA mainly. Much of it was done by DARPA. Yurick was at MIT and he had this prover, I can't even pronounce its name. They definitely came out of AI. I thought their work was very important.
Goldstein:
Yes. In order to set the stage I want to mention these people even if they didn't have foundation support. If they are important in the development of the field up to the stage where you began getting NSF funding then I certainly want to mention them.
Bledsoe:
You know, I'm not sure I'm going to be too complete for you. Do you have Howell Long's name down anywhere?
Goldstein:
Yes. But you mentioned him.
Bledsoe:
Yes, because he had earlier received NSF funding.
Goldstein:
Was automatic reasoning considered a promising area in the early '70s?
Bledsoe:
There was also the theorem, the geometry prover. Art Flagenbaum's first book, Computers and Thought , had I would say four or five main topics in it. One of them was theorem proving. So it was earlier. And there was a theorem prover by Neil Simon Shaw and then there was a theorem prover by Lim from IBM on geometry. After that I started and got into various Str+ve kind of prover. But it got into set theory and calculus.
Switch from NIH to NSF Funding
Goldstein:
The way I understand it so far, it's up to 1972, you were working without foundation support, and you finished Imply. What then were the circumstances of your turning to the National Science Foundation for support?
Bledsoe:
I had an NIH grant and they reformulated their theory and Washington put it exactly, every dollar of it, under NSF. They didn't even ask me. They said, "Hey, we're going to put you on NSF," and I said, "Yes."
Goldstein:
You mean the NIH just transferred their support?
Bledsoe:
Yes. I didn't bother to check on the policy, and after that I applied to them directly and got everything I asked for, for a number of years. The last year or two by the way it [inaudible word].
Goldstein:
Who were you dealing with at the NIH or at NSF? Did you talk to people about what the new terms were, or the conditions?
Bledsoe:
I forget., but it was so standard in those days to get a grant without a lot of worry. I didn't go to Washington and talk to them. I didn't have to.
Setvar and Str+ve
Goldstein:
What was going on in your mind that made you start working on Str+ve? Or rather what are the differences between Str+ve and Imply?
Bledsoe:
What happened was that the interactive mode in Imply was a beautiful experience because we proved some hard theorems in there.
Goldstein:
For instance?
Bledsoe:
Why is a human having to put in this stuff? Why can't it just do it automatically? It was an open series of questions for me. I'll just take two of them, two were on limit theorems, not theoretic ones. I said, "Well, why do I have to put in this special heuristic? Why can't I just have a general purpose prover for this general area of inequalities?" It was trying to go into theorems that we couldn't prove that made us do these other things. They were in analysis by the way. That's why I call it inequalities, they were all related. The set variable stuff was in, again in real analysis, but it had to do with the sets that you deal with in the intermediate value theorem.
There is a whole bunch of theorems that really are in high order logic but they're so-called set variables, [inaudible word] logic easier, and I helped develop some techniques that could solve a bunch of those kinds of theorems.
Goldstein:
When did this happen? When did you begin working on Str+ve?
Bledsoe:
About '78.
Goldstein:
So you were working with Imply up through the '70s, and then you switched over the Str+ve in '78?
Bledsoe:
I've got them out of order. Set variable came before Str+ve. Set variables are what I tackled first and that would prove some theorems in topology real analysis that we couldn't do before. But it opened up again some problems in equalities that we just couldn't handle. Then I went back and said, "Hey, we've got to work on these inequality problems."
Goldstein:
That prompted your work on Str+ve.
Bledsoe:
Yes.
Goldstein:
You say you are a mathematician. Were you still actively working as a mathematician and these theorems that you wanted to prove were important to your mathematical work, or were they long standing problems that a number of people were working on?
Bledsoe:
I was still working as a mathematician, but not very much. I did publish at least one or two important math papers after 1970, but basically I had worked, had [inaudible word] proven theorems for myself and worked completely on getting the computer to prove theorems. A lot of what I did was about proving theorems, but I don't consider that real mathematics.
Goldstein:
Where did you get the inspiration for the problems that you wanted to prove? From the literature or from consultation?
Bledsoe:
I was chairman of the math department, and so I drew inspiration from math and from talking to friends, but mainly it came from the fact that these theorems had been around. Automatic provers today aren't yet powerful enough to prove the existing theorems.
Goldstein:
Right.
Bledsoe:
Some of those have been masterpieces, you know.
Goldstein:
That is a good question then. How much of the theorem proving that you did consisted of working on theorems that have already been proven and how much of it was to really prove an unproven theorem?
Bledsoe:
Practically all of it was the first was an attempt at new stuff. When I had been working with the interactive Imply it was to go out to the boundary of mathematics, but I didn't really get there. I was distracted. And so, much of my career has consisted of working on things that have already been done.
Goldstein:
You said that, but you also said that the switch from a Setvar to Str+ve was motivated by the need to prove theorems in a different area. Those must have been unproven theorems?
Bledsoe:
Wait a second. In using Setvar and Imply we weren't able to finish the proof of some things simply because they couldn't handle any quality parts of it.
Goldstein:
I see. So these were supposed to work in conjunction with one another.
Bledsoe:
Yes. Setvar would pose problems that it couldn't solve.
Goldstein:
Right, and then it would turn to Str+ve to do the inequality.
Bledsoe:
That was a little more coupled than I had thought of it, but in two or three years on each you tend to be off on one and not coupling. But right now they're coupled.
Goldstein:
I just want to be sure I've got this story right. You're working on Imply in the early '70s, then you start working on Setvar, and what were the differences in the approach between Imply and Setvar? Was it simply a different class of problems, or was the attack different?
Bledsoe:
Yes. The structure was still Imply's structure. It had in it some extra abilities. Remember I had a rule set. If you were trying to prove a theorem for sum A where A is a set, [inaudible phrase] you are trying to make up a set. Suppose you have a set on the real line such that it's open. Then you are trying to prove something about sets, ordinary resolution maps don't even do that, because it's [inaudible word] variable. So it just brings a number of terms like the Hiny-Burrell theorem that [inaudible phrase], a bunch of these ordinary intermediate analysis which have that form.
Goldstein:
Yes.
Bledsoe:
I'm trying to prove them because this is dear to my heart as a mathematician. I said, "Why can't I prove these?" So we came up with the Setvar stuff and we were proving some of them, but we would run into other kind of problems concerning research. We said, wait a minute, here is one problem that we have over and over again. They were inequality problems, which have a special prover to solve them.
Goldstein:
But were these still non-resolution type provers?
Bledsoe:
When we got that all working together, [inaudible phrase] parallel [inaudible word] history in a few words, Str+ve then I made a version of it that went back to the resolution mode. It didn't fit so well back into Imply however. In fact what I did was convert Setvar over to resolution mode too. One has advantages and the other has disadvantages.
Goldstein:
So there were two different Setvars and two different Str+ves, one that worked via resolution approach and one that was non-resolution?
Bledsoe:
Yes. Now the non-resolution Setvar is very recent, but the others are not.
Goldstein:
So, you begin working on Str+ve in '78 and then what happened? You were working on Str+ve as a non-resolution prover.
Bledsoe:
By '80 I had a resolution version of it.
Goldstein:
By '80 you had a resolution version?
Bledsoe:
That's the one that really turned out well. To tell you why I went back to resolution, there is just something fundamental that was very, very important there, and it made the difference.
Goldstein:
What is that?
Bledsoe:
The word v-e-s-t-r means one thing and v-e is another. Your variable elimination turns out to be easier in resolution than it does in Imply version. And it's possible [inaudible word] but it's very straightforward and easy there, and so that threw me back into that resolution mode.
Analogy
Goldstein:
Yes. And you say that they are coupled now. What's the story behind their coupling? What were you doing during the '80s after you did the resolution version of Str+ve?
Bledsoe:
Then I spent three years at MCC as vice president, so that interrupted the '80s.
Goldstein:
When was that?
Bledsoe:
1984 to '87. Then I got off on Analogy, which has absorbed several years of my life here. I'm not famous for anything in it, though. But that has so disrupted my life, and finally in the last couple years Larry Heinz and I have been pulling Str+ve and the resolution version of Setvariable together in one prover. Another prover of his, which extends Str+ve, and that's now getting into something that does all the things that I ever tried to do.
Goldstein:
I'm curious about the work on Analogy. First of all, was it funded by the foundation?
Bledsoe:
Not really. Just as a side note, I'd said earlier that so many mathematical theorems that haven't been proved by automatic [inaudible word], [inaudible word] automation, incidentally. If you are going to get the man involved, you can prove anything. I'm sorry. You can quote me on that.
They had it really clumsy, but you can prove anything as long as he is in there. If he can prove it, you can do it by the automatic prover. You think you were an idiot if you didn't believe that? To prove it, you ought to be able to [inaudible word] into symbols through the computer.
Goldstein:
Is this why the heuristic methods were as successful as they were, because humans became involved?
Bledsoe:
Yes. As I said, we weren't proving very hard theorems even with Str+ve and Setvar and all this. And because we are not doing what humans do. The humans use what they have done before as a guide. I mean Analogy is this key.
Goldstein:
By Analogy you mean not that the machine works in a way analogous to humans, although that's true, but you mean that humans work by analogy.
Bledsoe:
Exactly, that humans work by analogy. You have proved something before, and somebody says, "Can you prove this sum?" You then say, "Wait a minute, maybe that technique I used over there on the Hiny-Burrell theorem will work. Yes, well I've got to do some de-bugging here, but it looks like I can get this through. I got the main idea from there." That has eaten me. Because it's so needed.
The community has not used human methods enough. I'm one of the people that's gotten on the stump and said, "Hey. If you don't, you're never going to be very successful." Analogy is one of the main ways, and I've worked hard on that. Other people who have worked on Analogy had tended to do it on trivial kind of theorems, and I tried to do it on hard things, where really it tends to bring in techniques you have used before on hard theorems and uses them on new hard theorem.
Goldstein:
But how do you do that? How do you make the computer find analogies?
Bledsoe:
You have a given proof, and by the way it has to be a formally given proof, and somehow you have a new theorem you are trying to prove. You have to fetch an old proof—which implies how, [inaudible word] which one to fetch—and you start applying its proof to your new theorem until it fails. If it goes through, chances are the whole problem is too trivial for me to discuss with you.
Goldstein:
Right.
Bledsoe:
If it didn't fail somewhere. Now the question is how do you recover from that failure. And what it does, if you're smart, is give you a simpler new theorem to prove. You have to correct and fix that. There are usually one or more problems in there. There are a number of techniques to try to do that, and that's just how the human does it. I insisted that that had to be part of any future in this field. By the way it's very much like AI [inaudible phrase] traditional. I will not budge from AI being central in the future.
Goldstein:
What are you using as your foundation for your model of how humans work? Your own experience or what?
Bledsoe:
Yes. But in one of my best examples I took the proofs right out of a published paper, one I published in 1970, and I formalized it. Because it was words and symbols [inaudible phrase] put it without changing hardly anything, and just put it in its formal setting. Then I said yes, take a theorem like it and devise a proof from that. Of course, how do I know how to de-bug? You bet I used my experience and others in mathematics.
Goldstein:
Have you succeeded in proving any harder theorems using this analogy approach?
Uses of Analogy
Bledsoe:
That's one of my complaints, the literature isn't very hard. Here are some theorems that people have proved and I haven't been too impressed with.
Goldstein:
And this was done by Analogy.
Bledsoe:
Yes. I didn't do it. Why did I not do it? Because I claim the second one is true in the first place, why did you bother with Analogy? I'm sorry that's — without hurting people's feelings — that's what I felt.
Now let me give you one that we did do. The limit of the sum is — without heuristics — is a hard theorem for provers. It's the limit of the sum, or the sum of the limits. Yes? Now take the limit of the prior product of the limits, we used Analogy to prove it from the proof of the first. From the proof of Lim Plus we got the proof of Lim Times. And that's not trivial. Provers can't easily get the second part. We are just now getting finishing touches on them.
It sounds like I'm using resolution, or at least the part about the theorem of resolution. Yes? [inaudible word] of resolution, if you are given the proof of that, you can prove the completeness of lock resolution. This is another version. And there is one where Analogy is just perfect, and yet it is very difficult to get the computer to follow that first proof because it's high order and a bunch of other stuff. That is my milestone, and I am trying to finish up now.
Goldstein:
You are working on Analogy now. When did you begin that?
Bledsoe:
In '80s. I'll tell you, I've been at it awhile.
Goldstein:
Yes, so that does constitute much of the work in the '80s, working on Analogy?
Bledsoe:
That and finishing up these other things, and being at MCC.
Goldstein:
Right.
Bledsoe:
I even had an agreement with my colleagues that I wouldn't publish until I had something that I was really proud of.
Goldstein:
You said that other people working in Analogy have proven some trivial things.
Bledsoe:
I don't have to quote them, do I?
Goldstein:
No, but I am curious who else is working in Analogy?
Bledsoe:
Steve Owens has written a book, and it's a good book. Believe me, I'm not trying to put him down. But the examples he gives tend to be simpler examples in there.
Goldstein:
Will it do things that could be done with other techniques, like either Str+ve or Setvar? Are they are simply using a sledgehammer to open an egg?
Bledsoe:
Definitely. I believe that in fact all those examples in the book can be done separate, except the one where he quotes us. And the book lays out a lot of good techniques in that, so I reference it in my work without putting it down. But I'm waiting for the first real milestone or two.
Goldstein:
To make the Analogy work, are you taking other techniques from AI?
Bledsoe:
That's [inaudible word] knowledge about what to do if you get in a problem.
Goldstein:
Right.
Impact of Analogy on AI
Bledsoe:
Incidentally, there is quite a bit of Analogy being used in problem solving in AI. I didn't say theorem proving. I don't think this problem is as hard as some of the theorems we were proving. But they're more involved with the stuff that's in the problem, and you see quite a bit of that being done in AI.
Incidentally, Himey Carbonelle is one of the main people in Analogy in AI. Not really in mathematics. I think if you were to mention his name you would be fair. I'm not putting that down at all.
Goldstein:
Yes.
Bledsoe:
There must be a hundred papers that have used something about Analogy in the AI stuff.
Goldstein:
Can you account for the increased excitement of automatic reasoning because of the introduction of Analogy? Is it possible that this is a promising new technique that has brought a lot of attention to automatic reasoning?
Bledsoe:
It ought to be that, but honestly I can't say. What happened is practically nobody in automatic reasoning has worked in Analogy, and yes, some of that did come from earlier work in AI.
Goldstein:
What makes Analogy so controversial?
Bledsoe:
It's too hard for them. I mean you don't work on mountains you can't climb. You think you can climb them and that's why you start, but if it's too hard. They said "We can't do that." "You won't ever do it. Quit working on it." And I said, "Well, I'm sorry. You're not my boss."
NSF Support and Grad Students
Goldstein:
How has the foundation worked in all this? Have they been generally supportive of your work? Have they offered any suggestions?
Bledsoe:
Yes, but it's dependent who's back there. It's a little bit like once they found that my early work was turning out papers they didn't tend to challenge them much. By the way, the referees decide all of this. I've had some, of course some [inaudible word] referees of reports about things my colleagues have tried to do.
Goldstein:
Who were some of them?
Bledsoe:
There was Donald Loveland at Duke in the APP community.
Goldstein:
When you submit a proposal to the foundation, what does the budget usually contain? Is it research assistance or support for grad students? Is it hardware computer time?
Bledsoe:
It has mainly been about a salary for myself, an occasional postdoc, a graduate student and an occasional undergraduate. A little bit on computers, some on travel and that stuff, but that's it.
Goldstein:
Right. Have you worked with any important or significant grad students?
Bledsoe:
There was Bob Boyer who is famous for the Boyer [inaudible word], he was my student. The others are not as well known. Larry Heinz, who is my current postdoc, is one of the best I've had. Some of them are pretty smart.
Prologue Style Compilation
Goldstein:
One of the things that you wrote when discussing Analogy was that you are not using Prologue style compilation techniques or other techniques. I wonder if you could explain that to me, what are those other techniques, or even Prologue style?
Bledsoe:
Did I use the word Prologue?
Goldstein:
Yes.
Bledsoe:
Incidentally that's nice language. I didn't think I used it. In using Analogy, what did I say?
Goldstein:
In my notes I wrote that you say that you did not use Prologue style compilation techniques.
Bledsoe:
There was a tremendous speed-up in provers, automated provers, a few years ago. Something like 100 to 1. There were some new techniques for proving. One was the so-called Prologue compilation techniques. I don't know if you're aware of the Warren machine stuff. But it was very powerful.
Goldstein:
You say this happened a few years ago?
Bledsoe:
Yes, I'd say maybe five to eight years ago. There was the Prologue style compilations. There was another thing they called Indexing and it also sped up things. But my view is that that speed-up of 100 distracted the field. It seemed to be helpful, and it is, but for proving mathematical theorems all you do is push a little deeper in the search tree. A hundred sounds like a lot, but if you have a branching factor of ten, what are you then, two deeper? Some of the math proofs are 30 deep, or 60, and so I loved having the speed. But it's not enough on its own. So you've got to do something like Analogy that cuts through that, cuts through that depth. Somehow it skirts around. So I said my Analogy prover didn't use these techniques, not because I wouldn't like to have them in there, but because it's just too much trouble to get them. I'm working on something I think is more important than speeding it up a little.
Goldstein:
Did you say it distracted the field, the speed-up techniques?
Bledsoe:
I hate to put it that way, because it's so important. For engineering applications, most of the speed would be worth its weight in gold. But for ordinary mathematics it doesn't help very much, I don't know any hard theorem you can prove after the 100 to 1 that you couldn't before. Isn't that amazing? The prover is 100 times faster, and you still can't prove this theorem. Why? Because the [inaudible phrase] it just kills you when you use syntactic methods.
Goldstein:
Could you describe that to me a little bit, syntactic methods, that has to do with laying out a proposition formally?
Bledsoe:
By the way, resolution essentially says if you have P and P implies Q, then you get Q. And you do that over and over again with a set of data until you finally get the thing it's trying to prove. That process doesn't have any direction or anything. Now there are a hundred versions of resolution, but you try to give a little direction to that and it hard because they're all syntactic. If you bring them some knowledge, a knowledge base of past experience, which resolution doesn't have any place to put, then we wouldn't try all Ps against P implies Qs. We'd say, "Hey, wait a minute. Here's what we're trying to prove. Let's see." It should be very selective of which one of those we would do.
Expert Systems and Theorem Proving
Goldstein:
It sounds like you want to create an expert system at theorem proving.
Bledsoe:
Yes.
Goldstein:
Have you discussed with people working in that area?
Bledsoe:
Well, [inaudible phrase] for system shells [inaudible word] don't seem to fit too well, because you need so much other stuff. But that's the basic idea. Before I ever heard the word expert system, that's what we were trying to do.
Goldstein:
When you say the other work in expert systems doesn't fit in, why is that?
Bledsoe:
I didn't say that. It's just that so much is involved in the inference calculations. It's an expert system mode because there is knowledge there and you are using it, but quite a bit is going on. It isn't a matter of just doing some production rules.
Impact of Advanced Hardware
Goldstein:
Do advances in hardware affect your ability to pursue this particular line? As you get better and faster memories, does Analogy look more promising?
Bledsoe:
Bigger really helps, but you heard what I just said about 100 to 1, didn't you?
Goldstein:
Right.
Bledsoe:
Anyway, you get the message. If I could have had some of the ideas 20 years ago that I have now, I think we'd have had almost the same result. Now they're bigger, and it helps immensely, but it ain't the difference. I don't mean it isn't important. It's just that the ideas are more important. I think anyway; you are getting my opinion here a lot.
Other Contributors to Field
Goldstein:
Yes. Actually we may be ready to wrap up. I want to give you an opportunity to point to any particular aspect of your career that you think some attention should be brought to.
Bledsoe:
I guess the main concern I have is that somehow people get the impression I didn't reference anybody else. That I didn't mention other names that are so important in this field. Back then when we were talking high order logic for example, Peter Andrews has played a major role in that field.
Goldstein:
Yes,
Bledsoe:
I don't tend to be one to try to change things around, so don't assume that. But I did like to just make sure. I wouldn't say, "Hey I need to add a page here" to something, but I would like to just make sure that I'm not embarrassed by something that misrepresents my ideas. That's my only concern.
Goldstein:
No, that's fine.
Importance of NSF
Bledsoe:
I guess if I could just say a word or two about the importance of the NSF to my work. And that it has been important in automated reasoning, and AI has always been a central issue to me in that. There are a lot of colleagues in this. Some disagree with me, but usually they're all friendly.
I think anything you said in terms of Imply or Str+ve, those have been just examples of trying to say it overall. To me that's what it sounds like anyway.
Goldstein:
There's one thing I did want to ask you. You said previously funding was relatively easy to obtain, you'd just submit your proposal. Are things different now?
Bledsoe:
The last few years NSF has cut back a great deal in funding.
Goldstein:
You've still been able to get funding, correct? You say you've been supported consistently.
Bledsoe:
I've been supported. Just it isn't quite as easy. It used to be just about what I'd write is what I'd get. Now they say, "Can't you take a lot less?" I say, "Sure." Of course I'm 70 years old. Maybe that might have something to do with it, I don't know.
Goldstein:
No, I'm hearing that story from a couple people. The field has mushroomed, there are so many more researchers, and funding hasn't increased proportionally.
Bledsoe:
By the way, there is this trend we said in the beginning, and most of the new ones are in it. Some people are just almost in [inaudible phrase] with the languages and things. By the way their goals even seem to be different from mine. I have, everybody has, different goals. They're trying to develop techniques for something, and I'm trying to say, "Look. I got these theorems in math and I'm trying to get my prover to prove them. Never mind showing my technique if you can't show me it gets me anywhere with my goal. I'm not going to read it."
Goldstein:
That's interesting. How would you characterize this more recent work. You say it isn't goal oriented. What is it?
Bledsoe:
Its goal is a goal of setting up formal procedures that somehow are complete. The word complete has taken on a new meaning. It always meant if you've got a set of rules that will eventually get you to the result, [inaudible word] for that set of results it will get.
My view is it isn't enough to be complete; it has to be effective. The computer will do that in less than 100 million years. Yes? That's been the difference. The recent trend has been, "I'm not going to worry a lot about implementing this. I'm more interested in whether it will formally do it." Category:Mathematics]]
