The TPTP World is a well known and established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems. 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 and how to use them, and presents some successful applications.

Geoff Sutcliffe is a Professor in 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 Theorem Proving (ATP), particularly in the evaluation and effective use of ATP systems. His most prominent achievements are the development and ongoing maintenance of the TPTP World - the de facto standard framework for developing, testing, and applying ATP systems; and the development and ongoing organization of the CADE ATP System Competition - the world championship for classical logic ATP systems. He is one of the leaders of the StarExec project that provides computing infrastructure to logic-solving communities. His research has been supported by grants from the National Science Foundation, the German Ministry for Research, the Australian Research Council, the European Union, Amazon, and internal university grants from Edith Cowan University, James Cook University, and the University of Miami. The research has produced over 160 refereed journal, conference, and workshop papers.