Tons of Data for Theorem Provers
The TDTP Data Library
Abstract
Machine Learning (ML) is emerging as a game changer in ATP, and ATP systems
and tools that take advantage of ML are being developed.
Concrete examples of the ways ML can be used in ATP include axiom selection,
search guidance, direct logical reasoning, and learning assisted reasoning.
In order to provide support for the development, evaluation, and deployment
of ATP systems and tools that include ML components, the TPTP World is
being extended to provide the large corpora of (ATP) data required for ML,
and infrastructure to support access to and use of the data.
This will be embodied in the new “Tons of Data for Theorem Provers” (TDTP)
data library.