The TPTP Typed First-order Form with Arithmetic:
The Language and Some Applications
Abstract
The TPTP World is a well established infrastructure supporting research,
development, and deployment of Automated Theorem Proving systems.
In 2010 the TPTP World was extended to include a typed first-order
logic, which in turn enabled the integration of arithmetic.
This talk describes the Typed First-order with Arithmetic (TFA) part of
the TPTP World - the language syntax and semantics, the arithmetic
capabilities, and some applications that use these features.