Special Event In Memory of Martin Davis

Time and Location:

Speaker:

Martin Davis advanced our understanding of the connections across mathematical foundations, computing, and unsolvability. Over twenty authors contributed—and many others would have happily done so—to the book devoted to his outstanding contributions to logic, testifying to the multifaceted nature of his intellectual élan. Solving Hilbert’s Tenth Problem (a major 20th century achievement towards which Martin made decisive steps) likewise called for an interplay of disciplines: number theory, computability, symbolic logic.

This talk will seek to highlight the unitary vision linking Martin’s results in various realms of theoretical computer science, leading him from his early passionate interest in the foundations of real analysis to his landmark writings on computability, unsolvable problems, computational logic, non-standard analysis, and the history of computing.

Particular focus will be put on the role that Martin has played as a pioneer of the field today known as ‘automated reasoning’ in collaboration with the distinguished philosopher Hilary Putnam with whom Martin enjoyed discussing “all day long about everything under the sun”. The Davis-Putnam-Logemann-Loveland procedure, still fundamental in the architecture of fast Boolean satisfiability solvers, was first implemented in 1961; shortly afterwards, a general-purpose theorem-proving system based on a method devised by Martin was implemented at Bell Labs in Murray Hills. Martin also coined some of the terminology that has become standard in the automated reasoning field.

Anil Nerode, who met Martin in 1957 at a gathering that “precipitated the formation of an international research community · · · whose influence on logic and computer science is strong even after sixty years”, recalls: “What I learned then about Martin was the universality of his interests, his utter concentration on fundamental problems, and his insatiable urge to learn new things. These are the signal marks of his long career.”

Speaker Bio: Eugenio G. Omodeo is Senior Scholar in the Department of Mathematics and Earth Sciences at the University of Trieste (Italy), where he served as full professor of Computer Science from 2004 to 2020. He received a degree in Mathematics in 1975 at the University of Padova, then Master of Science and PhD degrees in Computer Science at New York University in 1979 and 1984, where his supervisor was Martin Davis. From 1981 to 1989, he was employed by companies belonging to ENI, the National Hydrocarbon Company of Italy, where he became coordinator of R&D activities of Enidata in the area of Advanced Information Processing. His team took part in several Esprit projects funded by the European Commission. He then became a professor and worked for several Italian Universities (Udine, “La Sapienza” of Rome, Salerno, L’Aquila, Trieste) before entering retirement in 2020. His scientific publications include 4 monographs, over 60 articles and 40 contributions to conference proceedings. Main fields of interest: Automated reasoning, Computational logic, Proof verification, Computable set theory.