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.

Organizer: Pedro Quaresma

Date: 28-30 May 2024

Remark: the official dates of the meeting taken into account for reimbursements are from 28 to 30 of May (3 days). However, since most people will arrive on the 27th and leave on the 31st, the program includes two optional work sessions on those days (afternoon and morning).

Venue: Hôtel Restaurant Campanile Nice Aéroport, Nice, France 459-461 Promenade Des Anglais L’arénas 06200 Nice, France

How to get there? Hotel Campanile Nice Airport is 300m away from the airport.

Program: Different geometry systems, including axiomatic developments, school-level geometry, and automated theorem provers use a range of primitive axioms or “rules”. Preparing a meta-prover capable of dealing with and merging different sets of rules, specified in TPTP-FOL, formally verified to be consistent, with natural languages and geometric renderings and capable to be integrated in an array of educational system, such as dynamic geometry system is a milestone goal.

Objectives/Deliverables:

  • The construction/formal verification of the set of rules.

  • The construction of rule based provers

  • Integration of the provers in DGS(s), with natural and geometric renderings.

Registered participants:

Alexander Vujic, Anna Petiurenko,Jelena Marković, Julien Narboux, Nicolas Magaud, Nuno Baeta, Pedro Quaresma, Piotr Błaszczyk, Vesna Marinković, Zoltán Kovács

Programme:

Day 1 28 May
09:00-10:00 GDDM Set of Rules - Jelena Marković & Formal verification - Julien Narboux & Rule Base Provers - Zoltán Kovács (JGEx), Nuno Baeta (OGPCP-GDDM), Vesna Marinković (Larus) & Set of Rules for Education - Anna Petiurenko & Pedro Quaresma
10:00-10:30 coffee-break
10:30-12:30 GDDM set of rules - “Good Set of Rules”, how to build and check
12:30-14:00 Lunch
14:00-16:00 Rule Based Provers - implementation issues
16:00-16:30 Coffee-break
16:30-18:30 Applications of Rule Based Provers - Education, others
Day 2 29 May
09:00-10:00 GDDM set of rule, “Good set of rules” - how to build them and how to check them
10:00-10:30 coffee-break
10:30-12:30 Rule Based Provers, Implementation issues
12:30-14:00 Lunch
14:00-16:00 Application of Rule Based Provers, Education, others
16:00-16:30 Coffee-break
16:30-18:30 Other Geometries & other Strategies, SMT solvers and finite projective spaces
Day 3 30 May
09:00-10:00 GDDM set of rule, “Good set of rules” - how to build them and how to check them & Plan future work/collaborations
10:00-10:30 coffee-break
10:30-12:30 Rule Based Provers, Implementation issues & Plan future work/collaborations
12:30-14:00 Lunch
14:00-16:00 Application of Rule Based Provers, Readability/Efficiency/Usability issues at several levels & Plan future work/collaborations
16:00-16:30 Coffee-break
16:30-18:30 Other Geometries & other Strategies, Generic Provers / SMT solvers, Conjectures involving inequalities & Plan future work/collaborations

Application procedure: The number of participants is limited. If you want to be funded, check the eligibility rules and send a mail to Pedro Quaresma with the following information and documents:

  • URL of your homepage
  • planned date and time of arrival
  • planned date and time of departure
  • cost of travel in euros with quote (screen capture)
  • work plan: describe what you would like to do

Application deadline: 29/2/2024

Cost: Participants have to organize their travel by themselves. The hotel rooms are 84 euros per night including breakfast, lunch buffet is 18 euros. See the reimbursement rules for more details. The daily allowance is fixed at 125 euros.