HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

A Decision Procedure for Geometry in Coq

Julien Narboux 1, 2
2 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : We present in this paper the development of a decision procedure for affine plane geometry in the Coq proof assistant. Among the existing decision methods, we have chosen to implement one based on the area method developed by Chou, Gao and Zhang, which provides short and ``readable'' proofs for geometry theorems. The idea of the method is to express the goal to be proved using three geometric quantities and eliminate points in the reverse order of their construction thanks to some elimination lemmas.
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

Contributor : Julien Narboux Connect in order to contact the contributor
Submitted on : Monday, January 16, 2006 - 2:55:40 PM
Last modification on : Friday, February 4, 2022 - 3:23:50 AM
Long-term archiving on: : Saturday, April 3, 2010 - 9:26:18 PM


Distributed under a Creative Commons Attribution - NonCommercial - NoDerivatives 4.0 International License



Julien Narboux. A Decision Procedure for Geometry in Coq. Theorem Proving in Higher Order Logics 2004, Jul 2004, Park City, USA, United States. pp.225-240, ⟨10.1007/b100400⟩. ⟨inria-00001035⟩



Record views


Files downloads