TPTP Tea Party
will be held
at 9:00am EDT on Thursday 9th December 2021
This meeting will bring together developers and users of the TPTP World, including (but not
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
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,
- Funded researchers and faculty - $100/€100
- Unfunded researchers and faculty, Funded students - $50/€50
- Unfunded employed students - $20/€20
- Unfunded unemployed students - FREE
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-19 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
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
- Adding non-classical logics to TXF and
- The "Tons of Data for Theorem Prover" (TDTP) library
- Structural ideas
- Current tons
- Hosting the
TPTP World in Github
- So far ... TPTP World organization
- 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 provate account?
- Funding for StarExec (Geoff)
- Looks like about $5000 per year
- How about those who pay get higher priority on the cluster?
Tea Party Pictures