Automatic Verification of Regular Constructions in Dynamic Geometry Systems

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

• Type: Conference
• Year: 2006
• Where: ADG
• Authors: Predrag Janicic, Pedro Quaresma
• Keywords: ADG 2006, Dynamic Geometry, Dynamic Geometry Tools, Geometric Constructions, Mathematics