Skip to Main content Skip to Navigation
Conference papers

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

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download
Contributor : Julien Narboux <>
Submitted on : Monday, April 11, 2011 - 2:18:15 PM
Last modification on : Thursday, January 7, 2021 - 3:40:09 PM
Long-term archiving on: : Tuesday, July 12, 2011 - 2:43:49 AM


Files produced by the author(s)




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⟩



Record views


Files downloads