報告人：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

題目：JGXYZ - An ATP System for Gap and Glut Logics (JGXYZ -一種針對非經(jīng)典邏輯的自動定理證明系統(tǒng))

報告時間：2019年7月15日（星期一）9:30-10:30

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

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

This talk describes an ATP system, named JGXYZ, for some gap and glut logics. JGXYZ is based on an equi-provable translation to FOL, followed by use of an existing ATP system for FOL. A key feature of JGXYZ is that the translation to FOL is data-driven, in the sense that it requires only the addition of a new logic's truth tables for the unary and binary connectives in order to produce an ATP system for the logic. Experimental results from JGXYZ illustrate the differences between the logics and translated problems, both technically and in terms of a quasi-real-world use case.

報告2

報告題目：CASC - The CADE ATP System Competition (CASC -自動定理證明器競賽的歷史與發(fā)展)

報告時間：2019年7月16日（星期二）9:30-10:30

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

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

The CADE ATP System Competition (CASC) is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems - the world championship for such systems. Besides the obvious aim of evaluating ATP systems, CASC stimulates ATP research, motivates development and implementation of robust ATP systems that are useful and easily deployed in applications, provides an inspiring environment for personal interaction between ATP researchers, and exposes ATP systems within and beyond the ATP community. This talk covers the past, present, and future of CASC.

報告3

題目：The TPTP Problem Library and Associated Infrastructure - from CNF to TH1, and Beyond (TPTP自動定理證明問題庫及其架構(gòu))

報告時間：2019年7月18日（星期四）09:30-10:30

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

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

This talk describes the TPTP problem library and associated infrastructure, from its use of Clause Normal Form (CNF), via the First-Order Form (FOF) and Typed First-order Forms (TF0 and TF1), through to the Typed Higher-order Forms (TH0 and TH1). This talk summarizes the aims and history of the TPTP, documents its growth up to v7.3.0, reviews the structure and contents of TPTP problems, gives an overview of TPTP-related infrastructure, and describes current work extending the TPTP to include Boolean terms and modalities.