Name
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. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-21898-9_32 | ICCSA (4) |
Keywords | Field | DocType |
automated deduction method,basic geometric notion,formal proof,coq-based library,high-school geometry,plane geometry,interactive proof,geometric concept,coq proof assistant,automated theorem,area method,interactive theorem,geometry,teaching,automation | Programming language,Axiom,Computer science,Plane (geometry),Automated theorem proving,Automated proof checking,Automation,Mathematical proof,Proof assistant | Conference |
Volume | ISSN | Citations |
6785 | 0302-9743 | 5 |
PageRank | References | Authors |
0.53 | 9 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tuan Pham | 1 | 503 | 73.75 |
| Yves Bertot | 2 | 442 | 40.82 |
| Julien Narboux | 3 | 130 | 12.49 |