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,
The names should remain unique without the extension, using the N
- The introduction of new non-variable symbols can be recorded in a
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
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
! [X3] : ~ hates(X3,sK1(X3)) ),
( ~ sP1
<=> ! [X8] : ~ has_job(X8,boxer) ),
- 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
If you are interested in the history and motivations behind this
convention, read the source of this web page.