Abstract
Most input languages for ATP systems, including the existing TPTP logical
languages, are designed primarily to write the logical formulae that are
input to and output from ATP systems' reasoning processes.
There is minimal or no support for controlling the processing of the logical
formulae: tasks such as incrementally adding and deleting formulae,
controlling reasoning processes, and interacting with non-logical data.
The TPTP Process Instruction (TPI) language augments the existing and
well-known logical TPTP language forms with command and control instructions
for manipulating logical formulae in the context of ATP systems.
The TPI language makes it easy(er) for ATP users to specify their problems,
process the logical formulae, and report results, in a fully automatic way.
Two interpreters for the TPI language have been implemented, and have been
productively used in several applications.