The Area Method, Rigorous Proofs of Lemmas in Hilbert's Style Axiom System
Pedro Quaresma · 2009
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