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:

  • 09:00-09:30 Geoff - Welcome, TPTP derivation format, IDV, GDV
  • 09:30-10:00 Stephan - Pragmatics of Efficient Proof Generation
  • 10:00-10:30 Break
  • 10:30-11:00 Gilles - Dedukti, derivation format, tool overview
  • 11:00-11:30 Guillaume - Ekstrakto
  • 11:30-12:00 Discussion of interoperability, things that need to be done
  • 12:00-13:00 Lunch
  • 13:00-13:30 Geoff - TPTP interpretation format (classical), IIV, GCMV
  • 13:30-14:00 WHO - Dedukti interpretation format (thoughts?)
  • 14:00-14:30 Discussion of interoperability, things that need to be done
  • 14:30-15:00 Break
  • 15:00-15:30 Alex - TPTP non-classical language, Logic encodings
  • 15:30-16:00 Geoff - Non-classical tools - AGMMV, IKIV (Alex?)
  • 16:00-16:30 Discussion of interoperability, things that need to be done
  • 16:30-17:00 Break, with cheese and wine
  • 17:00-18:00 Action planning (with cheese and wine)
  • 19:00-22:00 Dinner

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