Abstract
This brief autobiography highlights events that have had a significant effect on my professional development.
“My father and mother were honest, though poor –”
“Skip all that!” cried the Bellman in haste.
“If it once becomes dark, there’s no chance of a snark–
We have hardly a minute to waste!”
“I skip forty years,” said the Baker, in tears,
“And proceed without further remark ...”
–Lewis Carroll’s “The Hunting of the Snark”
This is a revision and expansion to the present of an earlier autobiographical essay [22], much of which is included verbatim. I am grateful to Springer Verlag for their permission.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
That is, the language using the symbols \(\lnot \supset \vee \wedge \exists \; \forall \, =\) of elementary logic together with the symbols \(0 \;\, 1 \, + \, \times \) of arithmetic.
- 2.
The jump of a set A of natural numbers may be understood as the set of (numerical codes of) those Turing machines that will eventually halt when starting with a blank tape and able to obtain answers to any question of the form “\(n \in A?\)”.
- 3.
For example, the “Pell” equation \((x+1)^2 - d(y+1)^2 = 1\) has natural number solutions in x, y just in case d belongs to the set consisting of 0 and all positive integers that are not perfect squares; hence that latter set is Diophantine.
- 4.
A set of natural numbers is r.e. if it is the set of inputs to some given Turing machine for which that machine eventually halts.
- 5.
It furnishes no example of a Diophantine set whose complement is not Diophantine.
- 6.
Actually, Kleene’s system \(S_3\).
- 7.
Actually without any bound on the ordinal all the sets in the hierarchy are representable with only one second order function quantifer.
- 8.
Clifford Spector showed that the result remains true for all constructive ordinals in his dissertation, written a few years later under Kleene’s supervision.
- 9.
In [40] p. 61.
- 10.
Actually, indices of r.e. sets.
- 11.
- 12.
The report was reprinted in [43], pp. 41–48.
- 13.
The existence of “minimal” degrees. Only 31 years old, Clifford Spector died quite suddenly in 1961 of acute leukemia, a tragic loss.
- 14.
[7].
- 15.
The translator for the Italian version called it a “libro classico”.
- 16.
A review of the Dover edition by David Harel referred to the book as one of the few “classics” in computer science.
- 17.
\((\forall k)_{\le y} (\exists u) \;\ldots \) is equivalent to saying that there exists a sequence \(u_0 , u_1 , \ldots u_y \) of numbers satisfying \(\ldots \) The use of the Chinese Remainder theorem to code finite sequences of integers had been used by Gödel to show that any recursively defined relation could be defined in terms of addition, multiplication and purely logical operations. I had used the same device in obtaining my normal form.
- 18.
[27].
- 19.
Abraham Robinson had proposed similar investigations in a talk at the Cornell Institute. I attended that talk, but Hilary didn’t. Somehow, I didn’t connect the two ideas until years later when I noticed Robinson’s paper in the proceedings of the Institute.
- 20.
[40] p. 93.
- 21.
What has become known as the satisfiability problem.
- 22.
These are:
-
1.
The one literal rule also known as the unit rule .
-
2.
The affirmative-negative rule also known as the pure literal[3.] rule.
-
4.
The rule for eliminating atomic formulas
-
5.
The splitting rule, called in the report, the rule of case analysis
The procedure proposed in our later published paper used rules 1, 2, and 3. The computer program written by Logemann and Loveland discussed below used 1, 2, and 4. The first of these is the “Davis-Putnam procedure” which has been the subject of theoretical analysis, nowadays referred to as DP. The second choice is the one generally implemented, is usually called DPLL to refer to the four of us. It still seems to be useful. I might mention that I have received two awards based at least partly on this work and that I feel strongly that Hilary, at least, should have shared them.
-
1.
- 23.
Among other matters, we needed to find an exponential Diophantine definition for the relation:
$$\begin{aligned} \frac{p}{q} = \sum _{k=1}^{n} \frac{1}{r+ks}. \end{aligned}$$We didn’t go about it in the easiest way. We used the fact that
$$ \sum _{k=1}^{n} \frac{1}{\alpha +k} = \frac{\varGamma ^\prime (\alpha + n +1)}{\varGamma (\alpha + n +1)} -\frac{\varGamma ^\prime (\alpha + 1)}{\varGamma (\alpha + 1)}, $$expanded \(\varGamma ^\prime / \varGamma \) by Taylor’s theorem, and used an estimate for \(\varGamma ^{\prime \prime }\) to deal with the remainder.
- 24.
See [36].
- 25.
AFOSR TR59-124.
- 26.
Cf. [33].
- 27.
See footnote 22.
- 28.
- 29.
Here if \(\ell = \lnot R(c_1 , c_2 , \ldots , c_n)\) then it is understood that by \(\lnot \ell \), the literal \(R(c_1 , c_2 , \ldots ,c_n)\) is meant.
- 30.
It was J.A. Robinson’s key insight that a theorem-proving procedure for first order logic could be based on not merely finding complementary literals by unification , but also then eliminating them—what he called “resolution”—that revolutionized the field [42]. Anyone interested in tracing the history might notice that whereas Robinson’s [42] does not refer to my [4], his earlier [41] does and in its content clearly shows its influence.
- 31.
The example worked out in [4] shows unification in action.
- 32.
[6].
- 33.
[8].
- 34.
- 35.
[35].
- 36.
Actually, as I remember it, we worked on that article and the one on Hilbert’s tenth problem for which we received the Chauvenet prize pretty much at the same time. The one on nonstandard analysis appeared in 1972 [25], a year before the prize-winning article.
- 37.
[12].
- 38.
- 39.
- 40.
[38].
- 41.
These fellowships are administered by the CIES, the same office that manages Fullbright awards.
References
Davis, M. (1956). A note on universal turing machines. Automata Studies. In C.E. Shannon & J. McCarthy (Eds.), Annals of Mathematics Studies (pp. 167–175). Princeton University Press
Davis, M. (1957). The definition of universal turing machine. Proceedings of the American Mathematical Society, 8, 1125–1126.
Davis, M. (1958). Computability and unsolvability. New York: McGraw-Hill. (Reprinted with an additional appendix, Dover 1983)
Davis, M. (1963). Eliminating the irrelevant from mechanical proofs. Proceedings of Symposia in Applied Mathematics, 15, 15–30. (Reprinted from [43], pp. 315–330).
Davis, M. (1963). Extensions and corollaries of recent work on Hilbert’s tenth problem. Illinois Journal of Mathematics, 7, 246–250.
Davis, M. (Ed.). (1965). The undecidable. Raven Press. (Reprinted from Dover 2004).
Davis, M. (1967). First course in functional analysis. Gordon and Breach. (Reprinted from Dover 2013).
Davis, M. (1968). One equation to rule them all. Transactions of the New York Academy of Sciences, Sec., II(30), 766–773.
Davis, M. (1971). An explicit Diophantine definition of the exponential function. Communications on Pure and Applied Mathematics, 24, 137–145.
Davis, M. (1972). On the number of solutions of Diophantine equations. Proceedings of the American Mathematical Society, 35, 552–554.
Davis, M. (1973). Hilbert’s tenth problem is unsolvable. American Mathematical Monthly, 80, 233–269. (Reprinted as an appendix to the Dover edition of [3]).
Davis, M. (1977). Applied nonstandard analysis. Interscience-Wiley. (Reprinted from Dover 2005).
Davis, M. (1977). A relativity principle in quantum mechanics. International Journal of Theoretical Physics, 16, 867–874.
Davis, M. (1980). The mathematics of non-monotonic reasoning. Artificial Intelligence, 13, 73–80.
Davis, M. (1981). Obvious logical inferences. In Proceedings of the Seventh Joint International Congress on Artificial Intelligence (pp. 530–531).
Davis, M. (1982). Why Gödel didn’t have Church’s thesis. Information and Control, 54, 3–24.
Davis, M. (1983). The prehistory and early history of automated deduction. In J. Siekmann & G. Wrightson (Eds.), Automation of reasoning (Vol. 1, pp. 1–28). Springer.
Davis, M. (1987). Mathematical logic and the origin of modern computers. Studies in the History of Mathematics, pp. 137–165. Mathematical Association of America. (Reprinted from The universal turing machine—a half-century survey, pp. 149–174, by R. Herken, Ed., 1988, Hamburg, Berlin: Verlag Kemmerer & Unverzagt, Oxford University Press.)
Davis, M. (1988). Influences of mathematical logic on computer science. In R. Herken (Ed.), The universal turing machine–a half-century survey (pp. 315–326). Hamburg, Berlin: Verlag Kemmerer & Unverzagt, Oxford University Press.
Davis, M. (1989). Emil post’s contributions to computer science. In Proceedings Fourth Annual Symposium (Ed.), on Logic in Computer Science (pp. 134–136). Washington, D.C.: IEEE Computer Society Press.
Davis, M. (1995). American logic in the 1920s. Bulletin of Symbolic Logic, 1, 273–278.
Davis, M. (1999). From logic to computer science and back. In C. S. Calude (Ed.), People and ideas in theoretical computer science (pp. 53–85). Springer.
Davis, M. (2000). The universal computer: The road from Leibniz to Turing. W.W. Norton. Turing Centenary Edition, CRC Press, Taylor & Francis 2012.
Davis, M. (2001). Engines of logic: Mathematicians and the origin of the computer. W.W. Norton. [Paperpack edition of The Universal Computer]
Davis, M., & Hersh, R. (1972). Nonstandard analysis. Scientific American, 226, 78–86.
Davis, M., & Hersh, R. (1973). Hilbert’s tenth problem. Scientific American, 229, 84–91 (Reprinted in J.C. Abbott (Ed.), The Chauvenet papers , 2, 555–571. Math. Assoc. America, 1978).
Davis, M., & Putnam, H. (1958). Reductions of Hilbert’s tenth problem. Journal of Symbolic Logic, 23, 183–187.
Davis, M., & Putnam, H. (1960). A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7, 201–215. (Reprinted from [43], pp. 125–139).
Davis, M., & Putnam, H. (1963). Diophantine sets over polynomial rings. Illinois Journal of Mathematics, 7, 251–255.
Davis, M., & Weyuker, E. J. (1983). Computability, complexity, and languages. Second edition with Ron Sigal: Academic Press. 1994.
Davis, M., & Weyuker, E. J. (1983). A formal notion of program-based test data adequacy. Information and Control, 56, 52–71.
Davis, M., & Weyuker, E. J. (1988). Metric space based test data adequacy criteria. The Computer Journal, 31, 17–24.
Davis, M., Putnam, H., & Robinson, J. (1961). The decision problem for exponential Diophantine equations. Annals of Mathematics, 74, 425–436.
Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem proving. Communications of the Association for Computing Machinery, 5, 394–397. (Reprinted from [43], pp. 267–270).
Davis, M., Matijasevic, Y., & Robinson, J. (1976). Hilbert’s tenth problem: Diophantine equations: positive aspects of a negative solution. Proceedings of Symposia in Pure Mathematics, 28, 323–378.
Green, B., & Tao, T. (2008). The primes contain arbitrarily long arithmetic progressions. Annals of Mathematics, 167, 481–547.
Kleene, S. C. (1943). Recursive predicates and quantifiers. Transactions of the American Mathematical Society, 53, 41–73. (Reprinted from [11], pp. 254–287).
Post, E. L. (1994). Solvability, provability, definability: The collected works of Emil L. Post ed. by M. Davis with a biographical introduction. Boston, Basel and Berlin: Birkhäuser
Prawitz, D. (1960). An improved proof procedure. (Reprinted from [43] with an additional comment by the author, pp. 162–201).
Reid, C. (1996). Julia: A life in mathematics. Washington, D.C.: Mathematical Association of America.
Robinson, J. A. (1963). Theorem proving on the computer. Journal of the Association for Computing Machinery, 10. (Reprinted from [43], pp. 372–383).
Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12. (Reprinted from [43], pp. 397–415).
Siekmann, J., & Wrightson, G. (Eds.). (1983). Automation of reasoning 1: Classical papers on computational logic 1957–1966. Berlin: Springer.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Davis, M. (2016). My Life as a Logician. In: Omodeo, E., Policriti, A. (eds) Martin Davis on Computability, Computational Logic, and Mathematical Foundations. Outstanding Contributions to Logic, vol 10. Springer, Cham. https://doi.org/10.1007/978-3-319-41842-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-41842-1_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-41841-4
Online ISBN: 978-3-319-41842-1
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)