European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

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