Abstract
The TPTP World is a well known and established infrastructure that supports research, development,
and deployment of Automated Theorem Proving (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 practive in solving logic problems using TPTP World online tools, and
discusses "logic engineering" principles for solving problems using automated reasoning.