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 will be the final meeting of the WG2. It is part of the Final EuroProofNet Symposium.

Date: Thursday 11th to Saturday 13th (or Sunday 14th)

Venue: Institut Pascal, 530 Rue André Rivière, 91400 Orsay [access] [hotels] [food options]

Registration/funding requests: fill in this form

Important dates:

Objective: The aim of this meeting series is to bring together researchers working on the topics of working group 2 of EuroProofNet. Our work focuses on two topics: Our first aim is to work and improve automated theorem provers. Our second aim is to make them correct by improving proof logging – both in an attempt to produce short proofs but also to work on proof formats that support many features instead of having one format for each required feature. Proof logging is an important topic, as it makes it possible to check the work of a solver without trusting it. Our third aim is to translate proofs via the Dedukti proof system.

The program will be composed of talks and sessions to work alone or in small groups on the development of tools for automated theorem proving and proofs (in particular Dedukti proofs), taking advantage of the participation of experts on Dedukti, formula and proof exchange standards, and theorem provers and solvers, and to make progress on EuroProofNet objectives and deliverables.