【创源大讲堂】
报告人：Stephan Schulz教授 德国DHBW Stuttgart大学
报告题目：State of the Art in Automated Deduction (自动演绎推理研究最新进展)
报告时间：2017年7月3日（星期一）09:30-10:15
报告地点：九里校区信息楼01020
报告内容简介：
Automated deduction is a field in the intersection of Artificial Intelligence, Formal Logic, and Theoretical Computer Science. It is concerned with the development of systems that can automatically perform sound reasoning on well-defined domains like e.g. mathematics, computer programming or even philosophy.
This talk will provide an overview of recent applications and successes of automated deduction. It will describe the basic architecture of current high-performance automated theorem provers for first-order logic, including basics of saturation, equality handling, and implementation. We shortly discuss the evaluation and performance of theorem provers.The talk concludes with a short outlook on current and possible future developments.
报告人简介：
Stephan Schulz教授，2000年获得德国慕尼黑理工大学博士学位，现于德国DHBW Stuttgart大学计算机学院工作。他是逻辑自动推理领域国际知名专家，在自动推理理论、方法及实现、深度学习在自动推理中的应用等方面做出了非常有影响的工作，其研发的自动定理证明器E Prover是目前国际上最著名的证明器之一。此外，他还是国际自动推理联合会议(IJCAR-2018)等的程序委员会主席，并担任多个杂志客座编辑。
主办：研究生院
承办：威廉希尔亚洲公司
【创源大讲堂】
报告人：Stephan Schulz教授 德国DHBW Stuttgart大学
报告题目：Architecture and Implementation of the Automated Theorem Prover E (自动定理证明器E的架构与实现)
报告时间：2017年7月4日（星期二）09:30-10:15
报告地点：九里校区信息楼01020
报告内容简介：
E is an automated theorem prover for first-order logic with equality. In other words, it is a program that can (often) automatically construct a formal proof for a conjecture from a set of axioms. For several years, E has been among the strongest provers for this logic, and the strongest that is available in source from under a Free Software license.
In this talk, we discuss the architecture and implementation of the theorem prover. On the one hand, we look at various subsystems and their interplay, on the other hand we look at the software stack, from basic data types to the proof procedure, that implements these subsystems. We discuss issues like the efficient implementation of calculus rules, the main proof search procedure, and heuristics guidance for proof search.The talk concludes with a short outlook on possible and likely future directions for E.
报告人简介：
Stephan Schulz教授，2000年获得德国慕尼黑理工大学博士学位，现于德国DHBW Stuttgart大学计算机学院工作。他是逻辑自动推理领域国际知名专家，在自动推理理论、方法及实现、深度学习在自动推理中的应用等方面做出了非常有影响的工作，其研发的自动定理证明器E Prover是目前国际上最著名的证明器之一。此外，他还是国际自动推理联合会议(IJCAR-2018)等的程序委员会主席，并担任多个杂志客座编辑。
主办：研究生院
承办：威廉希尔亚洲公司
