Martin Davis memoriam

[Sam Buss]

An earlier FOM posting of the memoriam for Martin Davis failed to go
through since attachments are not allowed in FOM messages. A plain text
version is below.  It can also be seen online at
https://logicprogramming.org/2023/01/in-memoriam-martin-davis/.

Sam Buss
---

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

Martin Davis (March 8, 1928-January 1, 2023) and her 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".
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20230106/a62770be/attachment-0001.html>