Note ABES Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective Combinatorial approach for the automation in Coq of formal proofs in incidence projective geometry Aide à la preuve Automatisation Assistant de preuve Géométrie finie Géométrie projective Mécanisation des preuves Propriété de Desargues Prouveur automatique Théorie des matroïdes Automatic prover Automation Finite geometry Proof assistance Proof mechanization Projective geometry Proof assistant Desargues's property Matroid theory SAT/SMT solvers 005.4 516.5 Assistants de preuve Automatisation Coq (logiciel) Géométrie combinatoire Matroïdes Géométrie projective Ce travail de thèse s’inscrit dans le domaine de la preuve assistée par ordinateur et se place d'un point de vue méthodologique. L’objectif premier des assistants de preuves est de vérifier qu’une preuve écrite à la main est correcte; la question ici est de savoir comment à l’intérieur d’un tel système, il est possible d'aider un utilisateur à fabriquer une preuve formelle du résultat auquel il s'intéresse. Ces questions autour de la vérification de preuves, en particulier en certification du logiciel, et au delà de leur traçabilité et de leur lisibilité sont en effet devenues prégnantes avec l’importance qu’ont prise les algorithmes dans notre société. Bien évidemment, répondre à la question de l’aide à la preuve dans toute sa généralité dépasse largement le cadre de cette thèse. C’est pourquoi nous focalisons nos travaux sur la preuve en mathématiques dans un cadre particulier qui est bien connu dans notre équipe : la géométrie et sa formalisation dans le système Coq. Dans ce domaine, nous mettons premièrement en évidence les niveaux auxquels on peut oeuvrer à savoir le contexte scientifique à travers les méthodes de formalisation mais aussi le contexte méthodologique et technique au sein de l'assistant de preuve Coq. Dans un second temps, nous essayons de montrer comment nos méthodes et nos idées sont généralisables à d'autres disciplines. Nous mettons ainsi en place dans nos travaux les premiers jalons pour une aide à la preuve efficace dans un contexte géométrique simple mais omniprésent. À travers une approche classique fondée sur la géométrie synthétique et une approche combinatoire complémentaire utilisant le concept de rang issu de la théorie des matroïdes, nous fournissons à l'utilisateur des principes généraux et des outils facilitant l'élaboration de preuves formelles. Dans ce sens, nous comparons les capacités d'automatisation de ces deux approches dans le contexte précis des géométries finies avant de finalement construire un prouveur automatique de configuration géométrique d'incidence. This thesis work is part of the general field of computer-assisted proof and is methodologically based. The primary objective of proof assistants is to verify that handwritten demonstration is correct; the question here is how within such a system, it is possible to help a user to make a formal proof of the result in which he is interested. These questions around the verification of proofs, in particular in software certification, and beyond their traceability and readability have indeed become significant with the importance that algorithms have taken on in our society. Obviously, answering the question of proof assistance in all its generality goes far beyond the scope of this thesis. This is why we focus our work on proof in mathematics in a particular framework that is well known in our team: geometry and its formalization in the Coq system. In this field, we first highlight the levels at which we can work, namely the scientific context through the formalization methods but also the methodological and technical context within the Coq proof assistant. In a second step, we try to show how our methods and ideas can be generalized to other disciplines. In this way, we are putting in place the first steps towards effective proof assistance in a simple but omnipresent geometric context. Through a classical approach based on synthetic geometry and a complementary combinatorial approach using the concept of rank from matroid theory, we provide the user with general principles and tools to facilitate the development of formal proof. In this sense, we compare the automation capabilities of these two approaches in the specific context of finite geometries before finally constructing an automatic prover of geometric configurations of incidence. Electronic Thesis or Dissertation Text fr PDF 2136128 Université de Strasbourg Strasbourg 2020-12-31 https://theses.hal.science/tel-02512327 application/pdf 2521731 https://publication-theses.unistra.fr/public/theses_doctorat/2019/Braun_David_2019_ED269.pdf http://www.theses.fr/2019STRAD020/abes https://theses.hal.science/tel-02512327 https://theses.hal.science/tel-02512327 https://theses.hal.science/tel-02512327 Braun David 1991-01-16 FR 243009437 https://theses.fr/2019STRAD020 2019STRAD020 https://doi.org/10.70675/06896948z7d08z4706z887dzea409e7e19aa 2019-09-23 Informatique Strasbourg 131056549 Doctorat Docteur es non oui Schreck Pascal MADS_DIRECTEUR_DE_THESE_1 115931589 Bechmann Dominique MADS_PRESIDENT_DU_JURY 034489886 Schreck Pascal MADS_MEMBRE_DU_JURY_1 115931589 Bechmann Dominique MADS_MEMBRE_DU_JURY_2 034489886 Fleuriot Jacques MADS_MEMBRE_DU_JURY_3 156501007 Michelucci Dominique MADS_MEMBRE_DU_JURY_4 032984189 Théry Laurent MADS_MEMBRE_DU_JURY_5 150293887 Magaud Nicolas MADS_MEMBRE_DU_JURY_6 077385969 Fleuriot Jacques MADS_RAPPORTEUR_1 156501007 Michelucci Dominique MADS_RAPPORTEUR_2 032984189 École doctorale Mathématiques, sciences de l'information et de l'ingénieur (Strasbourg ; 1997-....) MADS_ECOLE_DOCTORALE_1 156504863 Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (Strasbourg ; 2013-....) MADS_PARTENAIRE_DE_RECHERCHE_1 176969721 260728 ddc:004 ddc:510 Schreck Pascal Bechmann Dominique Schreck Pascal Bechmann Dominique Fleuriot Jacques Michelucci Dominique Théry Laurent Magaud Nicolas Fleuriot Jacques Michelucci Dominique École doctorale Mathématiques, sciences de l'information et de l'ingénieur (Strasbourg ; 1997-....) Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (Strasbourg) PDF 2136128