History of the New Symbol Names

This issue was raised in an email to known ATP system developers:

1. Koen Claessen (Paradox, Equinox, Infinox),

2. Hans De Nivelle (Bliksem, Geo),

3. Damien Doligez (Zenon),

4. Alexander Fuchs (Darwin).

5. Joe Hurd (Metis),

6. Konstantin Korovin (iProver),

7. Bill McCune (Prover9, Mace4),

8. Stephan Schulz (E),

9. Mark Stickel (SNARK),

10. Andrei Voronkov (Vampire),

11. Russell Wallace (Ayane),

12. Christoph Weidenbach (SPASS),

13. Jens Otten (leanCoP).

(I apologize to any developers who I left out - your feedback is also of interest).

Constraints and Requirements and Features

1. A recommended, but not required, naming convention for new symbols would help.

2. The recommendation must accomodate various types of new symbols, including Skolems, defined functions, defined predicates, and variables.

3. The recommended new symbol names should not open new name spaces, which would require changes to the existing TPTP syntax. If the output from one system is to be used as input to other systems, then it is not possible to open a new name space for new symbol names. Thus new non-variable symbol names should start with lowercase and consist of only alphnumerics and underscore. Similarly, new variable symbol names should start with uppercase and consist of only alphnumerics and underscore.

4. If the recommended new non-variable symbol names are in the name space of input symbols, then the recommended new symbol names should minimize the possibility of clashes with input symbol names.vThe convention minimizes the possibility of clashes with inputvnon-variable symbol names - evidence for this is that no problemvin the TPTP has any lines that match '[(, ] *s[A-Z][0-9]+(_[A-Za-z0-9_]+)?'.

5. New symbol names should be easy to recognize, by having an uncommon format. The naming convention has these features:vNew non-variable function symbols are easily found in formulaevusing the regular expression '[(, ] *s[A-Z][0-9]+(_[A-Za-z0-9_]+)?'.

6. The recommended new symbol names should not have to be long or ugly,vfor the sake of those who look at a lot of clauses and proofs. The convention's basic new symbol names are short.

7. It should be possible to annotate new symbol names, reflecting some extra meaning behindvthe symbols, e.g., introduced via splitting, domain name as in finite interpretations,vsystem that introduced the name etc.vThe convention allows arbitrary annotation for particular applications.

8. It is necessary to check for clashes when a new symbol name is generated in an ATP system.vIf a clash occurs, options are:

   1. Report an error.

   2. Retrospectively rename the clashing generated symbol.

   3. Rename the clashing input symbol.

9. The introduction of new non-variable symbols should be documented in ATP systems' output.