coq-area-method

The Chou, Gao and Zhang area method. This contribution is the implementation of the Chou, Gao and Zhang's area method decision procedure for euclidean plane geometry. This development contains a partial formalization of the book "Machine Proofs in Geometry, Automated Production of Readable Proofs for Geometry Theorems" by Chou, Gao and Zhang. The examples shown automatically (there are more than 100 examples) includes the Ceva, Desargues, Menelaus, Pascal, Centroïd, Pappus, Gauss line, Euler line, Napoleon theorems. Changelog 2.1 : remove some not needed assumptions in some elimination lemmas (2010) 2.0 : extension implementation to Euclidean geometry (2009-2010) 1.0 : first implementation for affine geometry (2004)

opam install coq-area-method.8.5.0
homepage
https://github.com/coq-contribs/area-method
license
Proprietary
bugs tracker
https://github.com/coq-contribs/area-method/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/area-method/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-area-method/coq-area-method.8.5.0