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. His book
The Undecidable, the first edition of which was published in 1965, was a collection of
unsolvable problems and
computable functions. == Personal life and death ==