Abstract
The TPTP World is the established infrastructure used by the Automated Theorem Proving (ATP)
community for research, development, and deployment of ATP systems.
The data, standards, and services provided by the TPTP World have made it easy to develop,
evaluate, and deploy ATP technology.
This talk and tutorial reviews the core features of the TPTP World, describes key services
of the TPTP World, and presents some successful applications.
The use of ATP as the reliable substrate to subsymbolic AI systems (e.g., LLMs), to form
neurosymbolic AI systems, is reviewed.