August 11-12, 2022
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.
- Josef Urban (Czech Institute of Informatics, Robotics and Cybernetics)
- Geoff Sutcliffe (University of Miami, USA)
- Andres Notzli (Stanford, USA)
- Guillaume Burel (ENSIIE, France)
- The final report will be available here.
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.
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.
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
|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|
|14:05-14:50||Guillaume Burel (invited talk, ENSIIE)|
|EuroProofNet presentation on proofs in Dedukti|
|14:50-15:35||Andres Notzli (invited talk, Stanford)|
|EuroProofNet presentation on SMT and proofs|
|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|
Notice that some sessions of the PAAR workshop are of interest to the EuroProofNet Community (for instance Session 2 of Friday).