tptp2X

The tptp2X utility is a multi-functional utility for reformatting, transforming, and generating TPTP problem files. In particular, it: 1) Converts from the TPTP format to formats used by existing ATP systems. 2) Applies various transformations to TPTP problems. 3) Controls the generation of TPTP problem files from TPTP generator files. tptp2X is written in Prolog, and should run on most Prolog systems. It is known to run on current versions of Eclipse, SICStus, SWI, and YAP Prolog. Before using tptp2X, it is necessary to install the code for the dialect of Prolog that is to be used. This and other installation issues are described next.