Différences entre les versions de « Spécifications, Contraintes et Preuves en Géométrie Bilan2016-2021 »
| Ligne 9 : | Ligne 9 : | ||
===Résultats=== | ===Résultats=== | ||
====Mécanisation des constructions à la règle et au compas ==== | ====Mécanisation des constructions à la règle et au compas ==== | ||
| + | Cette problématique a été, dans l'équipe, essentiellement étudiée par P. Schreck et P. Mathis. Certaines résultats ont été obtenus et publiés avec Predrag Janicic et Vesna Marinkovic de l'Université de Belgrade (Serbie). | ||
| + | Le résultat le plus marquant réside dans la preuve algébrique en Maple des statuts de constructibilité à la règle et au compas de deux listes de problèmes de construction connues des mathématiciens américains sous le nom de liste de Wernick et liste de Connelly. Ces listes regroupent environ 270 problèmes de construction à la règle et au compas à partir de points caractéristiques, elles ont été créées de manière systématique à titre d'amusement et de challenge pour les professeurs de mathématique, principalement de lycée, et ont reçu des réponses partielles de divers mathématiciens dans le monde. L'originalité de notre travail est principalement d'avoir développer une méthode pour traiter automatiquement les deux listes et délivrer la statut, en gros constructible ou non constructible à la règle et au compas, de chaque problème. Nous avons à cette occasion mis en oeuvre ce qui fait la singularité de notre approche : nous avons mélangé du raisonnement géométrique formel, implanté sous forme d'un programme Prolog, pour guider la mise en forme et la triangularisation de systèmes algébriques sous forme de chaînes régulières, ces dernières étant traitées par Maple pour obtenir les groupes de Galois correspondant, tout cela a été implanté par un programme Maple. | ||
| + | Il convient de noter qu'il s'agit ici de tester la constructibilité et non d'exhiber, éventuellement, une construction. Les dernier résultats de noter équipe dans ce domaine ont consisté à comparer une méthode due à Lebesgue et que nous avons améliorer et une méthode due à Chou et Gao. Un challenge est de tirer parti de cette étude pour avoir une méthode praticable pour des équations de degré 8. | ||
====Fondements de la géométrie==== | ====Fondements de la géométrie==== | ||
====Aide à la preuve en géométrie d'incidence==== | ====Aide à la preuve en géométrie d'incidence==== | ||
Version du 5 janvier 2021 à 11:20
Objectifs/Challenges
Les objectifs de ce thèmes relèvent de la formalisation de la géométrie en vue d'usages pratiques comme la résolution de contraintes géométriques, l'aide à la preuve en géométrie dans les domaines de l'enseignement ou de la robotique ou encore la certification d'algorithmes ayant trait à la géométrie. C'est une thématique difficile où se côtoient des aspects théoriques comme le calcul algébrique formel, la théorie du calcul des constructions ou encore l'axiomatisation de la géométrie et des aspects plus pratique comme l'ingénierie de la preuve en Coq ou le guidage de méthodes numériques développées en C++.
Participants
- Un professeur : Pascal Schreck
- Quatre maîtres de conférences : Gabriel Braun, Nicolas Magaud (HDR), Pascal Mathis (HDR) (jusqu'au 31/08/2017), Julien Narboux
- Deux doctorants : David Braun (Allocataire UNISTRA du 10/2015 au 09/2018) et Pierre Boutry (Allocataire UNISTRA du 10/2013 au 09/2016)
Résultats
Mécanisation des constructions à la règle et au compas
Cette problématique a été, dans l'équipe, essentiellement étudiée par P. Schreck et P. Mathis. Certaines résultats ont été obtenus et publiés avec Predrag Janicic et Vesna Marinkovic de l'Université de Belgrade (Serbie). Le résultat le plus marquant réside dans la preuve algébrique en Maple des statuts de constructibilité à la règle et au compas de deux listes de problèmes de construction connues des mathématiciens américains sous le nom de liste de Wernick et liste de Connelly. Ces listes regroupent environ 270 problèmes de construction à la règle et au compas à partir de points caractéristiques, elles ont été créées de manière systématique à titre d'amusement et de challenge pour les professeurs de mathématique, principalement de lycée, et ont reçu des réponses partielles de divers mathématiciens dans le monde. L'originalité de notre travail est principalement d'avoir développer une méthode pour traiter automatiquement les deux listes et délivrer la statut, en gros constructible ou non constructible à la règle et au compas, de chaque problème. Nous avons à cette occasion mis en oeuvre ce qui fait la singularité de notre approche : nous avons mélangé du raisonnement géométrique formel, implanté sous forme d'un programme Prolog, pour guider la mise en forme et la triangularisation de systèmes algébriques sous forme de chaînes régulières, ces dernières étant traitées par Maple pour obtenir les groupes de Galois correspondant, tout cela a été implanté par un programme Maple. Il convient de noter qu'il s'agit ici de tester la constructibilité et non d'exhiber, éventuellement, une construction. Les dernier résultats de noter équipe dans ce domaine ont consisté à comparer une méthode due à Lebesgue et que nous avons améliorer et une méthode due à Chou et Gao. Un challenge est de tirer parti de cette étude pour avoir une méthode praticable pour des équations de degré 8.