The 15th TPTP Tea Party
The TPTP Tea Party (TPTPTP) brings together developers and users of the TPTP World, including
(but not limited to):
- The TPTP problem library and the TSTP solution library
- The TPTP languages, problem formats, and solution formats
- TPTP World software
- The CADE ATP System Competition (CASC)
- etc.
The meeting aims to elicit feedback, suggestions, criticisms, etc, of these resources, in order
to ensure that their continued development of the TPTP World meets the needs of successful
automated reasoning.
The 2026 TPTPTP will ask the question "What is an Acceptable Proof?", including the related topic
of "What is an Acceptable Answer?" (but other topics might sneak in).
The schedule below looks like a regular workshop, but presenters can make maximally a 20 minute
(optimally 15 minute) presentation, slides optional.
Then it's an open forum.
Program
- 08:30-09:00 Welcome coffee
- 09:00-09:10 Geoff - Welcome, thanks, today's mission, flexibility,
Zoom,
cheese and wine.
- 09:10-09:30 What is an
Acceptable Proof? - Geoff
- See the
CASC requirements
- See the
ProoVer Rules and Format
- Mixed languages ... Same as problem? Not stronger than problem?
- Geoff and Michael
- Is it acceptable to have inference rules that use unnecessary parents? -
Marton
- The rule "Inference steps must list exactly those parents that are used
in the inference." might be implementable by the request that "Proofs
should graft in subproofs from external systems.".
- Do formulae not part of the proof DAG have to be correct? - Stephan
- 09:30-10:00 Recording and Verifying
Derivations - Geoff
- Should introduced(definition,...) have to be in an
annotated formula with the definition role?
- Should variables in skolemized() records be quantified?
- axioms that have an introduced(theory,...) are
now also "gifts from god", like weird definitions - Marton
- Should nested interference records all have the same SZS status?
It would make verification cleaner. Geoff and Stephan
- Should new (Herbrand) symbols have to be recorded as
new_symbols()? Simon and Geoff
- Interferences - MartinS and MichaelR
- 10:00-10:30 Layers of
Solution Expectations for CASC - Geoff
- Leaf checking of proofs next year
- More?
- TPTP interpretation format (talk later today)
- 10:30-11:00 Break
- 11:00-11:30 Layers of Proof Expectations for ProoVer - Simon and Julie
- 11:30-12:00 The TPTP Format for Clausal Connection Tableaux - Sean
- 12:00-12:30 The
TPTP Format for Interpretations - Geoff
- 12:30-13:40 Lunch
- 13:40-14:20 Attend the Vampire workshop for
two interesting talks
- 14:30-15:00 Towards a
TPTP Format for Answers - Geoff and MartinS and MichaelR
- 15:00-15:30 General
TPTP stuff - Michael
- Interpretation in TXF and THF of ! [X: $o] : X = p -
Stephan
- Datatypes and codatatypes - Michael and Petra
- Qantification of variables in $let - Marton
- 15:30-16:00 Break
- 16:00-16:30 TPTP World and StarExec
development - Geoff
- StarExec
containerised ... git clone; make start
- StarExec Kubernetes ... AWS, Miami in August
- StarExec+benchexec+SLURM at TU Wien
- Does anyone need to hire a wizard programmer?
- VSCode extension, in the market place.
- A TPTP World consortium?
- 16:30-18:00 Action Planning == Wish List (with cheese and wine)
Speakers' Slides