A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry

Tuan Minh Pham 1, * Yves Bertot 1 Julien Narboux 2
* Auteur correspondant
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 LSIIT - Laboratoire des Sciences de l'Image, de l'Informatique et de la Télédétection
Abstract : In this article, we present the development of a library of formal proofs for theorem proving in plane geometry in a pedagogical context. We use the Coq proof assistant. This library includes the basic geometric notions to state theorems and provides a database of theorems to construct interactive proofs more easily. It is an extension of the library of F. Guilhot for interactive theorem proving at the level of high-school geometry, where we eliminate redundant axioms and give formalizations for the geometric concepts using a vector approach. We also enrich this library by offering an automated deduction method which can be used as a complement to interactive proof. For that purpose, we integrate the formalization of the area method which was developed by J. Narboux in Coq.
Keywords : formalization geometry Coq area method dynamic geometry
Type de document :
Communication dans un congrès
The 11th International Conference on Computational Science and Its Applications (ICCSA 2011), Jun 2011, Santander, Spain. Springer-Verlag, 6785, pp.368-383, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-21898-9_32〉
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00584918
Contributeur : Julien Narboux <>
Soumis le : lundi 11 avril 2011 - 14:18:15
Dernière modification le : mercredi 12 septembre 2018 - 01:16:40
Document(s) archivé(s) le : mardi 12 juillet 2011 - 02:43:49

Fichier

iccsaConf.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA

Citation

Tuan Minh Pham, Yves Bertot, Julien Narboux. A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry. The 11th International Conference on Computational Science and Its Applications (ICCSA 2011), Jun 2011, Santander, Spain. Springer-Verlag, 6785, pp.368-383, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-21898-9_32〉. 〈inria-00584918〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

359

Téléchargements de fichiers

402

Contact


archive-ouverte@inria.fr