Martin Davis | |
|---|---|
 Davis in 1996 | |
| Born | Martin David Davis (1928-03-08)March 8, 1928 New York City, U.S. |
| Died | January 1, 2023(2023-01-01) (aged 94) Berkeley, California, U.S. |
| Alma mater | City College of New York (AB) Princeton University (PhD) |
| Known for | |
| Spouse | |
| Awards | Chauvenet Prize (1975) |
| Scientific career | |
| Institutions | |
| Thesis | On the Theory of Recursive Unsolvability (1950) |
| Doctoral advisor | Alonzo Church |
| Doctoral students | |
Martin David Davis (March 8, 1928 – January 1, 2023) was an American mathematician andcomputer scientist who contributed to the fields ofcomputability theory andmathematical logic. His work onHilbert's tenth problem led to theMRDP theorem. He also advanced thePost–Turing model and co-developed theDavis–Putnam–Logemann–Loveland (DPLL) algorithm, which is foundational forBoolean satisfiability solvers.
Davis won theLeroy P. Steele Prize, theChauvenet Prize (withReuben Hersh), and theLester R. Ford Award. He was a fellow of theAmerican Academy of Arts and Sciences and a fellow of theAmerican Mathematical Society.
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 theBronx, 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 fromCity College in 1948 and his PhD fromPrinceton University in 1950.[3] His doctoral dissertation, entitledOn the Theory of Recursive Unsolvability, was supervised by American mathematician and computer scientistAlonzo Church.[1][2][4]
During a research instructorship at theUniversity of Illinois at Urbana-Champaign in the early 1950s, he joined theControl Systems Lab and became one of the early programmers of theORDVAC.[1] He later worked atBell Labs and theRAND Corporation before joiningNew 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 atUniversity of California, Berkeley.[5]
Davis first worked on Hilbert's tenth problem during his PhD dissertation, working with Alonzo Church. The theorem, as posed by the German mathematicianDavid Hilbert, asks a question: given aDiophantine 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 mathematiciansHilary Putnam andJulia Robinson, made progress toward solving this conjecture. The proof of the conjecture was finally completed in 1970 with the work of Russian mathematicianYuri Matiyasevich. This resulted in theMRDP 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]
Davis collaborated with Putnam,George Logemann, andDonald W. Loveland in 1961 to introduce theDavis–Putnam–Logemann–Loveland (DPLL) algorithm, which was acomplete,backtracking-basedsearch algorithm fordeciding the satisfiability ofpropositional logic formulae inconjunctive normal form, i.e., for solving theCNF-SAT problem.[7] The algorithm was a refinement of the earlierDavis–Putnam algorithm, which was aresolution-based procedure developed by Davis and Putnam in 1960.[8][9] The algorithm is foundational in the architecture of fastBoolean satisfiability solvers.[6]
In addition to his work oncomputability theory, Davis also made significant contributions to the fields ofcomputational complexity andmathematical logic.[1][6][10] Davis was also known for his model ofPost–Turing machines.[3]
In 1974, Davis won theLester R. Ford Award for his expository writing related to his work on Hilbert's tenth problem,[2][11] and in 1975 he won theLeroy P. Steele Prize and theChauvenet Prize (withReuben Hersh).[12] He became afellow of theAmerican Academy of Arts and Sciences in 1982,[2] and in 2013, he was selected as one of the inaugural fellows of theAmerican Mathematical Society.[13]
Davis's 1958 bookComputability and Unsolvability is considered a classic intheoretical computer science, while his 2000 bookThe Universal Computer traces the evolution and history of computing, fromGottfried Wilhelm Leibniz toAlan Turing.[1] His bookThe Undecidable, the first edition of which was published in 1965, was a collection ofunsolvable problems andcomputable functions.[6]
Davis was married to Virginia Whiteford Palmer, a textile artist. The couple met during their time in theUrbana–Champaign area and subsequently married in 1951.[14]: 8 They had two children.[3] The couple lived inBerkeley, 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]
Books
Articles
| International | |
|---|---|
| National | |
| Academics | |
| People | |
| Other | |