公共目录

您目前的位置: 首页» 公共目录» 学术活动

学术报告: Automation in Interactive Theorem Proving

      题: Automation in Interactive Theorem Proving

    人: 詹博华  博士后(慕尼黑工业大学)

      间: 2018.07.02,星期一,14:00-15:00

      首师大北二区教学楼小会议室

位:信息工程学院

主讲学者简介:

慕尼黑工业大学博士后。研究方向是交互式定理证明里的证明自动化,以及在形式化数学和程序验证里的应用。2014年从普林斯顿大学数学系获得博士学位。博士时期的研究方向是低维拓扑学。2014-2017在麻省理工学院数学系做博士后。现在研究方向的论文发表于ITP, TACAS, CADE会议。

 

 


内容介绍:

Interactive theorem proving involves using proof assistants to construct and verify formal proofs of mathematical theorems. It can be applied to verify results in both mathematics and computer science. Proof automation is an important tool in interactive theorem proving, as it can significantly reduce the amount of guidance that the user needs to provide to formalize a proof.

Auto2 is a new proof automation tool written for Isabelle, designed to combine the advantages of existing approaches to automation: tactics and external automatic theorem provers. In this talk, I will describe the ideas behind auto2, and its application to formalization of mathematics, in particular building a library of mathematics from the axioms of set theory to the definition of the fundamental group in algebraic topology.

欢迎感兴趣的老师同学参加!