A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

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

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

Citer

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
226 Consultations
401 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More