A combination of a dynamic geometry software with a proof assistant for interactive formal proofs

Tuan Minh Pham 1 Yves Bertot 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : This paper presents an interface for geometry proving. It is a combination of a dynamic geometry software - Geogebra[11] with a proof assistant - Coq[8]. Thanks to the features of Geogebra, users can create and manipulate geometric constructions, they discover conjectures and interactively build formal proofs with the support of Coq. Our system allows users to construct fully traditional proofs in the same style as the ones in high school. For each step of proving, we provide a set of applicable rules veri ed in Coq for users, we also provide tactics in Coq by which minor steps of reasoning are solved automatically.
Type de document :
Communication dans un congrès
9th International Workshop On User Interfaces for Theorem Provers FLOC'10 Satellite Workshop, Jul 2010, Edinburgh, Scotland, United Kingdom. Elsevier, 2010, Electronic Notes in Theoretical Computer Science (ENTCS)
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00585400
Contributeur : Tuan Minh Pham <>
Soumis le : mardi 12 avril 2011 - 17:21:43
Dernière modification le : mercredi 12 septembre 2018 - 01:16:37
Document(s) archivé(s) le : mercredi 13 juillet 2011 - 02:48:44

Fichier

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

Identifiants

  • HAL Id : inria-00585400, version 1

Collections

INRIA

Citation

Tuan Minh Pham, Yves Bertot. A combination of a dynamic geometry software with a proof assistant for interactive formal proofs. 9th International Workshop On User Interfaces for Theorem Provers FLOC'10 Satellite Workshop, Jul 2010, Edinburgh, Scotland, United Kingdom. Elsevier, 2010, Electronic Notes in Theoretical Computer Science (ENTCS). 〈inria-00585400〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

407

Téléchargements de fichiers

338

Contact


archive-ouverte@inria.fr