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.

August 11-12, 2022

This is the first EuroProofNet WG2 meeting, taking place at Haifa, August 11-12, 2022. The meeting is co-located with PAAR 2022, which is itself an IJCAR 2022/FLoC 2022 workshop.

See this page for more information about EuroProofNet Working Group 2

This meeting aims to

  • bring together members of the different communities working on proofs and automated theorem provers (in the broad sense, including SAT solvers, SMT solvers, First-Order and Higher-Order Provers, Computer Algebra Systems,…)
  • foster collaborations and build synergies among participants to ease the path to more fruitful results for the Action, and
  • pave the way for the WG2 deliverables:
    • D3 (April 2023) Inventory of automated theorem provers producing proofs, description of proof formats, and inventory of checking tools for these proof formats.
    • D4 (February 2025): Software for translating proof formats used by automated theorem provers to Dedukti.

Speakers

  • Josef Urban (Czech Institute of Informatics, Robotics and Cybernetics)
  • Geoff Sutcliffe (University of Miami, USA)
  • Andres Notzli (Stanford, USA)
  • Guillaume Burel (ENSIIE, France)

Organization

Registration

Participation to the WG meeting is free but registration is required. Please notice however that participation to collocated events and usage of FLoC facilities is not free.

Registration form

Please contact Pascal Fontaine and Alex Steen if you have any problem during the registration process, including reluctance to use google forms.

We might allocate time in the last session (WG 2 business meeting and planning) to present and discuss topics raised by WG2 members in the context of the Action goals and deliverables. If you are interested in briefly presenting a specific problem, please let us know through the dedicated question in the registration form. You can also contact us for any question related to the program.

Funding applications

EuroProofNet can partially fund the travel to Haifa and the accommodation to attend the WG2 kickoff meeting for some participants. The daily allowance for accommodation and meals has been fixed at 120 euros.

If you want to be funded, you need to:

  • Register to EuroProofNet if not already done. (Subscribe to WG2)

  • Before July 15, send a mail to Pascal Fontaine and Alexander Steen with
  • justified travel cost estimation (e.g., via screenshots or invoices for flights)

  • a short justification to explain your contribution to the objectives of EuroProofNet WG2

  • Notifications will be sent out on July 22. Selected people will receive an invitation from e-cost.

  • During the meeting, sign the attendance sheet that will be circulating.

  • After the meeting, and within 2 weeks, upload on e-cost a copy of your flight/train tickets and of your hotel bill.

You are free to arrive before August 11 (e.g. to attend FLoC and PAAR) and leave after August 12 (e.g. to work with some colleagues), but EuroProofNet will only cover accommodation costs necessary to attend the WG meeting (in particular, it does not cover registration cost to any FLoC event!).

The action members who will be reimbursed will be chosen by taking into account the following criteria in order: importance wrt the research coordination objectives; inclusive target countries; age; gender; team with low resources; balance over the action life time between people, teams, countries and working groups.

For more details, see the reimbursement rules.

Venue & Accommodation

See the FLoC pages

Program

Day 1 Thursday, August 11
09:00-10:00 Josef Urban (invited talk, Czech Institute of Informatics, Robotics and Cybernetics)
  Training ENIGMAs, CoPs, and other thinking creatures
  Slides of the talk or on the author’s web
Day 2 Friday, August 12
09:00-10:00 Geoff Sutcliffe (invited talk, University of Miami)
  The Logic Languages of the TPTP World
  Slides (part 1) Slides (part 2)
14:00-14:05 COST action EuroProofNet plenary presentation
  Slides
14:05-14:50 Guillaume Burel (invited talk, ENSIIE)
  EuroProofNet presentation on proofs in Dedukti
  Slides
14:50-15:35 Andres Notzli (invited talk, Stanford)
  EuroProofNet presentation on SMT and proofs
  Slides
16:00-16:45 SMT Proof discussion (joint with the SMT Workshop)
  The items discussed are also summarized in
  Haniel Barbosa’s invited column in the AAR newsletter
16:45-17:30 WG 2 business meeting and planning
  Slides

Notice that some sessions of the PAAR workshop are of interest to the EuroProofNet Community (for instance Session 2 of Friday).

Organization