Seminaire Philmath du 17 avril 2023
Lundi 17 avril 2023, 17h-19h, salle des conférences de l’IHPST, 13 rue du Four, 75006 PARIS
(University of Calgary)
Titre : The pre-history of automated reasoning
Automated theorem proving started around 1960 with the almost simultaneous proposal and implementation of several proof search and refutation algorithms which are still used today. These algorithms were based on the work of logicians working on Hilbert’s program, especially Bernays, Herbrand, and Gentzen. Strikingly, most of the theoretical groundwork for automated theorem proving was laid in the 1950s by analytic philosophers. The talk will focus on Alan Robinson’s resolution proof system and its influences found in the work of W. V. O. Quine, Burton Dreben, Martin Davis & Hilary Putnam, and Bernard Symonds & Roderick Chisholm.
Lien Zoom : https://pantheonsorbonne.zoom.us/j/99346835483?pwd=SWJIN01sWHBscDJsbUFtcFNqMmtNdz09
ID : 993 4683 5483