题目：           Automation in interactive theorem proving

报告人：      Bohua Zhan (MIT, USA)

时间地点：   2017.06.19  14:00pm  N202

摘要：          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.