Je présenterai d'une part un système formel qui permet de faire des preuves diagrammatiques dans le cadre de la réécriture abstraite. Le système proposé est correct et complet vis à vis d'une classe de formules appelée "logique cohérente" par Marc Bezem et Thierry Coquant. Il permet de formaliser des raisonnements diagrammatiques (comportant des inductions) comme la preuve de Huet du lemme de Newman par exemple.

D'autre part je présenterai mon protoptype de logiciel de preuve formelle interactive en géométrie appelé Geoproof.

GeoProof combine :

• un logiciel de géométrie dynamique pour explorer une figure et réaliser des conjectures,
• un système de preuve automatique (basé sur des procédures de décision implantées par John Harrison)
• un système de preuve interactive (Coq).

  Enfin je montrerai le lien qui existe entre ces deux thématiques.