Programme
|
1st Day |
1 of August | |
| 1st session | 9h00 -- 12h00 | Chair: Pedro Quaresma |
| 9:00-- 9:30 | Welcome | |
| 9:30--10:00 | András Kerekes and Zoltán Kovács | Towards automatic detection of geometric difficulty of geometry problems |
| 10:00--10:30 | Michael Katzenberger and Jürgen Richter-Gebert | Manifold-based Proving Methods in Projective Geometry |
| 10:30--11:00 | Coffee Break | |
| 11:00--11:30 | Predrag Janičić and Julien Narboux | Geometry Machine Revisited |
| 11:30--12:00 | Gábor Gévay, Benedek Kovács and Zoltán Kovács | Is a regular polygon determined by its diagonals? |
| 12:00--14:30 | Lunch | |
| 2nd session | 14:30 -- 17:30 | Chair: Zoltán Kovács |
| 14:30--15:00 | Álvaro Pereira-Albert, Tomas Recio and M. Pilar Velez | Computing loci with GeoGebra Discovery: some issues and suggestions |
| 15:00--15:30 | Shivam Sharma and John Keyser | Inference Maximizing Point Configurations for Parsimonious Algorithms |
| 15:30--16:00 | Coffee Break | |
| 16:00--16:30 | Vesna Marinković,
Tijana Šukilović and Filip Marić |
Different Types of Locus Dependencies in Solving Geometry Construction Problems |
| 16:30--17:00 | Pedro Quaresma and Pierluigi Graziani | Towards a Structural Analysis of Interesting Geometric Theorems: Analysis of a Survey |
| 17:00--17:30 | Thierry Dana-Picard | Singular points of plane curves obtained from geometric constructions: automated methods in man-and-machine collaboration |
| 2nd Day | 2 of August | |
| 3rd session | 9h00 -- 12h00 | Chair Julien Narboux |
| 9:00--10:00 | Vesna Marinković | Invited Talk: Automating Geometry Construction Problems |
| 10:00--10:30 | Yoan Géran and Pierre Boutry | First-order Simplification of GeoCoq using Dedukti |
| 10:30--11:00 | Coffee Break | |
| 11:00--11:30 | Alexandre Jean, Pierre Boutry and Nicolas Magaud | An Automated Approach towards Constructivizing the GeoCoq Library |
| 11:30--12:00 | Prunelle Colin and Pierre Boutry | On the Coq/Rocq Mechanization of Beeson's "On the Notion of Equal Figures in Euclid" |
| 12:00--14:30 | Lunch | |
| 4rd session | 14:30 -- 17:30 | Chair: Pierre Boutry |
| 14:30--15:00 | Pedro Quaresma, Predrag Janičić, Julien Narboux, Zoltán Kovács, Anna Petiurenko, Filip Marić and Nuno Baeta | ADG-Lib Initiative |
| 15:00--15:30 | Pedro Quaresma and Nuno Baeta | A Generator of Geometry Deductive Database Method Provers |
| 15:30--16:00 | Coffee Break | |
| 16:00--16:30 | Roland Coghetto | IsaGeoCoq, a port of GeoCoq with Isabelle/HOL |
| 16:30--17:00 | Zoltán Kovács | Proving theorems on regular polygons by elimination --- the elementary way |
| 17:00--17:30 | Business Meeting | Chair: Pedro Quaresma and Julien Narboux |