Geometry with its formal, logical and spatial properties is well suited to be taught in an environment that includes dynamic geometry software (DGSs), geometry automated theorem provers (GATPs) and repositories of geometric problems (RGPs). With the integration of those tools in a given learning environment the student is able to explore the built-in knowledge, but also to do new constructions, and to test new conjectures. In such an environment the student can visualise geometric objects and link the formal, axiomatic, nature of geometry with its standard models and corresponding illustrations, e.g., Euclidean Geometry and the Cartesian model. With the help of a geometry automated theorem prover it is possible to check the correctness of the constructions, e.g. if two given lines are parallel, and also to make formal proofs of geometric conjectures. Automated theorem proving in geometry has two major lines of research: synthetic proof style and algebraic proof style [1, 13]. Algebraic proof style methods are based on reducing geometric properties to algebraic properties expressed in terms of Cartesian coordinates. These methods are usually very efficient, but the proofs they produce do not reflect the geometrical nature of the problem and they give only yes or no conclusion. Synthetic methods attempt to automate traditional geometry proof methods, producing human-readable proofs but they are inefficient [7]. The area method and the full-angle method are two semi-synthetic methods providing traditional (not coordinate-based), human-readable proofs. The proofs are expressed in terms of higher-level geometric lemmas and expression simplifications. The main idea of the method is to express the hypotheses of a theorem using a set of constructive statements, each of them introducing a new point or a new line, and to express the conclusion by an equality of expressions in some geometric quantities (e.g. the signed area of a triangle), without referring to Cartesian coordinates. The proof is then based on eliminating (in reverse order) the points and/or lines introduced before, using a set of appropriate lemmas for that purpose. After eliminating all introduced elements, the current goal becomes an equality between two expressions in quantities over independent points. If it is trivially true, then the original conjecture was proved valid, if it is trivially false, then the conjecture was proved invalid, otherwise, the conjecture has been neither proved nor disproved [3, 4, 5]. The following simple example briefly illustrates some key features of this type of methods.
Example 1.1 Two circles o and q meet in two points A and B. A line passing through A meets circles o and q in C and E. A line passing through B meets circles o and q in D and F. Show that CD k EF.
This result can be stated and proved, within the full-angle method realm.
The Construction. The points O and Q, the centres of the circles o and q respectively, are free points, i.e. they are implicitly universally quantified, points not defined by construction steps. The point A and B are given by the intersection of the two circles, the lines a and b are two lines containing A and B respectively and points C to F are the intersections of lines a and b with the circles with centre in O and Q (see Figure 1).
For this problem, an initial non-degeneracy condition is that the two circles must intersect.
The Conjecture. Proving that CD k EF amounts to prove that the full-angle defined by CD and EF is
the angle 6 [0]. This conjecture could also be expressed within the area method settings but there the four
cases seen in figure 1 should be considered [
The Proof. Proving the conjecture goes by eliminating all the constructed points and/or lines, in reverse
order, using for that purpose the properties of the geometric quantities, until an equality in only the free
points is reached. If the equality is provable, then the original conjecture is a theorem as well. For
the given example the Java Geometry Expert (JGEX)1 is able to prove this theorem in very few steps,
justifying each of them by lemmas of the full-angle method [
While the area method introduces the geometric quantities ratio of parallel directed segments, the signed
area and Pythagoras difference [
Definition 2.1 (Full-angle) A full-angle consists of an ordered pair of lines l and m and is denoted by 6 [l; m]. Two full-angles 6 [l; m] and 6 [u; v] are equal if there exists a rotation K such that K(l)ku and K(m)kv.
New constructive statements and several elimination lemmas are introduced to cope with this new
geometric quantity. Its application runs along the same lines as the area method [
At the semantic level the full-angle method does not add anything new, because every conjecture expressed using full-angles can be expressed using geometric quantities of the area method. The real benefit of the full-angle method is more expressiveness, given the fact that a conjecture could be expressed using angles and circles.
The added expressiveness of the full-angle method, allowing it to prove conjectures involving circles and angles, and the fact that the proofs produced with this method are more alike the way mathematicians prove geometry theorems and therefore more human-readable and usually shorter are important issues when we consider the use of GATPs in education. The foreseen integration of the GATP into a DGS is also a very important issue given the fact that the two programs can complement themselves, allowing a richer setting for education.
Consider the following example: Example 2.1 In triangle ABC, two altitudes AD and BE meet in H. G is the foot of perpendicular from point H to AB. Show that 6 [DG;GH] = 6 [HG;GE].
Once more, if we do not use full-angles, we must give proofs for both cases of figure 2. Here the
conjecture is expressed as an equality of two full-angles, this cannot be express, at least as it is, with the
area method geometric quantities [
Again the Java Geometry Expert is able to prove this theorem in very few steps [
In both cases (examples 1.1 and 2.1) a theorem prover based in the area method is not capable of proving the conjectures or it will produce very long proofs, e.g. the GCLC2 is unable to prove any of the two theorems, the first because it exceed the time limit, already with a huge proof record, the second because it is out of scope of the prover. 2.1
Implementation
The OpenGeoProver3 is an open source project, aiming to implement various geometry automated
theorem provers. It can be used as a stand-alone tool but can also be integrated into other geometry tools, such
as dynamic geometry software, e.g., work is being made to integrate OpenGeoProver with GeoGebra [
Concerning the full-angle method implementation in OpenGeoProver, a development branch already exists. The analysis of the existing code is currently being done, e.g., the parser and the data structure that holds a constructive geometry statement. The next step will be to change the parser to accept full-angles and later implement all the needed properties and elimination lemmas.
Other implementations of the full-angle method exist, but to the best of our knowledge, the only ones are those by the original authors, namely the one in JGEX, and the one by Wilson and Fleuriot in the Geometry Explorer [12]. 3
Geometry with its very strong and appealing visual contents and its also strong and appealing connection between the visual content and its formal specification, is an area where computational tools can enhance, in a significant way, the learning environments.
Dynamic geometry software systems significantly help students to acquire knowledge about
geometric objects and, more generally, to acquire mathematical rigour. The geometry automated theorem
provers capable of construction validation and production of human readable proofs, will consolidate
the knowledge acquired with the use of the DGSs. If the GATP produces synthetic proofs, the proof of
a conjecture or the proof of soundness of a construction can be used as an object of study, providing a
logical explanation. We claim that the GATPs can be used in the learning process [
The full-angle method implementation within OpenGeoProver’s is part of the Web Geometry
Laboratory (WGL) project, an adaptive and collaborative blended-learning Web-environment, integrating
dynamic geometry systems and geometry automated theorem provers. The implementation of the
collaborative module is already done and it is currently being tested with case-studies inside the classroom
and also outside the classroom. The adaptive module is the next step and the integration of the GATP
in this environment will be made as soon as possible. The need of a GATP, implementing a synthetic
method, capable of short and easy to follow by students proofs, is very important. The integration of the
OpenGeoProver’s full-angle method prover into the Web Geometry Laboratory will allow students to
explore the connection between the visual content and its formal specification, consolidating the geometric
knowledge of the students [
3https://code.google.com/p/open-geo-prover/