This meeting will bring together developers and users of the TPTP World, including (but not limited to):

  • The TPTP problem library
  • The TSTP solution library
  • The TPTP syntax
  • Anything else in the TPTP World

Specifically, this meeting will look at:

  • Producing TPTP-compliant proof output.
  • Tools for verifying (GDV, Dedukti), visualizing, translating (e.g., to and from Dedukti), TPTP proofs.
  • The new TPTP format for interpretations.
  • Tools for verifying (AGMV), visualizing (IIV), translating, TPTP interpretations.
  • TPTP formats and tools for proofs and models in non-classical logics.

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.

Organizers: Frédéric Blanqui, Geoff Sutcliffe, Alexander Steen, Pascal Fontaine

Date: 13 July 2023, 9 am - 6 pm (hours to be confirmed)

Venue: ENS Paris-Saclay, 4 avenue des Sciences, 91190 Gif-sur-Yvette, France

How to get there? See here. ENS is 25 minutes away from Massy by bus (2.10€). Massy is 30 minutes away from Paris center by train (4.05€), and 20 minutes away from Orly airport by train (13.15€).

Registration/Funding application procedure: EuroProofNet can reimburse the travel of a number of participants. If you would like to participate, give a talk or be reimbursed of your travel, check the eligibility and reimbursement rules, apply to the EuroProofNet working groups you are interested in, and fill in the registration/application form.

Deadline for funding applications: May 8 (notification on May 13)

Possible hotels around at about 100€/night with breakfast and free cancellation included:

Previous TPTP Tea Parties