Abstract
The TPTP World is the established infrastructure used by the Automated Theorem Proving (ATP)
community for research, development, and deployment of ATP systems.
This tutorial reviews the key components of the TPTP World, examines the logics supported in
the TPTP World, shows how problems can be encoded in logic using the TPTP languages,
demonstrates and provides practice in solving logic problems using TPTP World online tools, and
discusses "logic engineering" principles for solving problems using automated reasoning.