Fixing the TPTP (and its old syntax)

All in the new TPTP Syntax

Equality

• Now assumed to be builtin
  • (TPTP) Problems do not contain equality axioms
  • Axioms can be added with tptp2X
  • equal/2 still reserved and recognized by tptp2X

Terms with Semantics

• $true and $false
• Numbers reserved for future builtin arithmetic

Types and Statuses

• New formula types ... negated_conjecture, lemma, plain
• Problem statuses (in the TPTP) from the problem status ontology

Include Files

• Absolute
• Search under the $TPTP environment variable
• Search under the current working directory