Martin Davis (mathematician)
- Davis–Putnam algorithm
- DPLL algorithm
- Work on Hilbert's tenth problem
- Bell Labs
- RAND Corporation
- New York University
- University of California, Berkeley
- Moshe Koppel
- Donald W. Loveland
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.[1][2] 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.[3] His doctoral dissertation, entitled On the Theory of Recursive Unsolvability, was supervised by American mathematician and computer scientist Alonzo Church.[1][2][4]
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.[1] He later worked at Bell Labs and the RAND Corporation before joining New York University.[1] During his time at the NYU, he helped set up the university's computer science department. He retired from NYU in 1996.[3][1] He was later a member of visiting faculty at University of California, Berkeley.[5]
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?[1] 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.[1] 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".[6]
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.[7] The algorithm was a refinement of the earlier Davis–Putnam algorithm, which was a resolution-based procedure developed by Davis and Putnam in 1960.[8][9] The algorithm is foundational in the architecture of fast Boolean satisfiability solvers.[6]
In addition to his work on computability theory, Davis also made significant contributions to the fields of computational complexity and mathematical logic.[1][6][10] Davis was also known for his model of Post–Turing machines.[3]
In 1974, Davis won the Lester R. Ford Award for his expository writing related to his work on Hilbert's tenth problem,[2][11] and in 1975 he won the Leroy P. Steele Prize and the Chauvenet Prize (with Reuben Hersh).[12] He became a fellow of the American Academy of Arts and Sciences in 1982,[2] and in 2013, he was selected as one of the inaugural fellows of the American Mathematical Society.[13]
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 starting including works of Gottfried Wilhelm Leibniz and Alan Turing.[1] His book The Undecidable, the first edition of which was published in 1965, was a collection of unsolvable problems and computable functions.[6]
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.[14]: 8 They had two children.[3] The couple lived in Berkeley, California, after his retirement.[1]
Davis died on January 1, 2023, at age 94.[15] His wife died the same day several hours later.[16]
Selected publications
Books
- Davis, Martin (1958). Computability and Unsolvability. New York: Dover. ISBN 0-486-61471-9. Dover reprint
- Davis, Martin (1977). Applied nonstandard analysis. New York: Wiley. ISBN 9780471198970. 2014 Dover reprint
- Davis, Martin; Weyuker, Elaine J.; Sigal, Ron (1994). Computability, complexity, and languages: fundamentals of theoretical computer science (2nd ed.). Boston: Academic Press, Harcourt, Brace. ISBN 9780122063824.
- Davis, Martin (2000). The Universal Computer: The Road from Leibniz to Turing. Norton. ISBN 0393047857. Reprinted as Engines of Logic: Mathematicians and the Origin of the Computer. New York: Norton. 2000. ISBN 9780393322293.
- Davis, Martin (2004). The Undecidable : Basic papers on undecidable propositions, unsolvable problems and computable functions. New York: Dover Publications. ISBN 0-486-43228-9. OCLC 53840050.
Articles
- Davis, Martin (1973), "Hilbert's Tenth Problem is Unsolvable", The American Mathematical Monthly, 80(3), 233–269. doi:10.1080/00029890.1973.11993265.
- 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. doi:10.1007/978-3-030-48006-6_8.
See also
References
- ^ a b c d e f g h i j Jackson, Allyn (September 2007), "Interview with Martin Davis" (PDF), Notices of the American Mathematical Society, vol. 55, no. 5, Providence, Rhode Island: American Mathematical Society (published May 2008), pp. 560–571, ISSN 0002-9920, OCLC 1480366.
- ^ a b c d O'Connor, John J.; Robertson, Edmund F., "Martin Davis (mathematician)", MacTutor History of Mathematics Archive, University of St Andrews
- ^ a b c d "Martin Davis – Biography". Maths History. Retrieved January 8, 2023.
- ^ Martin Davis at the Mathematics Genealogy Project
- ^ "Martin Davis | Department of Mathematics at University of California Berkeley". math.berkeley.edu. Retrieved January 8, 2023.
- ^ a b c d Martin Davis on Computability, Computational Logic, and Mathematical Foundations. Outstanding Contributions to Logic. Vol. 10. 2016. doi:10.1007/978-3-319-41842-1. ISBN 978-3-319-41841-4.
- ^ "Computer Science – University of Texas CS395T, Spring 2011" (PDF).
- ^ "Davis–Putnam algorithm". hellenicaworld.com. Retrieved January 8, 2023.
- ^ "DPLL algorithm – Learning Logic for Computer Science". logic4free.informatik.uni-kiel.de. Retrieved January 8, 2023.
- ^ "New and Noteworthy Titles on Our Bookshelf" (PDF). American Mathematical Society - Notices of the AMS. December 1, 2017. p. 1327. Retrieved January 7, 2023.
- ^ Davis, Martin (1973). "Hilbert's tenth problem is unsolvable". Amer. Math. Monthly. 80 (3): 233–269. doi:10.2307/2318447. JSTOR 2318447.
- ^ Davis, Martin; Hersh, Reuben (1973). "Hilbert's 10th Problem". Scientific American. 229 (5). Springer Science and Business Media LLC: 84–91. Bibcode:1973SciAm.229e..84D. doi:10.1038/scientificamerican1173-84. ISSN 0036-8733.
- ^ List of Fellows of the American Mathematical Society. Retrieved March 17, 2014.
- ^ Omodeo, E. G., & Policriti, A., eds., Martin Davis on Computability, Computational Logic, and Mathematical Foundations (Berlin/Heidelberg: Springer, 2016), p. 8.
- ^ "Martin David Davis". Harris Funeral Home. Retrieved January 4, 2023.
- ^ "Remembering Martin and Virginia Davis". Retrieved January 8, 2023.
External links
- 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)
- Martin Davis: Universality is Ubiquitous (Princeton Academics) on YouTube
- "In Memory of Martin Davis" (PDF). Notices of the American Mathematical Society. 71 (7): 898–907. August 2024. doi:10.1090/noti2982.
- v
- t
- e
- 1925 G. A. Bliss
- 1929 T. H. Hildebrandt
- 1932 G. H. Hardy
- 1935 Dunham Jackson
- 1938 G. T. Whyburn
- 1941 Saunders Mac Lane
- 1944 R. H. Cameron
- 1947 Paul Halmos
- 1950 Mark Kac
- 1953 E. J. McShane
- 1956 Richard H. Bruck
- 1960 Cornelius Lanczos
- 1963 Philip J. Davis
- 1964 Leon Henkin
- 1965 Jack K. Hale and Joseph P. LaSalle
- 1967 Guido Weiss
- 1968 Mark Kac
- 1970 Shiing-Shen Chern
- 1971 Norman Levinson
- 1972 François Trèves
- 1973 Carl D. Olds
- 1974 Peter D. Lax
- 1975 Martin Davis and Reuben Hersh
- 1976 Lawrence Zalcman
- 1977 W. Gilbert Strang
- 1978 Shreeram S. Abhyankar
- 1979 Neil J. A. Sloane
- 1980 Heinz Bauer
- 1981 Kenneth I. Gross
- 1982 No award given.
- 1983 No award given.
- 1984 R. Arthur Knoebel
- 1985 Carl Pomerance
- 1986 George Miel
- 1987 James H. Wilkinson
- 1988 Stephen Smale
- 1989 Jacob Korevaar
- 1990 David Allen Hoffman
- 1991 W. B. Raymond Lickorish and Kenneth C. Millett
- 1992 Steven G. Krantz
- 1993 David H. Bailey, Jonathan M. Borwein and Peter B. Borwein
- 1994 Barry Mazur
- 1995 Donald G. Saari
- 1996 Joan Birman
- 1997 Tom Hawkins
- 1998 Alan Edelman and Eric Kostlan
- 1999 Michael I. Rosen
- 2000 Don Zagier
- 2001 Carolyn S. Gordon and David L. Webb
- 2002 Ellen Gethner, Stan Wagon, and Brian Wick
- 2003 Thomas C. Hales
- 2004 Edward B. Burger
- 2005 John Stillwell
- 2006 Florian Pfender & Günter M. Ziegler
- 2007 Andrew J. Simoson
- 2008 Andrew Granville
- 2009 Harold P. Boas
- 2010 Brian J. McCartin
- 2011 Bjorn Poonen
- 2012 Dennis DeTurck, Herman Gluck, Daniel Pomerleano & David Shea Vela-Vick
- 2013 Robert Ghrist
- 2014 Ravi Vakil
- 2015 Dana Mackenzie
- 2016 Susan H. Marshall & Donald R. Smith
- 2017 Mark Schilling
- 2018 Daniel J. Velleman
- 2019 Tom Leinster
- 2020 Vladimir Pozdnyakov & J. Michael Steele
- 2021 Travis Kowalski
- 2022 William Dunham, Ezra Brown & Matthew Crawford
- 2023 Kimmo Eriksson & Jonas Eliasson
- 2024 Jeffrey Whitmer