報告人：Geoff Sutcliffe教授 美國邁阿密大學計算機科學系
報告人簡介：
Geoff Sutcliffe is a Professor and the Chair of the Department of Computer Science at the University of Miami. He received a BSc(Hons) and MSc from the University of Natal, and a PhD in Computer Science from the University of Western Australia. His research is in the area of Automated Reasoning, particularly in the evaluation and effective use of automated reasoning systems. His most prominent achievements are: the first ever development of a heterogeneous parallel deduction system, leading to the development of the SSCPA automated reasoning system; the development and ongoing maintenance of the TPTP problem library, which is now the de facto standard for testing classical logic automated reasoning systems; the development and ongoing organization of the CADE ATP System Competition - the world championship for classical logic automated reasoning systems; and the specification of the TPTP language standards for automated reasoning tools. The research has been supported by grants from the National Science Foundation, the German Ministry for Research, the Australian Research Council, the European Union, and internal university grants from Edith Cowan University, James Cook University, and the University of Miami. The research has produced over 125 refereed journal, conference, and workshop papers.
He is an editor of Acta Informatica and the Formalised Mathematics journal, and has been guest editor of several special journal issues on topics in automated reasoning. He has contributed to the automated reasoning and artificial intelligence communities as a conference or program chair of (several instances of) the International Conference on Automated Deduction (CADE), the International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), and the International Florida Artificial Intelligence Research Society (FLAIRS). He was co-founder and organizer of the "ES*" series of workshops on Empirically Successful Automated Reasoning. He regularly serves as a program committee member and reviewer for automated reasoning and artificial intelligence journals and conferences. He has served three terms as a CADE trustee, is on the LPAR steering committee, is on the Linking Research Globally (LRG) steering committee, and is currently the president of FLAIRS. As a faculty member at the University of Miami he is currently chair of the College of Arts and Sciences curriculum committee.
報告1
題目：The TPTP World -Infrastructure for Automated Reasoning (TPTP世界—自動推理的基礎)
報告時間：2018年6月4日（星期一）15:00-16:00
報告地點：九里校區(qū)信息樓01020
報告內(nèi)容簡介：
The TPTP World is a well-known and established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The data, standards, and services provided by the TPTP World have made it increasingly easy to build, test, and apply ATP technology. This talk reviews the core features of the TPTP World, describes key service components of the TPTP World, presents some successful applications, and gives an overview of the most recent developments.
報告2
題目：ATutorial on the ATP Systems Running on TPTP (TPTP基準庫上運行的自動推理系統(tǒng))
報告時間：2018年6月4日（星期一）16:30-17:30
報告地點：九里校區(qū)信息樓01020
報告內(nèi)容簡介：
The TPTP World is a well-known and established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The data, standards, and services provided by the TPTP World have made it increasingly easy to build, test, and apply ATP technology. This interactive tutorial, based on the introduction about TPTP world, shows the audience how to use TPTP tools, how to run the ATP systems on TPTP, and pose some simple problems for them to solve.
報告3
報告題目：Making Belnap's "Useful 4-Valued Logic" Useful (讓Belnap的“有用的4值邏輯”真正有用)
報告時間：2018年6月5日（星期二）15:00-16:00
報告地點：九里校區(qū)信息樓01020
報告內(nèi)容簡介：
In 1977 Nuel Belnap published two articles, "How a Computer Should Think" and "A Useful Four-Valued Logic", in which he defined a four-valued logic called FDE (First Degree Entailment). However, FDE does not allow entailments within statements, and no conditional connective is defined. As such, it is not really computationally "useful". This work proposes conditional connectives to add to FDE, and describes the implementation of a reasoning tool for FDE with a conditional connective, with experimental results. With the addition of a conditional connective FDE starts to become truly computationally useful.
報告4
報告題目：State of the Art in Automated Reasoning (自動推理研究最新進展)
報告時間：2018年6月7日（星期四）09:30-10:15
報告地點：九里校區(qū)信息樓01020
報告內(nèi)容簡介：
Automated reasoning 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 reasoning. It will describe the basic architecture of current high-performance automated theorem provers for first-order logic. We shortly discuss the evaluation and performance of theorem provers. The talk concludes with a short outlook on current and possible future developments.
