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

報(bào)告人：Stephan Schulz教授 德國(guó)DHBW Stuttgart大學(xué)

報(bào)告題目：State of the Art in Automated Deduction (自動(dòng)演繹推理研究最新進(jìn)展)

報(bào)告時(shí)間：2017年7月3日（星期一）09:30-10:15

報(bào)告地點(diǎn)：九里校區(qū)信息樓01020

報(bào)告內(nèi)容簡(jiǎn)介：

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.

報(bào)告人簡(jiǎn)介：

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

主辦：研究生院

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

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

報(bào)告人：Stephan Schulz教授 德國(guó)DHBW Stuttgart大學(xué)

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

報(bào)告時(shí)間：2017年7月4日（星期二）09:30-10:15

報(bào)告地點(diǎn)：九里校區(qū)信息樓01020

報(bào)告內(nèi)容簡(jiǎn)介：

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.

報(bào)告人簡(jiǎn)介：

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

主辦：研究生院

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