The Logic Languages of the TPTP World
Abstract
The TPTP World is a well established infrastructure that supports research,
development, and deployment of Automated Theorem Proving (ATP) systems.
This talk provides an overview of the logic languages of the TPTP World,
from classical first-order form, through typed first-order form, up to typed
higher-order form, and beyond to non-classical forms.
The logic languages are described in a non-technical way, and are illustrated
with examples using the TPTP language.