slideshow 3

Logic seminar

Interactive theorem proving for the working logician

Jeremy Avigad
Carnegie Mellon University

 

Monday, 7. December 2020 - 15:30 to 17:00
Zoom meeting 472 648 284 - https://cesnet.zoom.us/j/472648284 - contact thapen@math.cas.cz to join
Over the last few decades, computational proof assistants have made it possible to construct formal axiomatic derivations of increasing complexity. They are now used to verify that hardware and software designs meet their specifications, as well as to verify the correctness of mathematical proofs. The practice has taken root and promises to play an important role in mathematics and computer science.

In this talk, I will survey the technology, with an emphasis on formal mathematics. I will then discuss aspects of interactive theorem proving that may be of interest to the working logician, and places where a better theoretical understanding can lead to progress. Specifically, I'll discuss the need for practical foundations, search procedures, decision procedures, and proof systems.