GitHub - jnarboux/area-method: The Chou, Gao and Zhang area method

jnarboux / area-method Public

forked from rocq-archive/area-method

Notifications You must be signed in to change notification settings
Fork 0
Star 0

The Chou, Gao and Zhang area method

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 33 Commits
Make		Make
Makefile		Makefile
README		README
Rgeometry_tools.v		Rgeometry_tools.v
advanced_parallel_lemmas.v		advanced_parallel_lemmas.v
area_coords_constructions.v		area_coords_constructions.v
area_coords_elimination.v		area_coords_elimination.v
area_elimination_lemmas.v		area_elimination_lemmas.v
area_method.v		area_method.v
basic_geometric_facts.v		basic_geometric_facts.v
bench_normalization_tactics.v		bench_normalization_tactics.v
chou_gao_zhang_axioms.v		chou_gao_zhang_axioms.v
constructed_points_elimination.v		constructed_points_elimination.v
construction_lemmas.v		construction_lemmas.v
construction_lemmas_2.v		construction_lemmas_2.v
construction_tactics.v		construction_tactics.v
description		description
elimination_prepare.v		elimination_prepare.v
euclidean_constructions.v		euclidean_constructions.v
euclidean_constructions_2.v		euclidean_constructions_2.v
examples_1.v		examples_1.v
examples_2.v		examples_2.v
examples_3.v		examples_3.v
examples_4.v		examples_4.v
examples_5.v		examples_5.v
examples_6.v		examples_6.v
examples_centroid.v		examples_centroid.v
examples_circumcenter.v		examples_circumcenter.v
examples_interactive.v		examples_interactive.v
field.v		field.v
field_general_properties.v		field_general_properties.v
field_variable_isolation_tactic.v		field_variable_isolation_tactic.v
free_points_elimination.v		free_points_elimination.v
free_points_elimination_py.v		free_points_elimination_py.v
freepoints.v		freepoints.v
general_tactics.v		general_tactics.v
geometry_tools.v		geometry_tools.v
geometry_tools_lemmas.v		geometry_tools_lemmas.v
my_field_tac.v		my_field_tac.v
parallel_lemmas.v		parallel_lemmas.v
py_elimination_lemmas.v		py_elimination_lemmas.v
pythagoras_difference.v		pythagoras_difference.v
pythagoras_difference_lemmas.v		pythagoras_difference_lemmas.v
ratios_elimination_lemmas.v		ratios_elimination_lemmas.v
simplify_constructions.v		simplify_constructions.v
tests_elimination_tactics_areas.v		tests_elimination_tactics_areas.v
tests_elimination_tactics_py.v		tests_elimination_tactics_py.v
tests_elimination_tactics_ratios.v		tests_elimination_tactics_ratios.v

Repository files navigation

            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.