(2017.06.19 14:00pm N202)Bohua Zhan:Automation in interactive theorem proving

Time:2017-06-16  Source:KLMM

Title                Automation in interactive theorem proving

Speaker          Bohua Zhan (MIT, USA)

Time&Venue 2017.06.19  14:00pm  N202

Abstract:             Interactive theorem proving involves using proof assistants to verify, with human guidance, proofs of either mathematical theorems or correctness of computer programs. In this talk, I will give a brief overview of the history of this field, with an emphasis on automation techniques. I will then discuss my own work on a new heuristic theorem prover called auto2 for the proof assistant Isabelle.