A Symbolic Dynamic Geometry System Using the Analytical Geometry Method
- PDF / 3,074,677 Bytes
- 34 Pages / 547.087 x 737.008 pts Page_size
- 83 Downloads / 212 Views
Mathematics in Computer Science
A Symbolic Dynamic Geometry System Using the Analytical Geometry Method Philip Todd
Received: 20 December 2018 / Revised: 18 November 2019 / Accepted: 29 April 2020 © Springer Nature Switzerland AG 2020
Abstract A symbolic geometry system such as Geometry Expressions can generate symbolic measurements in terms of indeterminate inputs from a geometric figure. It has elements of dynamic geometry system and elements of automated theorem prover. Geometry Expressions is based on the analytical geometry method. We describe the method in the style used by expositions of semi-synthetic theorem provers such as the area method. The analytical geometry method differs in that it considers geometry from a traditional Euclidean/Cartesian perspective. To the extent that theorems are proved, they are only proved for figures sufficiently close to the given figure. This clearly has theoretical disadvantages, however they are balanced by the practical advantage that the geometrical model used is familiar to students and engineers. The method decouples constructions from geometrical measurements, and thus admits a broad variety of measurement types and construction types. An algorithm is presented for automatically deriving simple forms for angle expressions and is shown to be equivalent to a class of traditional proofs. A semiautomated proof system comprises the symbolic geometry system, a CAS and the user. The user’s inclusion in the hybrid system is a key pedagogic advantage. A number of examples are presented to illustrate the breadth of applicability of such a system and the user’s role in proof. Keywords Automatic theorem proving · Dynamic geometry · Symbolic geometry Mathematics Subject Classification Primary 68T15; Secondary 51-04
1 Introduction Dynamic geometry software has seen widespread use in high school mathematics education, starting in the mid 80’s with successful commercial packages [7,10,13], and latterly with broadly comparable, but free, open-source software [6]. Symbolic computation first became commercially available in the ‘80s, while strongly adopted at the university level, has had more limited uptake in the high school. Automated theorem provers for Euclidean Geometry date back further but have been an area of academic research. Wholly algebraic provers based on Wu’s This material is based upon work supported, in part, by the National Science Foundation under Grant IIP-0750028. P. Todd (B) Saltire Software, 12700 SW Hall Blvd., Tigard, OR 97223, USA e-mail: [email protected]
P. Todd
Method [3,17] or Groebner Bases [2,9] give yes/no answers to the correctness of a geometric statement, along with non-degenerate conditions. Semi-synthetic methods, such as the area and full angle methods [4], and the mass point method [18] give human readable proofs, some of which are quite short and worth reading. Recent work [1] has added theorem proving to dynamic geometry systems. An interesting question is what educational value such capabilities will confer on the user. The pedagogic e
Data Loading...
