报告题目：Automation in interactive theorem proving
主讲：Dr BoHua Zhan
日期：2017 年6 月12日 (周一)
时间：下午14:30 – 17:00
地点：jbo竞博电竞官方网站东校区学院楼A201
主持：万海 副教授
摘要:
Interactive theorem proving involves using proof assistants to verify, with human guidance, proofs of either mathematical theorems or correctness of computer programs. One of the major difficulties in interactive theorem proving is the length and complexity of proof scripts needed to verify deep theorems or long computer programs. These scripts take significant effort and expertise to write and maintain, limiting the depth of results that can be verified economically. Simplifying the proof script requires improvements in proof automation, which means having the computer automatically generate the "routine" parts of the proof.
In this talk, I will give a brief overview of interactive theorem proving, with a focus on automation techniques. I will then discuss my own work on a new heuristic theorem prover called auto2 for the proof assistant Isabelle. The auto2 prover can be considered as a mixture of existing approaches based on tactics and the use of external first-order logic solvers, taking the advantages and avoiding the disadvantages of each approach. It has been used to verify large amounts of mathematics from the foundations, as well as the correctness of functional and imperative implementations of algorithms and data structures.
报告人简介:
Dr. Bohua Zhan is currently an Instructor and postdoctoral fellow at the Massachusetts Institute of Technology. He received his Bachelor's degree from MIT in 2010 and PhD in mathematics from Princeton University in 2014. While in graduate school, he worked on low dimensional topology, in particular algorithms for computing invariants of knots and 3-dimensional manifolds. More recently he is working on automation in interactive theorem proving, in particular as the author of the auto2 prover in Isabelle.