Coq OPAMcoq-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.6.0
- homepage
- https://github.com/coq-contribs/area-method
- license
- Unknown
- bugs tracker
- https://github.com/coq-contribs/area-method/issues
- dependencies
- coq (>= 8.6 & < 8.7~)
- source
- https://github.com/coq-contribs/area-method/archive/v8.6.0.tar.gz
- package
- https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-area-method/coq-area-method.8.6.0