Contribution: AreaMethod

The Chou, Gao and Zhang area method

Authors

Description

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)

Keywords

geometry chou gao zhang area method decision procedure automatic theorem proving

README

            Implementation of the Area Method
                 Julien Narboux
             University of Strasbourg             

This contribution consists in the formalization of a decision procedure for constructive theorems in Euclidean plane geometry. The procedure implemented is the area method by Chou, Gao and Zhang. 

More than 100 example theorems are available among them:

- Ceva
- Desargues
- Pappus
- Menelaus
- Gauss line
- Euler line
- Centroïd
- Pascal
- Napoleon

More information about this implementation is available at :

http://dpt-info.u-strasbg.fr/~narboux/area_method.html

History:
2004 : implementation of the method for affine plane geometry
2009 : extension of the implementation to deal with euclidean geometry

References:
__________

Chou, Gao and Zhang - Machine Proofs in Geometry, Automated Production of Readable Proofs for Geometry Theorems, World Scientific 1994.

Julien Narboux - A decision procedure for geometry in Coq, Proceedings of TPHOLs'2004,Slind Konrad and Bunker Annett and Gopalakrishnan Ganesh editors, LNCS 3223, Springer-Verlag 2004.

Julien Narboux - Thèse : Formalisation et automatisation du raisonnement géométrique, 2006.

Predrag Janicic and Julien Narboux, and Pedro Quaresma - The Area Method : a recapitulation, submitted, 2009.

Available files