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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [11 references]  Display  Hide  Download
https://hal.inria.fr/inria-00585400
Contributor : Tuan Minh Pham <>
Submitted on : Tuesday, April 12, 2011 - 5:21:43 PM
Last modification on : Wednesday, September 12, 2018 - 1:16:37 AM
Document(s) archivé(s) le : Wednesday, July 13, 2011 - 2:48:44 AM

File

paper8.pdf
Files produced by the author(s)

Identifiers

  • 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〉

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

414

Files downloads

351

Contact


archive-ouverte@inria.fr