Geoff Sutcliffe and Juergen Zimmer and Stephan Schulz:
TSTP Data-Exchange Formats for Automated Theorem Proving Tools

Abstract:

This paper describes two data-exchange formats for Automated Theorem
Proving (ATP) tools.  First, a language for writing the problems that
are input to ATP systems, and for writing the solutions that are
output from ATP systems, is described.  Second, a hierarchy of values
for specifying the logical status of an ATP problem, as may be
established by an ATP system, is described.  These data-exchange
formats will support application and research in ATP, and will
facilitate communication between ATP tools in distributed and embedded
environments.