The Full Angle Method on the OpenGeoProver Nuno Baeta Pedro Quaresma ISEC, Polytechnic Institute of Coimbra CISUC, University of Coimbra Coimbra, Portugal Coimbra, Portugal nmsb@isec.pt pedro@mat.uc.pt 1 Introduction 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 envi- ronment 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 c Baeta, Nuno & Quaresma, Pedro Submitted to: This work is licensed under the THedu’13 Creative Commons Attribution License. 2 Readable Proofs in Geometry 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. Figure 1: Illustration of Example 1.1 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 [2]. 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 [2]. 6 [DC,EF] = 6 [CD,DB] + 6 [DB,EF] = 6 [DB,EF] + 6 [CA,AB] = −6 [EA,AB] + 6 [CA,AB] = −6 [EA,AB] + 6 [EA,AB] = 6 [0] Q.E.D. 2 The Full-Angle Method While the area method introduces the geometric quantities ratio of parallel directed segments, the signed area and Pythagoras difference [3, 5] the full-angle method introduces the notion of full-angle [4]. 1 http://www.cs.wichita.edu/ ˜ye/index.html Baeta, Nuno & Quaresma, Pedro 3 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 [2, 3, 4]. 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 ex- pressed 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]. Figure 2: Illustration of Example 2.1 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 [2]. Again the Java Geometry Expert is able to prove this theorem in very few steps [2]. In order to prove that 6 [EG,GH] = 6 [HG,GD] we prove that 6 [HG,GE] + 6 [HG,GD] = 6 [0]. 6 [HG,GE] + 6 [HG,GD] = 6 [HG,GD] − 6 [EG,GD] + 6 [HG,GD] = −6 [EG,GD] − 26 [GD,BA] = −6 [GD,BA] + 6 [HA,AE] − 6 [1] = −6 [DH,HB] + 6 [HA,AE] − 6 [1] = −6 [HB,EA] − 6 [1] = 6 [1] − 6 [1] = 6 [0] Q.E.D. 4 Readable Proofs in Geometry 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 theo- rem 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 [8]. In its current state, OpenGeoProver implements two algebraic methods, the characteristic method, also known as Wu’s method, and the Gröbner basis method, as well as one semi-synthetic method, the area method. 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 Conclusions & Future Work 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 geo- metric 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 [6, 9, 10, 11]. The full-angle method implementation within OpenGeoProver’s is part of the Web Geometry Lab- oratory (WGL) project, an adaptive and collaborative blended-learning Web-environment, integrating dynamic geometry systems and geometry automated theorem provers. The implementation of the col- laborative 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 ex- plore the connection between the visual content and its formal specification, consolidating the geometric knowledge of the students [10, 11]. 2 http://poincare.matf.bg.ac.rs/ ˜janicic/gclc/ 3 https://code.google.com/p/open-geo-prover/ Baeta, Nuno & Quaresma, Pedro 5 References [1] Shang-Ching Chou & Xiao-Shan Gao (2001): Automated Reasoning in Geometry. In: Handbook of Auto- mated Reasoning, Elsevier and MIT Press, pp. 707–749. [2] Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (1994): Machine Proofs in Geometry. Series on Applied Mathematics 6, World Scientific. [3] Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (1996): Automated Generation of Readable Proofs with Geometric Invariants, I. Multiple and Shortest Proof Generation. Journal of Automated Reasoning 17(13), pp. 325–347, doi:10.1007/BF00283133. [4] Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (1996): Automated Generation of Readable Proofs with Geometric Invariants, II. Theorem Proving With Full-Angles. Journal of Automated Reasoning 17(13), pp. 349–370, doi:10.1007/BF00283134. [5] Predrag Janičić, Julien Narboux & Pedro Quaresma (2012): The Area Method: A Recapitulation. Journal of Automated Reasoning 48(4), pp. 489–532, doi:10.1007/s10817-010-9209-7. [6] Predrag Janičić & Pedro Quaresma (2007): Automatic Verification of Regular Constructions in Dynamic Geometry Systems. In Francisco Botana & Tomás Recio, editors: Automated Deduction in Geometry, Lecture Notes in Computer Science 4869, Springer, pp. 39–51, doi:10.1007/978-3-540-77356-6 3. [7] Jianguo Jiang & Jingzhong Zhang (2012): A review and prospect of readable machine proofs for geometry theorems. Journal of Systems Science and Complexity 25, pp. 802–820, doi:10.1007/s11424-012-2048-3. Available at http://dx.doi.org/10.1007/s11424-012-2048-3. [8] Ivan Petrović & Predrag Janičić (2012): Integration of OpenGeoProver with GeoGebra. Available at http: //argo.matf.bg.ac.rs/events/2012/fatpa2012/slides/IvanPetrovic.pdf. [9] Pedro Quaresma & Predrag Janičić (2006): Integrating Dynamic Geometry Software, Deduction Sys- tems, and Theorem Repositories. In Jonathan M. Borwein & William M. Farmer, editors: Mathe- matical Knowledge Management, Lecture Notes in Artificial Intelligence 4108, Springer, pp. 280–294, doi:10.1007/11812289 22. [10] Vanda Santos & Pedro Quaresma (2012): Integrating DGSs and GATPs in an Adaptative and Collaborative Blended-Learning Web-Environment. In: First Workshop on CTP Components for Educational Software (THedu’11), EPTCS 79, pp. 111–123, doi:10.4204/EPTCS.79.7. [11] Vanda Santos & Pedro Quaresma (2013): Collaborative Aspects of the WGL Project. Electronic Journal of Mathematics & Technology. (to appear). [12] Sean Wilson & Jacques Fleuriot (2005): Combining Dynamic Geometry, Automated Geometry Theorem Proving And Diagrammatic Proofs. Workshop User Interfaces for Theorem Provers (UITP 2005). [13] Wen-Tsun Wu (1984): Automated Theorem Proving: After 25 Years, chapter On the decision problem and the mechanization of theorem proving in elementary geometry, pp. 213–234. Contemporary Mathematics 29, American Mathematical Society.