Logic seminar
Interactive theorem proving for the working logician
Carnegie Mellon University
Monday, 7. December 2020 - 15:30 to 17:00
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.
published by Neil Thapen on Wed, 18/11/2020 - 10:33