In Memory of Martin Davis

TL;DR

Martin Davis's lifelong work spans computability, Hilbert's Tenth Problem, and automated reasoning. The paper surveys his core contributions, including the hyperarithmetical hierarchy up to ordinals $< \omega^2$, computably enumerable sets, and the universal Turing machine, as well as the Davis–Putnam–Robinson–Matiyasevich solution showing there is no algorithm to decide solvability of Diophantine equations over $\mathbb{Z}$. It also reviews his pivotal role in automated reasoning, from Presburger arithmetic on the JOHNIAC to the DPLL-based propositional provers and proof-verification research. Beyond results, it highlights his influence on establishing computability theory as a distinct mathematical field and his mentorship and advocacy for formal methods.

Abstract

The present paper gives an account for the general mathematical reader of the life and work of Martin Davis. Since two rather comprehensive autobiographical accounts and two long biographical interviews already exist, the present work focusses on Davis's scientific achievements, including work on computably enumerable sets, universal Turing machines, the hyperarithmetical hierarchy, neural networks, Hilbert's Tenth Problem, and automated reasoning.

Figures (11)

• Figure 1: Martin in the late 1940s. (Courtesy of his son Harold Davis)
• Figure 2: Martin, middle, with his friends Jacob T. and Judith Schwartz. (Courtesy of Diana Robinson Schwartz)
• Figure 3: Martin ready to give an answer, late 1990s. (Courtesy of Domenico Cantone)
• Figure 4: Martin and his wife Virginia as grandparents, holding Katie Rose. (Courtesy of Harold Davis)
• Figure 5: Julia Robinson announces the possibility of getting rid of the hypothesis made by Davis and Putnam. (Courtesy of Harold Davis)