The TPTP Tea Party

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 TPTP problem library
The TSTP solution library
The TPTP syntax
Anything else in the TPTP World
etc

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.

Meeting Artifacts

Registration: This tea party requires registration using this link, with payment of a registration fee:

Funded researchers and faculty - $100/€100
Unfunded researchers and faculty, Funded students - $50/€50
Unfunded employed students - $20/€20
Unfunded unemployed students - FREE

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^*, André Duarte, Clemens Eisenhofer^*, Pascal Fontaine^*, Christian Franck,^* David Fuenmayor^*, Pamina Georgiou^*, Pierre Grenon^*, Marton Hadju^*, Edvard Holden, Petra Hozzova^*, Cezary Kaliszyk^*, Konstantin Korovin, Laura Kovacs^*, Jack McKeown, Cláudia Nalon^*, Chris Partridge^*, Adam Pease^*, Elaine Pimentel^*, Michael Rawson^*, Giles Reger, 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):

The Big Picture - my plans for 2022 and 2023
- I'm working on upgrading my parser, and the tools that use it, e.g., TPTP4X, to fully support Boolean terms, tuples, $ite, and $let.
- A new sublanguage TXF, split into TX0 (monomporphic) and TX1 (polymorphoc), will appear. TXF is TFF plus Boolean terms, tuples, $ite, and $let. THF will also (continue to) have tuples, $ite, and $let. See below, and the web page.
- The statistics I collect for each problem and solution are being revised, which will percolate through to the ProblemAndSolutionStatistics file (which might impact some people's analysis tools).
- TPTP v8.0.0, with TXF problems, will be released in the first half of 2022.
- CASC-J11 will be based on TPTP v8.1.0, but will not use TXF.
- CASC-29 will be based on a TPTP v8.* version, with the TFA division becoming the TXA division - TX0 with arithmetic.
- The TPTP will embrace non-classical logic - see below and the web page. New sublanguages for non-classical logics will appear. These are necessarily built on TXF and THF. The new languages will probably be NFF (split into NF0 and NF1) and NHF (split into NH0 and NH1).
- TPTP v9.0.0, with NFF and NHF problems is planned for the second half of 2022.
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?

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>)

Extending TFF and THF (Geoff)
- Adding FOOL, tuples, $let, $ite to TFF, to produce TXF (i.e., TX0 and TX1)
- Adding tuples, $let, $ite to THF.
  - Should $ite be a function that can be applied, relational, or both?
Adding non-classical logics to TXF and THF (Alex)
The "Tons of Data for Theorem Prover" (TDTP) library (Geoff)
- Structural ideas
- Current tons
Hosting the TPTP World in Github (Geoff)
- So far ... TPTP World organization
  - JJParser
  - SyntaxBNF
  - Non-classical logic, and web pages
  - TPTP Problem library (empty)
  - MPTPTP2078 (part of the TDTP)
- What should be there?
- How should it be structured?
- Who should have what access in what ways?
- Should it be separated from my private account?
Funding for StarExec (Geoff)
- Looks like about $5000 per year
- How about those who pay get higher priority on the cluster?

TPTP Tea Party

Tea Party Pictures