The Area Method, Rigorous Proofs of Lemmas in Hilbert\'s Style Axiom System

Authors

Abstract

The area method for Euclidean constructive geometry was proposed by Chou et al. in early
1990's. The method produces human-readable proofs and can efficiently prove many non-
trivial theorems. It can be considered as one of the most interesting and most successful
methods in geometry theorem proving and probably the most successful in the domain of
automated production of readable proofs.
In this research report, we focus on the rigorous proofs of all the lemmas of the area method.
This text is meant as a support text for the article, The Area Method: a Recapitulation,
by Predrag Janičić, Julien Narboux and Pedro Quaresma, submitted for publication in the
Journal of Automated Reasoning, in October 2009.

Keywords

Automated theorem proving, Area Method

Subject

Automated theorem proving

TechReport Number

2009/006

PDF File