Martin Davis

Martin David Davis (March 8, 1928 – January 1, 2023) was an American mathematician and computer scientist who contributed to the fields of computability theory and mathematical logic. His work on Hilbert's tenth problem led to the MRDP theorem. He also advanced the Post–Turing model and co-developed the Davis–Putnam–Logemann–Loveland (DPLL) algorithm, which is foundational for Boolean satisfiability solvers.

Davis won the Leroy P. Steele Prize, the Chauvenet Prize (with Reuben Hersh), and the Lester R. Ford Award. He was a fellow of the American Academy of Arts and Sciences and a fellow of the American Mathematical Society.

Early life and education Davis's parents were Jewish immigrants to the United States from Łódź, Poland , and married after they met again in New York City. Davis was born in New York City on March 8, 1928. He grew up in the Bronx, where his parents encouraged him to obtain a full education. He graduated from the prestigious Bronx High School of Science in 1944 and went on to receive his bachelor's degree in mathematics from City College in 1948 and his PhD from Princeton University in 1950. His doctoral dissertation, entitled On the Theory of Recursive Unsolvability, was supervised by American mathematician and computer scientist Alonzo Church.

Academic career During a research instructorship at the University of Illinois at Urbana-Champaign in the early 1950s, he joined the Control Systems Lab and became one of the early programmers of the ORDVAC.

Hilbert's tenth problem

Davis first worked on Hilbert's tenth problem during his PhD dissertation, working with Alonzo Church. The theorem, as posed by the German mathematician David Hilbert, asks a question: given a Diophantine equation, is there an algorithm that can decide if the equation is solvable?

Other contributions Davis collaborated with Putnam, George Logemann, and Donald W. Loveland in 1961 to introduce the Davis–Putnam–Logemann–Loveland (DPLL) algorithm, which was a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e., for solving the CNF-SAT problem. The algorithm was a refinement of the earlier Davis–Putnam algorithm, which was a resolution-based procedure developed by Davis and Putnam in 1960. The algorithm is foundational in the architecture of fast Boolean satisfiability solvers. Davis was also known for his model of Post–Turing machines. and in 1975 he won the Leroy P. Steele Prize and the Chauvenet Prize (with Reuben Hersh). He became a fellow of the American Academy of Arts and Sciences in 1982,

Davis's 1958 book Computability and Unsolvability is considered a classic in theoretical computer science, while his 2000 book The Universal Computer traces the evolution and history of computing, from Gottfried Wilhelm Leibniz to Alan Turing. They had two children. His wife died the same day several hours later.

Selected publications Books Dover reprint 2014 Dover reprint

Reprinted as

Articles Davis, Martin (1973), "Hilbert's Tenth Problem is Unsolvable", The American Mathematical Monthly, 80(3), 233–269. . Davis, Martin (1995), "Is Mathematical Insight Algorithmic?", Behavioral and Brain Sciences, 13(4), 659–60. Davis, Martin (2020), "Seventy Years of Computer Science", In: Blass A., Cégielski P., Dershowitz N., Droste M., Finkbeiner B. (eds.) Fields of Logic and Computation III, 105–117. Lecture Notes in Computer Science, vol. 12180. Springer: Cham, Switzerland. .