The TPTP Convention for New Symbol Names

• 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 non-negative integer used to make the basic symbol name unique.
  • 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 predicate symbols with other uses, e.g., for splitting
  • The index N should be global across all symbol types, or local to each symbol type.
  • Examples: sK1, sF99, sP127.

• 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 suffix.

• The introduction of new non-variable symbols should 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]),skolemized(X4)],[49])).
      
      fof(64,plain,
          ( sP1 <=> ! [X8] : ~ has_job(X8,boxer) ),
          introduced(definition,[new_symbols(definition,[sP1])],[])).

• ATP systems should 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.