Formalisation et
automatisation du raisonnement géométrique en Coq.
Soutenance
La soutenance a eu lieu le
mardi 26 septembre 2006
à 14h30, au LRI (Laboratoire de Recherche en Informatique de l'Université
Paris-Sud).
Devant la commission d'examen composée de :
Téléchargement
La version actuelle
est disponible en :
- portable document format [.pdf]
(3.6 Mo)
- postscript [.ps]
(35 Mo)
Les transparents se trouvent
ici.
- Développements Coq
associés :
GeoProof est
disponible
ici.
Résumé
L'objet de cette
thèse est la formalisation et l'automatisation du
raisonnement géométrique au sein de l'assistant
de preuve Coq.
Dans une première partie, nous réalisons un tour
d'horizon des principales axiomatiques de la
géométrie puis nous présentons une
formalisation des huit premiers chapitres du livre de
Schwabäuser, Szmielew et Tarski: Metamathematische Methoden in
der Geometrie.
Dans la seconde partie, nous présentons l'implantation en
Coq d'une procédure de décision pour la
géométrie affine plane : la méthode
des aires de Chou, Gao et Zhang. Cette méthode produit des
preuves courtes et lisibles.
Dans la troisième partie, nous nous intéressons
à la conception d'une interface graphique pour la preuve
formelle en géométrie : Geoproof.
GeoProof combine un logiciel de géométrie
dynamique avec l'assistant de preuve Coq.
Enfin, nous proposons un système formel diagrammatique qui
permet de formaliser des raisonnements dans le domaine de la
réécriture abstraite. Il est par exemple possible
de
formaliser dans ce système la preuve diagrammatique du lemme
de Newman. La correction et la complétude du
système sont prouvées vis-à-vis d'une classe de formules
appelée logique cohérente.
Mots clefs : géométrie,
formalisation, automatisation, Coq, axiomatique de Tarski,
procédure de décision, méthode des
aires, diagrames, logique cohérente,
réécriture abstraite,
géométrie dynamique.
Abstract
This thesis deals with the formalization and automation of geometric
reasoning within the Coq proof assistant.
In the first part, we provide an overview of the main axiom systems for
geometry and we present a mechanization of the geometry of Tarski. This
consists in the formalization of the first eight chapters of the book of
Schwabäuser, Szmielew and Tarski: Metamathematische Methoden in
der Geometrie.
In the second part, we present our implementation in Coq of a decision
procedure for affine plane geometry: the area
method of Chou, Gao and Zhang. This method produces short and readable
proofs.
In the third part, we explain the design of graphical user interface
for formal proof in geometry: GeoProof. GeoProof combines a
dynamic geometry software with the Coq proof assistant.
Finally, we propose a diagrammatic formal system to perform proofs in
the field of abstract term rewriting. For instance, using this system
we can formalize the diagrammatic proof of the Newman's lemma. The
system is proved correct and complete for a class of formulas called the
coherent logic.
Keywords: geometry,
formalization, automation, Coq, Tarski's axiom system, decision
procedure, area method, diagrams, coherent logic, abstract rewriting,
dynamic geometry.