We present an application of an automatic theorem proving (ATP) in the verification of constructions made with dynamic geometry software (DGS). Given a specification language for geometric constructions, we can use its processor (i.e., a DGS) to deal with syntactic errors (with respect to the underlying language). The processor can also detect semantic errors --- situations when, for a given concrete set of geometrical objects, a construction is not possible. However, dynamic geometry tools don't test if, for a given set of geometrical objects, a construction is geometrically sound, i.e., if it is possible in a general case. Using an ATP, we can do this last step by verifying the geometric construction deductively. We have developed a system for the automatic verification of regular constructions, using our ATP system, GCLCprover, to automatically verify the geometric constructions made with the DGSs GCLC and Eukleides. This gives a real application of ATP in dynamic geometry tools.
Maric, Filip and Petrovic, Ivan and Petrovic, Danijela and Janicic, Predrag, Formalization and Implementation of Algebraic
Methods in Geometry, EPTCS79. 10.4204/EPTCS.79
Year 2010 : 3 citations
Heck, André and Ellermeijer, Ton, Mathematics Assistants: Meeting the Needs of Secondary School Physics Education, Acta Didactica Napocensia, Volume 3, Number 2, 2010.
Billich, Martin. Deduction And Proving Of Geometric Statements In Interactive Geometry Environment, South Bohemia Mathematical Letters Volume 18, (2010), No. 1, 39-46.
Janicic, Predrag, Geometry Constructions Language, JAR 44(1-2). Doi: 10.1007/s10817-009-9135-8
