Martin Davis (mathematician)

Davis's parents were Jewish immigrants to the United States from Łódź, Poland, and married after they met again in New York City.

[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.

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.

[6] 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.

[1] His book The Undecidable, the first edition of which was published in 1965, was a collection of unsolvable problems and computable functions.