Using the TPTP Language for Writing Derivations and Finite Interpretations

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.

• Type: Conference
• Year: 2006
• Where: CADE
• Authors: Geoff Sutcliffe, Stephan Schulz, Koen Claessen, Allen Van Gelder
• Keywords: Automated Reasoning, CADE 2006, TPTP Language