Logic List Mailing Archive

Martin Davis (1928-2023)

Martin Davis (1928-2023)
https://logicprogramming.org/2023/01/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 the Americas, Europe, and 
Asia.

Martin's mentor at the City College of New York was Emil Leon Post, and his PhD 
advisor at 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. Shortly 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".
--
[LOGIC] mailing list
http://www.dvmlg.de/mailingliste.html
Archive: http://www.illc.uva.nl/LogicList/

provided by a collaboration of the DVMLG, the Maths Departments in Bonn and Hamburg, and the ILLC at the Universiteit van Amsterdam