A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

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.
Fichier principal
Vignette du fichier
iccsaConf.pdf (474.76 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00584918 , version 1 (11-04-2011)

Identifiers

Cite

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⟩

Collections

CNRS INRIA INRIA2
218 View
365 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More