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



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.


Automated theorem proving, Area Method


Automated theorem proving

TechReport Number


PDF File

Cited by

Year 2010 : 2 citations

 BILLICH, M.: Verification of Geometric Statements in Dynamic Geometry Environment. Usta ad Albim BOHEMICA, ročník X, 2010, číslo 1, s. 1-7.

 Billich, Martin. Deduction And Proving Of Geometric Statements In Interactive Geometry Environment, South Bohemia Mathematical Letters Volume 18, (2010), No. 1, 39-46.