The TDTP Library

with Cezary, Josef, others

• The Tons of Data for Theorem Provers

  library, containing large sets of
  • Problems, with
  • Solutions, and
  • Meta-data, and a
  • Plug-and-play framework (yeah!)

• Two views

  using symbolic links
  • The TPTP view to integrate with the TPTP and TSTP
  • The ML view to support use of ML in ATP

• The TDTP exists

  in some ways
  • MPTPTP2078, GRUNGE, HOL4, Jinja Threads, could make CakeML, ...
  • Used in and extracted from CASC LTB divisions
  but needs work

• We all believe that

  Machine Learning will Save the World