Lecture by Geoff Sutcliffe


Watch the talk by Geoff Sutcliffe (Department of Computer Science at university in Miami) entitled „Automated Theorem Proving and the TPTP World – Infrastructure for Automated Reasoning“ that took place at CIIRC on 5th April 2019

You can watch the video here

Automated Theorem Proving (ATP) is one of the older endeavors in Computer
Science. It is underpinned in mathematical logic, and aspects of ATP hark
back to the ideas of Socrates and Chrysippus. Modern ATP, especially
state-of-the-art ATP computer programs, are slowly starting to make
contributions in applications, stemming from mathematics, through
various natural and social sciences, touching on the humanities, and
even reaching commonsense reasoning. These successes are to some extent
dependent on frameworks that allow the various components to work together
seamlessly. The TPTP World is a well known and established infrastructure
that supports research, development, and deployment of 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 introduces the general field of ATP and the logics
employed in ATP, reviews the core features of the TPTP World, describes
key service components of the TPTP World and how to use them, and presents some successful applications.


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 automated reasoning system (SSCPA); 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. He is one of the leaders of the StarExec project that provides computing infrastructure to logic-solving communities, to facilitate the experimental evaluation of logic solvers. 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 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 chair of the College of Arts and Sciences curriculum committee.