In memoriam: Martin Davis

By Eugenio Omodeo and Alberto Policriti with a foreword by Domenico Cantone.

Martin Davis (March 8, 1928-January 1, 2023) and his beloved wife Virginia passed away yesterday. They had been married for over 71 years. Martin was one of the fathers of Computability, to which he contributed with a model of Post–Turing machines and with basic work on Hilbert’s tenth problem concerning integral solutions to Diophantine equations that led to the Davis-Matiyasevich-Putnam-Robinson theorem stating the algorithmic unsolvability of that problem. Martin was also the co-inventor of the Davis–Putnam and the DPLL algorithms which determine the satisfiability of propositional formulas.

Martin David Davis, born in the Bronx on March 8, 1928, emeritus professor at the New York University since 1996, an eminent logician and one of the boosters of the computability field, died on January 1, 2023 — a few hours later, also his wife Virginia passed away.

Martin made decisive steps towards a major 20th century achievement, namely the answer to ‘Hilbert’s tenth’, a problem lying at the intersection of computability, number theory and symbolic logic, which Martin rightly expected—on the footsteps of Post—to “beg for an unsolvability proof”.

Over the years, Martin’s scientific contributions have also spanned mathematical foundations, non-standard analysis, automated reasoning, and artificial intelligence; moreover, prompted by a keen interest in the history and philosophy of computing, he charted the path “from ideas and concepts developed by logicians, sometimes centuries ago, to their embodiment in software and hardware”.
Martin’s scientific monographs and his writings on the history of the universal computer have had a far-reaching influence. Martin has also been a deep-impact lecturer in many countries in Americas, Europe, and Asia.

Martin’s mentor at the City College of New York was Emil Leon Post, and his PhD advisor at the Princeton University was Alonzo Church. Martin’s PhD dissertation, defended in 1950, extended Kleene’s arithmetical hierarchy of sets into the constructive transfinite, thus capturing the hyperarithmetical sets; it also tackled the said Hilbert’s problem, H10, about the solvability of Diophantine equations in integers, and boldly stated the hypothesis (implying that H10 is algorithmically unsolvable) that every listable set of natural numbers is Diophantine. Martin’s first attempt to prove his hypothesis—which would be affirmatively settled twenty years later—consisted in devising a manner of describing listable sets (known as the Davis normal form) whose syntax went “tantalizing close” to a genuinely Diophantine specification.
Martin’s intimacy with the writings by Gödel, Church, Turing, Rosser, Kleene, Post (of which he curated an anthology published in 1965) on algorithmically unsolvable problems, made him an authoritative scholar on The Undecidable.

Martin contributed in several ways, through his research, teachings, and dissemination activity, to ensure that computability theory acquired the dignity of an independent discipline. While working with Claude Shannon at Bell Labs in the summer of 1953 he elicited the notion of universal Turing machine from extant implementations of it; a couple of decades later, he unified Post’s model with Turing’s model of computation. In the 1950s, Martin also programmed concrete computers (initially, ORDVAC and ILLIAC I)
and “began to see that Turing machines provided an abstract mathematical model of real-world computers”.
As early as 1954, Martin coded Presburger’s decision algorithm for integer arithmetic without multiplication on a JOHNNIAC, at the Institute for Advanced Study in Princeton: his program produced the first computer-generated mathematical proof. With this accomplishment, and with subsequent work on automatic theorem-proving for first-order quantification theory, he was a forerunner of computational logic. The Davis-Putnam-Logemann-Loveland procedure, to date so basic in the architecture of fast Boolean satisfiability solvers, was first implemented in 1961. Short after, without much emphasis on its relevance, a unification algorithm became a component of a general-purpose theorem-proving system named Linked Conjunct: this method was conceived by Martin and implemented at Bell Labs by a team which involved M. Douglas McIlroy. Some of the terminology which has gradually become standard in the area of automated theorem proving (the notion of ‘Herbrand universe’, to mention one entry) was introduced by Martin in those early years. Martin’s contributions to automated deduction are not limited to autonomous proving: while visiting John McCarthy’s AI lab at Stanford University in the late 1970s, he worked on proof-checking (he would then coauthor ‘Metamathematical extensibility for theorem verifiers
and proof-checkers’ with Jacob T. Schwartz) and addressed mathematical questions concerned with non-monotonic reasoning.

With Elaine J. Weyuker, in the 1980s, Martin worked on software testing, proposing criteria for program-based test data adequacy. H10 is a problem that Martin says he found “irresistibly seductive” when still an undergraduate. It became his “lifelong obsession” and, in association with Hilary Putnam and Julia Bowman Robinson, he gave a decisive push towards its (negative) solution. “It was in the summer of 1959”, Martin reports, that “Hilary and I really hit the jackpot”; this is when they proved the algorithmic unsolvability of a strengthened variant of H10, regarding exponential (instead of polynomial) Diophantine equations. This result, known as the Davis-Putnam-Robinson theorem, would evolve 10 years later into the sought theorem about the unsolvability of H10, dubbed DPRM, thanks to the definitive contribution of the Russian mathematician Yuri V. Matiyasevich.
Short before Matiyasevich’s breakthrough, which amounted to getting a polynomial Diophantine representation of an exponential-growth relation between natural numbers, Martin had tried in 1968 to achieve the same goal by a different approach: a specific quaternary quartic Diophantine equation—he found—would act as a ‘rule-them-all ’ equation (leading to an exponential-growth Diophantine relation and hence to a negative answer to H10) if it turned out to be finite-fold, i.e., to admit only a finite number of integer solutions. As of today, it is an open issue whether Martin’s equation, or any of a few other candidate rule-them-all equations constructed in conformity with his recipe, are finite-fold; should it turn out that this is the case, then every listable set would admit a finite-fold Diophantine representation. Another open challenge related to H10 is establishing whether the analogue of this problem regarding rational (instead of integer) solutions to Diophantine equations is algorithmically solvable; concerning this, in 2010 Martin indicated a path—little explored so far—that could possibly lead to a negative answer.
Martin proved in 1972 a broad-gauge corollary of the unsolvability of H10: for no nonempty set A of finite cardinal numbers, there exists an algorithm for testing, given any (multi-variate) polynomial P with integer coefficients, whether or not the number of distinct positive integer solutions to the equation P = 0 belongs to A. In a paper jointly written with Yuri Matiyasevich and Julia Robinson in 1976, Martin outlined a translation of the famous Riemann Hypothesis into the claim that a certain Diophantine equation has no solutions. Julia Robinson wrote to him “I like your reduction of RH immensely”. Yet Martin himself, in an interview given in 2008, so judges the equation he can reduce RH to: “This is an equation that only its mother could love”.
Various books written by Martin have become ‘classics’ and have been translated into various languages: ‘Computability and Unsolvability’ (1958), ‘A first course in functional analysis’ (1966), ‘Applied nonstandard analysis’ (1977), ‘Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science’ (with Ron Sigal and Elaine J. Weyuker, 1994), and ‘The Universal Computer: The Road from Leibniz to Turing’ (2000).
His ‘Lecture Notes in Logic’ (1993, Courant Inst. of Mathematical Sciences) are a true jewel.
Martin supervised 25 doctoral dissertations and has had at least 71 PhD descendants so far.

His honors and awards include: Lester R. Ford Prize, MAA (1974); Leroy P. Steele Prize, AMS (1975); Chauvenet Prize, MAA (with Reuben Hersch, 1975); Earle Raymond Hedrick Lecturer 1976, MAA; Fellow of the A.A.A.S. (January 1982); Guggenheim Foundation Fellowship 1983–84; Elected to Gamma Chapter, Phi Beta Kappa (1995); Townsend Harris medal (2001); Trjitzinski Memorial Lecturer, Univ. of Illinois (2001); Herbrand Award of the International Conference on Automated Deduction (2005); Pioneering Achievement Award from the ACM SIG on Design Automation (2009).
Anil Nerode, recalling the occasion when he first met Martin, in 1957, says: “What I learned then about Martin was the universality of his interests, his utter concentration on fundamental problems, and his insatiable urge to learn new things. These are the signal marks of his long career”.