The 11th

TPTP Tea Party

will be held in Zoom at 9:00am EDT on Thursday 9th December 2021


This meeting will bring together developers and users of the TPTP World, including (but not limited to): The meeting aims to elicit feedback, suggestions, criticisms, etc, of these resources, in order to ensure that their continued development meets the needs of successful automated reasoning.

The organizer is Geoff Sutcliffe.


Registration: This tea party requires registration using this link, with payment of a registration fee: When you have registered you will receive an email with details of how to pay. Invoices are available. Receipts are provided. Certificates of participation are available. Once you have registered you will receive an individualised link to access the Zoom meeting that is hosting the event,

Registered*=paid: Geoff Alexander*, Christoph Benzmüller*, Ahmed Bhayat, Jasmin Blanchette*, Franz Brauße, Martin Desharnais*, Clemens Eisenhofer*, Pascal Fontaine*, David Fuenmayor*, Pamina Georgiou, Pierre Grenon*, Edvard Holden, Petra Hozzova*, Cezary Kaliszyk*, Laura Kovacs, Cláudia Nalon*, Chris Partridge*, Adam Pease*, Elaine Pimentel*, Michael Rawson*, Giles Reger, Johannes Schoisswohl, Stephan Schulz*, Nick Smallbone*, Alexander Steen*, Martin Suda*, Petar Vukmirović, Yoni Zohar,


Topics: The meeting will be structured discussion following an agenda of topics that have been suggested and agreed upon in advance. The topics for this year are (so far - please email me if you have more):
  1. The Big Picture - my plans for 2022 and 2023
  2. The unused definition formula role (Geoff)
    %----"definition"s are intended to define symbols. They are either universally
    %----quantified equations, or universally quantified equivalences with an
    %----atomic lefthand side. They can be treated like "axiom"s.
    See an example in SYO365^5.p. Originally Chris Benzmüller (I think) suggested having a := connective for definitions, to indicate that the LHS is the defined term and RHS is the definition. That has never been used, and all definitions just use equality, with a default assumption of the LHS is defined by the RHS. Is that adequate? Can I throw := out of the syntax?
  3. Sequents ... what's their status? (Geoff)
    <thf_sequent>          ::= <thf_tuple> <gentzen_arrow> <thf_tuple>
    <tfx_sequent>          ::= <tfx_tuple> <gentzen_arrow> <tfx_tuple>
    %----This section is the FOFX syntax. Not yet in use.
    <fof_sequent>          ::= <fof_formula_tuple> <gentzen_arrow>
                               <fof_formula_tuple> | (<fof_sequent>)

  4. Extending TFF and THF
  5. Adding non-classical logics to TXF and THF (Tobias/Alex/Geoff)
  6. The "Tons of Data for Theorem Prover" (TDTP) library
  7. Hosting the TPTP World in Github (Geoff)
  8. Funding for StarExec (Geoff)



Tea Party Pictures