| HAL-Inria | Publications, software ... of Inria's scientists |
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.
Cited literature [14 references]
https://hal.inria.fr/inria-00584918
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
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
File
iccsaConf.pdf
Files produced by the author(s)