A Symbolic Dynamic Geometry System Using the Analytical Geometry Method

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 semi-automated 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.