(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.