Framework for Constructive Geometry (Based on the Area Method)

Authors

Abstract

In this technical report we present a rational reconstruction of the area method (developed by Chou, Gao and Zhang) for automated theorem proving for Euclidean geometry. Our rational reconstruction covers all relevant lemmas proved in full details and also full details of required algebraic reasoning (missing from the papers introducint the area method). We also present our implementation of this algorithm, made within the program GCLC.

The area method main idea is to express the hypothesis of a theorem using a set of constructive statements each of then introducing a new point, and to express the conclusion by a polynomial in a some geometry quantities, without any relation to a given system of coordinates. The proof is then developed by eliminating, in reverse order, the point introduced before, using for that purpose a set of lemmas. After eliminating all the introduced points the polynomial is just an equality between two rational expression in independent variables. Hence if they are equal the statement is true, otherwise it is false.

The proofs generated by the prover (developed as a part of GCLC) are generally short and readable. The program can prove many non-trivial theorems in a very efficient way.

Keywords

automated theorem proving, Euclidian geometry, coordinate-free methods, area method

Subject

Automated theorem proving

PDF File