Rule based automated provers for geometry, 28-30 May 2024, Nice, France
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).
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, Pierre Boutry, Nuno Baeta, Pedro Quaresma, Piotr Błaszczyk, Vesna Marinković, Zoltán Kovács. Thierry Dana-Picard also join the group (extra-registry).
Some Photos:
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.