Martin Davis (mathematician)

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.<ref name="jackson">Template:Citation.</ref><ref name="mactutor">Template:MacTutor Biography</ref> 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.<ref name=":0">Template:Cite web</ref> His doctoral dissertation, entitled On the Theory of Recursive Unsolvability, was supervised by American mathematician and computer scientist Alonzo Church.<ref name="jackson" /><ref name="mactutor" /><ref>Template:MathGenealogy</ref>

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.<ref name="jackson" /> He later worked at Bell Labs and the RAND Corporation before joining New York University.<ref name="jackson"/> During his time at the NYU, he helped set up the university's computer science department. He retired from NYU in 1996.<ref name=":0" /><ref name="jackson"/> He was later a member of visiting faculty at University of California, Berkeley.<ref>Template:Cite web</ref>

Hilbert's tenth problem

Template:Further 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?<ref name="jackson"/> Davis's dissertation put forward a conjecture that the problem was unsolvable. In the 1950s and 1960s, Davis, along with American mathematicians Hilary Putnam and Julia Robinson, made progress toward solving this conjecture. The proof of the conjecture was finally completed in 1970 with the work of Russian mathematician Yuri Matiyasevich. This resulted in the MRDP or the DPRM theorem, named for Davis, Putnam, Robinson, and Matiyasevich.<ref name="jackson"/> Describing the problem, Davis had earlier mentioned that he found the problem "irresistibly seductive" when he was an undergraduate and later had progressively become his "lifelong obsession".<ref name=":2">Template:Cite book</ref>

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.<ref>Template:Cite web</ref> The algorithm was a refinement of the earlier Davis–Putnam algorithm, which was a resolution-based procedure developed by Davis and Putnam in 1960.<ref>Template:Cite web</ref><ref>Template:Cite web</ref> The algorithm is foundational in the architecture of fast Boolean satisfiability solvers.<ref name=":2"/>

In addition to his work on computability theory, Davis also made significant contributions to the fields of computational complexity and mathematical logic.<ref name="jackson"/><ref name=":2"/><ref>Template:Cite news</ref> Davis was also known for his model of Post–Turing machines.<ref name=":0" />

In 1974, Davis won the Lester R. Ford Award for his expository writing related to his work on Hilbert's tenth problem,<ref name="mactutor" /><ref>Template:Cite journal</ref> and in 1975 he won the Leroy P. Steele Prize and the Chauvenet Prize (with Reuben Hersh).<ref name="Davis Hersh Hilbert 10th">Template:Cite journal</ref> He became a fellow of the American Academy of Arts and Sciences in 1982,<ref name="mactutor"/> and in 2013, he was selected as one of the inaugural fellows of the American Mathematical Society.<ref>List of Fellows of the American Mathematical Society. Retrieved March 17, 2014.</ref>

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.<ref name="jackson"/> His book The Undecidable, the first edition of which was published in 1965, was a collection of unsolvable problems and computable functions.<ref name=":2"/>

Personal life and death

Davis was married to Virginia Whiteford Palmer, a textile artist. The couple met during their time in the Urbana–Champaign area and subsequently married in 1951.<ref>Omodeo, E. G., & Policriti, A., eds., Martin Davis on Computability, Computational Logic, and Mathematical Foundations (Berlin/Heidelberg: Springer, 2016), p. 8.</ref>Template:Rp They had two children.<ref name=":0" /> The couple lived in Berkeley, California, after his retirement.<ref name="jackson"/>

Davis died on January 1, 2023, at age 94.<ref>Template:Cite web</ref> His wife died the same day several hours later.<ref>Template:Cite web</ref>

Selected publications

Books

• Template:Cite book Dover reprint
• Template:Cite book 2014 Dover reprint
• Template:Cite book
• Template:Cite book Reprinted as Template:Cite book
• Template:Cite book

Articles

• Davis, Martin (1973), "Hilbert's Tenth Problem is Unsolvable", The American Mathematical Monthly, 80(3), 233–269. {{#invoke:CS1 identifiers|main|_template=doi}}.
• 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. {{#invoke:CS1 identifiers|main|_template=doi}}.

See also

• Criticism of non-standard analysis
• Halting problem
• Influence of non-standard analysis

External links

• Template:Official website
• Celebrating Emil Post & His "Intractable Problem" of Tag: 100 Years Later on YouTube, including contributions by Martin Davis (from 1 hour 39 minutes in the recording)
• Template:YouTube
• Template:Cite journal