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

Tuan Minh Pham 1, * Yves Bertot 1 Julien Narboux 2
* Corresponding author
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
Document type :
Conference papers
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download
https://hal.inria.fr/inria-00584918
Contributor : Julien Narboux <>
Submitted on : Monday, April 11, 2011 - 2:18:15 PM
Last modification on : Wednesday, September 12, 2018 - 1:16:40 AM
Long-term archiving on : Tuesday, July 12, 2011 - 2:43:49 AM

File

iccsaConf.pdf
Files produced by the author(s)

Identifiers

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. pp.368-383, ⟨10.1007/978-3-642-21898-9_32⟩. ⟨inria-00584918⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

395

Files downloads

484

Contact


archive-ouverte@inria.fr