Package: wnpp Severity: wishlist Owner: Riley Baird <bm-2cvqnduybau5do2dfjtrn7zbaj246s4...@bitmessage.ch>
* Package name : coq-areamethod Version : 8.4+20150823 Upstream Author : Julien Narboux <narb...@unistra.fr> * URL : http://dpt-info.u-strasbg.fr/~narboux/area_method.html * License : GPL-2+ Programming Lang: Coq Description : coq library for the area method decision procedure This library is a coq implementation of the Area Method decision procedure described by Shang-Ching Chou, Xiao-Shan Gao and Jing-Zhong Zhang in their 1994 book "Machine Proofs in Geometry". This package contains more than 100 example theorems which can be proved using the area method, such as: -Ceva -Desargues -Menelaus -Pappus -Pascal's axiom -Gauss line -Nine points circle -Euler line