【創(chuàng)源大講堂】

報告人：Stephan Schulz教授 德國DHBW Stuttgart大學(xué)

報告題目：State of the Art in Automated Deduction (自動演繹推理研究最新進展)

報告時間：2017年7月3日（星期一）09:30-10:15

報告地點：九里校區(qū)信息樓01020

報告內(nèi)容簡介：

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年獲得德國慕尼黑理工大學(xué)博士學(xué)位，現(xiàn)于德國DHBW Stuttgart大學(xué)計算機學(xué)院工作。他是邏輯自動推理領(lǐng)域國際知名專家，在自動推理理論、方法及實現(xiàn)、深度學(xué)習(xí)在自動推理中的應(yīng)用等方面做出了非常有影響的工作，其研發(fā)的自動定理證明器E Prover是目前國際上最著名的證明器之一。此外，他還是國際自動推理聯(lián)合會議(IJCAR-2018)等的程序委員會主席，并擔(dān)任多個雜志客座編輯。

主辦：研究生院

承辦：kaiyun開云官方網(wǎng)站

【創(chuàng)源大講堂】

報告人：Stephan Schulz教授 德國DHBW Stuttgart大學(xué)

報告題目：Architecture and Implementation of the Automated Theorem Prover E (自動定理證明器E的架構(gòu)與實現(xiàn))

報告時間：2017年7月4日（星期二）09:30-10:15

報告地點：九里校區(qū)信息樓01020

報告內(nèi)容簡介：

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年獲得德國慕尼黑理工大學(xué)博士學(xué)位，現(xiàn)于德國DHBW Stuttgart大學(xué)計算機學(xué)院工作。他是邏輯自動推理領(lǐng)域國際知名專家，在自動推理理論、方法及實現(xiàn)、深度學(xué)習(xí)在自動推理中的應(yīng)用等方面做出了非常有影響的工作，其研發(fā)的自動定理證明器E Prover是目前國際上最著名的證明器之一。此外，他還是國際自動推理聯(lián)合會議(IJCAR-2018)等的程序委員會主席，并擔(dān)任多個雜志客座編輯。

主辦：研究生院

承辦：kaiyun開云官方網(wǎng)站