Paper Info
Title
A Decision Procedure for Geometry in Coq
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.
Year
DOI
Venue
2004
10.1007/978-3-540-30142-4_17
Lecture Notes in Computer Science
Field
DocType
Volume
Affine transformation,Affine geometry,Plane (geometry),Computer science,Automated theorem proving,Algorithm,Mathematical proof,Geometry,Lemma (mathematics),Proof assistant,Formal proof
Conference
3223
ISSN
Citations 
PageRank 
0302-9743
23
1.68
References 
Authors
6
1
Name
Order
Citations
PageRank
Julien Narboux113012.49