The 9th TPTP Tea Party will be held in the ZoomRoom at 4:30pm CEST on Friday 3rd July 2020 at the 10th International Joint Conference on Automated Reasoning 1st-4th July 2020

• 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 meeting will be structured discussion following an agenda of topics that have been suggested and agreed upon in advance.

The organizer is Geoff Sutcliffe. People who have confirmed that they will attend are: Jeremy Avigad, Seulkee Baek, Haniel Barbosa, Jasmin Blanchette, Frédéric Blanqui, Ahmed Bhayat, Pascal Fontaine, Mohamed Yacine el Haddad, Laura Kovacs, Andre Platzer, Thomas Prokosch, Giles Reger, Martin Riener, Stephan Schulz, Nick Smallbone, Martin Suda, Geoff Sutcliffe.

The topics for this year are (so far - please email me if you have more):

---

1. The new "Slammer Division" for CASC-28 - Jasmin Blanchette. (Slides)

   ---

2. Solution Representation.

   The TPTP Format for Derivations and the TPTP Format for Finite Interpretations have been around for a while, and widely adopted in the ATP community. Solution output is useful for:

   • Solution visualization
   • Solution verification
   • Solution optimization
   • Solution replay
   • What else?

   In order for a solution to be used for these tasks, it must have properties that make it Acceptable:

   • Must be parseable (in TPTP(-style) format)
   • Derivations must show only relevant inference steps.
   • Inference steps must document the parent formulae, the inference rule used, and the inferred formula.

   Can we formalize "acceptable", as a first step towards the uses listed above, and build a tool to check for acceptability?

   ---

3. Proof Verification.

   This is "easy" for SAT, "tricky" for FOF and beyond. I would say it is an unsolved problem for FOF and beyond.

   Techniques so far:

   • Verification of steps (by trusted tools) based on their semantics, e.g., SPASS, Vampire, GDV.
   • Verification of steps (by trusted tools) based on their inference rules, e.g, WHAT?.
   • Compilation to another form for verification (by trusted tools), e.g., TESC, ProofCert.

   Properties of proofs that might be required:

   • Derivations must be complete, starting at formulae from the problem, and ending at the conjecture (for axiomatic proofs) or a false formula (for proofs by contradiction, e.g., CNF refutations). For proofs that use translations from one form to another, e.g., translation of FOF problems to CNF, the translations must be adequately documented.
   • Inference steps must be reasonably fine-grained.
   • An unsatisfiable set of ground instances of clauses is acceptable for establishing the unsatisfiability of a set of clauses.
   Some of the above are limited to certain styles of proof.

   Can we find a way to verify proofs that works very generally?