The 14th 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 2025 TPTPTP will focus on "Representation, Verification, and Visualization of TPTP Format
Proofs and Models" (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 Geoff - Review of the TPTP format for derivations, IDV
- 09:30-10:00 Geoff - Proof verification, GDV, GDV-LP
- 10:00-10:30 Melanie - Leo-III and LambdaPi
- 10:30-11:00 Break
- 11:00-11:30 Anja - Vampire and Dedukti?
- 11:30-12:00 Michael - VoRaSu verification of Skolemization steps
- 12:00-12:30 Martin - Equisatisfiable inferences.
- 12:30-14:00 Lunch
- 14:00-14:30 Sean - The new TPTP format for tableau proofs, ITV, GDV
- 14:30-15:00 Geoff, Alex - The new TPTP format for interpretations, IIV, AGMV
- 15:00-15:30 Who - Recording details of failed proof verification
- 15:30-16:00 Break
- 16:00-16:30 Simon, Julie - The ProoVer Competition at IJCAR 2026.
- 16:30-17:00 StarExec-ARC, TPTP IDE - Geoff, David, Daniel, Esteban
- 17:00-18:00 Action planning == Wish list (with cheese and wine)
- Slides
- Email me geoff@tptp.org