The TPTP Convention for New Symbol Names

This page describes the TPTP convention for the names of new symbols that are introduced by ATP systems when processing a TPTP problem.

Basic new non-variable symbol names are recommended to be of the form sKN, where K is an uppercase letter indicating the type of new symbol, and N is a decimal number used to make the basic symbol name unique. For examples, sK1, sF99, sP127.
- The conventions for K are
  - K for Skolems
  - F for defined functions
  - G for function symbols with other uses
  - P for defined predicates
  - Q for predicte symbols with other uses
- The index N can be global across all symbol types, or local to each symbol type.
Basic new variable symbol names are recommended to be of the form SVN, where N is a decimal number used to make the symbol name unique. (Thus the form mimics that form of new non-variable symbol names, but with an uppercase first letter as dictated by the TPTP language.) For examples, SV1, SV99. The index N can be global across all formulae, or local to each formula.
Basic new symbol names can optionally be extended by an underscore then one or more alphanumeric and underscore characters. For examples, sK1_iProver, sF99_Splitting, sP127_3, SV99_ForallIntro. The names should remain unique without the extension, using the N decimal number.
The introduction of new non-variable symbols can be recorded in a <new_symbol_record> in the <useful_info> field of the <inference_record> of a derived formula, or in the <optional_info> field of the <internal_source> of an introduced formula. The new form will have the format new_symbols(Type,[Symbols]). The Type indicates the type of new symbol, with possible values skolem, definition, other. Symbols is a comma separated list of new symbols of that type. The <useful_info> field can have multiple new_symbols() terms. For examples,
```
    fof(50,plain,(
        ! [X3] : ~ hates(X3,sK1(X3)) ),
        inference(skolemize,[status(esa),new_symbols(skolem,[sK1])],[49])).
    
    fof(64,plain,
        ( ~ sP1
      <=> ! [X8] : ~ has_job(X8,boxer) ),
        introduced(definition,[new_symbols(definition,[sP1])])).
```
ATP systems can be expected to check for clashes whenever they generate a new symbol, and whenever they read input after any new symbols have been generated.

If you are interested in the history and motivations behind this convention, read the source of this web page.