TPTP Tea Partywill be held in the ZoomRoom at 4:30pm CEST on Friday 3rd July 2020 at the
10th International Joint Conference on Automated Reasoning
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):
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:
In order for a solution to be used for these tasks, it must have properties that make it Acceptable:
Can we formalize "acceptable", as a first step towards the uses listed above, and build a tool to check for acceptability?
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:
Properties of proofs that might be required:
Can we find a way to verify proofs that works very generally?