Oral-History:Martin Davis

About Martin Davis

Martin Davis was born in 1928 in New York City to parents who had known each other in Poland, but did not marry until they had met again in the US. He received his Ph.D. from Princeton University in 1950, where his adviser was Alonzo Church. He is known for his work on Hilbert's Tenth Problem and for his model of Post-Turing machines. He is the co-inventor of the Davis-Putnam and the DPLL algorithms. He is a co-author, with Ron Sigal and Elaine J. Weyuker, of Computability, Complexity, and Languages, Second Edition: Fundamentals of Theoretical Computer Science, a textbook on the theory of computability.

The interview traces his work, from Hilbert's Tenth Problem through the Complement Problem, with an emphasis on means of funding, ranging from the National Science Foundation to the Office of Naval Research.

About the Interview

MARTIN DAVIS: An Interview Conducted by Andrew Goldstein, IEEE History Center, July 18, 1991

Interview #108 for the IEEE History Center, The Institute of Electrical and Electronics Engineering, 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 at Stevens Institute of Technology, Castle Point on Hudson, Hoboken, NJ 07030 USA. 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:

Martin Davis, an oral history conducted in 1991 by Andrew Goldstein, IEEE History Center, Hoboken, NJ, USA.

Interview

INTERVIEW: Dr. Martin Davis

INTERVIEWER: Andy Goldstein

DATE: 18 July 1991

PLACE: Telephone Interview

Academic Biography

Goldstein:

Could you outline your academic biography for me?

Davis:

Sure. My undergraduate training was at City College in New York where the logician Emil Post was one of my teachers and a very influential one. I went to Princeton as a graduate student in 1948 and got my Ph.D. in 1950 with Alonzo Church.

Goldstein:

The degree from City College was in 1947?

Davis:

1948.

Goldstein:

That was at the master's.

Davis:

No, that was a bachelor's.

Goldstein:

Oh, you went straight from a bachelor's to a Ph.D.?

Davis:

I got a master's degree in 1949 at Princeton.

Goldstein:

I see.

Davis:

I don’t know what the rules are today, but the master's degree wasn’t a very big deal. You passed the qualifying exam for the doctorate and they gave you a master's degree. There was no thesis requirement.

Goldstein:

Right, okay.

Davis:

The reason that I was able to finish so fast was not because I’m a genius, but because the subject that I was interested in, Recursive Function Theory, out at that time, was a very small literature. I'd started studying it as an undergraduate, when one could really get to the limits of what the boundaries of what was known very, very quickly. I hesitate to think what my success would be if I tried to get into the field today, where you really have to be a virtuoso in some very difficult techniques to get anywhere. Anyhow, my first job was at the University of Illinois in Urbana where I held the position of Research Instructor. I was there for two years, from ’50 to ’52; however, I did not remain in that position partly because of an interest that I developed in computers. Urbana had just started the Illiac Project. It was partly a matter of ducking the draft in the Korean War. While working at the Illiac Project I got involved in a military project which made use of the computers they were developing there, to build what nowadays would be called real time programming systems. I wrote what from a concurrent point of view would be regarded as an incredibly naïve program, that was supposed to navigate a hundred airplanes in real time. In 1952 I left the University of Illinois and went to the Institute for Advanced Study in Princeton for two years as a temporary member. I was supported by the Office of Naval Research at that time, a temporary membership.

Yeshiva University & Hilbert's Tenth Problem

Goldstein:

Well, we went over the list of grants. I have your first National Science Foundation grant in 1967. There might be some before then. It actually becomes difficult to track down grants before that because the Office of Computing Activities hadn’t organized yet.

Davis:

I had NSF support starting before that. The grant was really more in pure mathematics but there was support in ’62 in fact.

Goldstein:

Okay. Could you tell me something about that work? I’m interested in the biography, in the way that it describes how you became involved with computers and interested in computer theory. If you say that your original grants were NAT.

Davis:

I was at Yeshiva University, where there were no computing facilities, and I let that side of me go into abeyance at that time. I was interested in things that would be called Theory of Computation nowadays, but nothing that actually involved really working with computers. Then in 1965 I came to New York University where I have been ever since. That's when I got a rather substantial NSF grant to work on Mechanical Theorem Proving. I don’t really remember how long that continued, but it did for many years. Probably about a decade.

Goldstein:

Well, let’s start with ’62 when you said you were at Yeshiva University then, and you started to get money. What were you working on? What was the proposal?

Davis:

Hilbert's Tenth Problem, Hierarchy Theory were really the main focuses of my interest. I was interested in things that I call proof theory nowadays. Aspect of the Hilbert's Second Epsilon Theorem was one of the things that I was working on.

Goldstein:

I’m not familiar with the mathematics. Is that unrelated to computer science?

Davis:

Well, it’s not clear. In fact, I have co-authored a paper that is just about to appear which suggests that the Epsilon Calculus might even have applications in automated deduction. It’s not clear.

Goldstein:

At the time you weren’t thinking along those lines?

Davis:

Not at all. I wasn’t thinking algorithmically, but foundationally, really.

Goldstein:

Okay, so at that time you had money when you say from the NSF, from the mathematics program?

Davis:

Yes, there was no computer science program at that point, if I’m not mistaken.

NYU and Theorem Proving

Goldstein:

Right, right. But then you say in ’65 you received a chunk of money.

Davis:

In ’65 I moved to New York University and was supported continuously for something like ten years. At first I was associated with the University Heights campus of NYU, which no longer exists. I was in the mathematics department there and the situation was flexible enough so that I could have a group of young researchers who were working on various things. From a computer science point of view, the most prominent of those is Don Loveland. He developed his Model Elimination Algorithm for theorem proving and predicate calculus, which has recently had quite a bit of attention.

Goldstein:

Just could you describe what that is, the Model Elimination?

Davis:

It’s really too technical. It is something that turned out to be a variant of S-Linear Resolution, as the original motivation. The intuitive idea was that typically theorem proving algorithms use a refutation point of view, and human mathematicians tend to refute things by constructing models, the program attempting to work in that manner. That is why it is called Model Elimination.

Goldstein:

Well, in 1965 you said you moved to NYU. What turned your attention to theorem proving?

Davis:

I was interested in theorem proving all along. Hillary Putnam and I had done work that was sponsored by the air force in 1958. Then there were some actual programs written at NYU when I was a visitor at NYU in ’59 and ’60. The work of Hillary Putnam and myself was published in the JACM, Journal of the Association of Computing Machinery. Then, the implementation resulted in a paper that appeared in the communications by me, Don Loveland, and George Logoman. So it was a long standing interest, but it went into abeyance when I was at Yeshiva because there really weren’t any computing facilities to speak of.

Goldstein:

I see. You were still at the IAS when you were doing the work that you just mentioned?

Davis:

Oh no. That was just the two years from ’52 to ’54.

Goldstein:

And where were you with Putnam?

Davis:

Putnam was at Harvard or Princeton. He has moved between the two. I was at Rensselaer Polytechnic Institute’s graduate center in Eastern Connecticut. I was there from ’56 to ’59, for three years. Hillary and I had support during the summer. The first support was from the National Security Agency, and then the two subsequent summers from the air force when we were doing that work.

Goldstein:

Okay, I see. At NYU when you started working on theorem proving, were you working with hardware or was this all theoretical?

Davis:

I wasn’t doing any programming myself, but there were a number of people supported on the project who did some programming. There was David Jarmush and Josh Fisher and Fleisid. Fleisid actually wrote the first model elimination program.

Goldstein:

Well, what were the dimensions of the project when you say a couple of people working on it? You said earlier that it was a lot of money. How many people?

Davis:

I never said it was a lot. I said it continued for a long time. I don’t remember what the amounts of money involved were, but they were not gigantic.

Goldstein:

Right. But a team of at least four people?

Davis:

What they had boiled down to was summer support for a handful of people plus some staff people. Generally no more than two at any one time.

Goldstein:

And those were the key items in the budget? There wasn’t a hardware component? Was there money for grad students?

Davis:

There was always money for grad students, and there was money for computer time. We got to use the computers and the Academic Computing Facility here at NYU. There was first an IBM 7090 and then an IBM 370 or whatever the current technology was at the time.

Goldstein:

Right. Those were computers that NYU had?

Davis:

Yes, they were computers that NYU had and they were managed by the Academic Computing Facility. A lot of the funding for that computing facility came from the Department of Energy, in fact.

Goldstein:

Yes, I could see that the laboratory may have had support from other sources. Did your project have co-support from the military?

Davis:

No, it did not. We generally paid for our own computer time. I don’t remember the details, but the ACF, the Academic Computing Facility was always generous. If we ran out of computing time, they didn’t make us stop using the facility. It was more a matter of citizenship to help support the effort in that way.

Shortcomings of Theorem Proving Research

Goldstein:

<flashmp3>108_-_davis_-_clip_1.mp3</flashmp3>

Can you tell me some of the highlights of that work then? Did you manage to successfully prove any particular knotty theorems?

Davis:

No. In fact I would say that the work kind of petered out at a certain point and, all in all, I’m not immensely proud of the effort. The algorithms we managed to produce, the algorithms that we coded, managed to prove some fairly standard theorems, but the group at Argon Labs really got way ahead of us and did a lot better than we did in my judgment.

Goldstein:

Who was at Argon?

Davis:

Larry Wost was the leader in that effort.

Goldstein:

I just spent some time talking to Bertram Rafael who was at SRI , and he was telling me about the automatic theorem proving that he had been doing, using first auto-predicate calculus. Are you aware of his work?

Davis:

Yes.

Goldstein:

And how did yours relate to his?

Davis:

As you gather, I’m not especially proud of what we did and I would regard his work as even less interesting than ours.

Goldstein:

Oh really. In what ways?

Davis:

I don’t think that it got anywhere. The group that really did well was the group in the Chicago area, Larry Hennsion and Ross Overbeak and Larry Wost. Their work was, as far as I’m concerned, head and shoulders above the rest of us.

Goldstein:

And what causes you to say that?

Davis:

Honesty.

Goldstein:

But by what criteria are you judging the results?

Davis:

The flexibility of the software and the kinds of theorems that they were able to prove. They proved a lot harder theorems than we did and certainly what Bertram Rafael did. Recently they were able to settle some open questions that Herb Kaplansky, who is a prominent algebraist, had raised about semi groups. You know, they really did it right. They knew what they were doing.

Goldstein:

In what ways did their approach differ from yours? I mean, you said that you were using predicate calculus and that is what I heard.

Davis:

Well they were using predicate calculus too, but they were doing a much better job. Their basic theory that they were using, as far as I was concerned, was no better than anything the rest of us knew about. But their implementation skills were really much better.

Goldstein:

In terms of designing a software?

Davis:

That is right.

Goldstein:

I see. So, are you characterizing your work now between ’65 and ’75, or was this only one stage of it?

Davis:

It’s not the only thing that I was doing, but the work that involved computers specifically I would put it in that category.

Goldstein:

Okay. I would like to be able to offer some examples, or some specific information about this. So when you say you managed to prove some theorems, could you just name a few?

Davis:

There were elementary theorems and group theory: "the left inverse is a right inverse," "the left identity is a right identity," "if the square of every element is the identity, the group is ebullient". I dealt with things of that level of difficulty.

Goldstein:

Okay. Did this work have impact in any other areas? I know, again like I said, most of my familiarity with this area comes from talking to Rafael. Rafael was describing how his work applied in this robot project they were building out at SRI.

So what is the real objective then for these systems? Is it to prove theorems that are unproved now?

Davis:

That is what I think are the real objectives. I think that will happen someday. We are still very far from it.

Goldstein:

What is missing?

Davis:

Understanding. It’s a matter of the progress of science.

Goldstein:

Well is it the fundamental logic or the ability to implement it in terms of software?

Davis:

Well, if I knew the answer to that I would write a paper. As I’m sure that you know, science is an open ended undertaking. One thing that is very clear is that human mathematicians are very, very good at proving theorems, at coming against an open question and marshaling techniques of all kinds. Algorithms, to do that kind of thing, certainly, just at the predicate calculus level, it’s all much too primitive really. How to incorporate higher order constructs is something that is not very well understood. Woody Bledsoe is someone who has attempted to do that to a certain extent. I don’t think that they have come to grips with the real issues here.

Goldstein:

When you say higher order concepts, what things are you thinking of?

Davis:

Sets, functions, integrals, derivatives, and formal mappings, topological spaces. All of the things that mathematicians talk about.

Grants and the Complement Problem

Goldstein:

All right. Let’s say that this brings us up to the mid ‘70s. Did you cease your work then in this area?

Davis:

No. The truth is that I generally am able to only think about what I’m passionately interested in at a given moment. It has floated in and out. As I mentioned, I just did some work quite recently that I think might have applications in automated theorem proving. There is a paper coming out.

Goldstein:

Are you still under NSF support?

Davis:

No. I haven’t been for many years. My research more recently was supported by the Office of Naval Research, and it was an entirely different area, in the theory of software testing. Which is something that interested me for awhile.

Goldstein:

Was ONR interested in supporting automatic theorem proving at that time? You said that you were getting NSF money. Were there other places that you could turn?

Davis:

Yes, I was getting air force support after NSF support ceased.

Goldstein:

That was when?

Davis:

Oh, I have lost track of the years. Congress said that the military couldn’t support research unless it had direct and specific military application. At that time, I told the air force that I couldn’t really take their money under those conditions. And then things softened again. Certainly, software testing is fraught with practical implications. The kind of work that I was doing was not going to have any immediate applications.

Goldstein:

Yes, in looking over this list of grants that you received I see a grant called Computation and Logical Proof Procedures. It was renewed many times up until 1976.

Davis:

That is what I was talking about.

Goldstein:

And then I see grants in ’78 and ’80 called Logical Investigations into Computer Science and that is fairly ambiguous. I can’t get a sense of what you were after then.

Davis:

Actually, I remember now. That is what happens when you live so long, it all gets to be amorphous. Yes, I was working on theoretical issues at that time, particularly on the context sensitive languages. I was really interested in this complement problem that was solved just a couple of years ago. I can’t say that I made any great contributions there.

Goldstein:

Can you describe it for me, the complement problem?

Davis:

Noam Chomsky had a hierarchy of formal language types depending on the kinds of grammars that generated those languages. One of the categories was called context-sensitive languages. They turned out to be equivalent to languages that could be generated by grammars with production rules, in which the substitutions always resulted in strings that were no longer than the original strings. The question was whether the complement of a context-sensitive language had to be context-sensitive — that is, whether the set of all strings in the alphabet in question that didn’t belong to the language could also be generated by another context-sensitive grammar. That was recently proved to be the case, but it was an open question for over 20 years. That was really the main thing that I worked on for that research.

Goldstein:

I see. I’m interested on how you tackled it? Also, did you consider that computer science work?

Davis:

Yes, it’s the theory of computation. I’m not the only one that worked on that problem very hard. Burroughs Hart-Manus at Cornell University is a very prominent computer scientist.

Goldstein:

Right. I intend to speak to him actually. Who finally got it? Who cracked complementarity?

Davis:

I’m sorry, but I’m having a problem generating it. They might know him very well. He is a young theoretician.

Goldstein:

How did you go after it? What was your approach?

Davis:

I was using alternating Turing machines.

Goldstein:

Did that involve use of hardware or was that all pencil and paper?

Davis:

It was all theoretical.

Goldstein:

I see. Were you working with anyone else on it? Grad students or collaborators?

Davis:

Elaine Wyuker.

Goldstein:

Was she faculty at NYU?

Davis:

Yes.

NSF Grants

Goldstein:

Okay, so you worked on that for a couple of years and then when did NSF money break off?

Davis:

You probably know better than I do. I really haven’t kept a careful diary of it.

Goldstein:

Could you recall any other major research project that you undertook under NSF support?

Davis:

No.

Goldstein:

I wonder if you could comment on the cooperation that you received from NSF? The reception that you received from them for you proposals. Were they eagerly received? Did you have to do much negotiating with them?

Davis:

I would say that it was quite variable. There were times when they were very forthcoming. In fact, there was one period when I got a call out of the blue from the NSF saying that this proposal that I had sent in was something that they would like to fund in a more extended way. That was very forthcoming.

Goldstein:

Was that a computer one or a math one?

Davis:

It was computer. That was the thing that you mentioned that went to 1976.

Goldstein:

The theorem proving.

Davis:

As I recall, it was the summer when I was in Aspen, which would mean 1971. So it went from ’71 to ’76. It was a five year grant. If I’m correct, NSF was expanding quite a bit in computer science at that time.

Goldstein:

That is right. Were you aware that there was any particular program that they wanted to emphasize in terms of supporting grad students or promoting a particular line of research?

Davis:

No, I’m not one of those professors who trotted off to Washington all of the time. We just did our own stuff here. I didn’t have any particular impression. In fact, I had the impression that they were supportive and wanted us to do what we thought was appropriate.

Goldstein:

Okay, I’m trying to get a sense of what the understanding in the community was at the time. When you would talk to other computer scientists, was it understood that there were certain places that you went for certain fields of research? Or did anyone feel like they had a good shot at NSF money or defense money?

Davis:

I don’t think that I had many conversations along those lines.

I was very pleased that my research was being supported. The atmosphere really changed. I think the kinds of questions that you are asking are more appropriate for the era of the last five or six years than for the time that we are talking about.

Goldstein:

Funding was not much of an issue then?

Davis:

That is right. How shall I put it? It was all a lot less cut-throat.

Goldstein:

But basically, if you were a scientist and you had a legitimate research proposal you could expect to receive support?

Davis:

It would likely be received in a hospitable way. At least that was my sense.

Shift to Algorithmic Analysis

Goldstein:

And now I’m moving away from the financial end of it, and I’m just speaking about the field of computer science, or maybe even theoretical computer science. Was there an excitement about the subject at the time? Did you find your particular field becoming hot or en vogue?

Davis:

Yes.

Goldstein:

During the early ’70s?

Davis:

Yes. In the ’60s and ’70s.

Goldstein:

Did interest start to wane?

Davis:

First of all, I distinguish my interest with first order logic theorem proving and theory of computation, which are really quite different. The aspects of the theory of computation I was interested in were what people would call high level theory. The interest shifted very much to algorithmic analysis. It’s a very important subject, but it’s one that I haven’t had any great personal interest in. People tended to lose interest in the higher level theory.

Goldstein:

I want to be sure that I understand what you are saying. First order logic refers to the theorem proving that you were talking about before.

Davis:

Right.

Goldstein:

And the theory of computation — is this the other aspect that you were interested in, in the late ’70s?

Davis:

The theory of computation generally is the mathematical study of models of computation. You can model computation at various levels, at the very abstract levels and relatively concrete levels. They are all worthwhile and worthy undertakings, but the focus of interest is quite different.

Goldstein:

When you were doing the work in theory of computation, who were other people interested in that same area at that time?

Davis:

I have mentioned Hart-Manus and Emanuel Bloom.

Goldstein:

Okay. Any contrast between your approach and some of the other ones?

Davis:

I would say that they were more successful than I. How is that?

Goldstein:

Okay. I’m trying to understand the research program that you defined for yourself, in comparison to some of the others.

Davis:

We were all looking at what we thought were interesting questions, and trying to answer them, and prove the appropriate theorem.

Goldstein:

Do you have any generalizations, any impressions that you would like to offer about the role of NSF in the field or the development of the field, independent of the foundation?

Davis:

No. I think that they had a very supportive role and a very important one. I think that the more relaxed atmosphere in the earlier years, corresponding to fewer people in the field and easier funding, made for better science. People were comfortable with more long term reflections. The tendency nowadays as I see it is more frenzied and more focused on quick results and that doesn’t necessarily go with deep thinking.

Goldstein:

I’m not sure that I caught this. What has your research been concentrating on during the ’80s as you moved away from the theory of computation towards something else?

Davis:

The theory of software testing.

Goldstein:

And you are saying that the Navy has supplied support for that?

Davis:

Yes, the navy supported that For the last year or so my research hasn’t been supported by anybody.

Goldstein:

Just NYU?

Davis:

Right.

Goldstein:

Okay. Thank you for taking the time to talk to me.