Using the TPTP Language for Writing Derivations and 
                     Finite Interpretations 

                        Geoff Sutcliffe
                        Stephan Schulz
                        Koen Claessen
                        Allen Van Gelder

One of the keys to the success of the TPTP and related projects is
their consistent use of the TPTP language.  The ability of the TPTP
language to express solutions as well as problems, in conjunction with
the simplicity of the syntax, sets it apart from other languages used
in ATP.  This paper provides a complete definition of the TPTP
language, and describes how the language should be used to write
derivations and finite interpretations.