Motivation and History

ATP and Arithmetic

• An inglorious past
  • Partial implementations (Otter, Bill McCune, RIP)
  • Procedural attachments (SNARK, Mark Stickel, RIP)
  • Living dangerously without types (SPASS-XDB, Geoff Sutcliffe, ...)
  • No standardization
• Incredulous users
• SMT took the territory

Remember the Alamo (or the TPTP)?

• TPTP, TSTP, SystemOnTPTP, CASC
• CNF, FOF, THF, TFF

TFF and TFA

• TFF ... partially motivated by the need for arithmetic
• Designed in consultation with users and developers
• Rich arithmetic ... integers, rationals, reals
• Growing linkage with SMT