zbMATH — the first resource for mathematics

Automatic verification of regular constructions in dynamic geometry systems. (English) Zbl 1195.68092
Botana, Francisco (ed.) et al., Automated deduction in geometry. 6th international workshop, ADG 2006, Pontevedra, Spain, August 31–September 2, 2006. Revised papers. Berlin: Springer (ISBN 978-3-540-77355-9/pbk). Lecture Notes in Computer Science 4869. Lecture Notes in Artificial Intelligence, 39-51 (2007).
Summary: We present an application of 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 to deal with syntactic errors. 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 do not 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 ATP, we can do this last step by verifying the geometric constructions deductively. We have developed a system for the automatic verification of regular constructions (made within DGSs GCLC and Eukleides), using our ATP system, GCLCprover. This gives a real-world application of ATP in dynamic geometry tools.
For the entire collection see [Zbl 1132.68006].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
51-04 Software, source code, etc. for problems pertaining to geometry
68U05 Computer graphics; computational geometry (digital and algorithmic aspects)
Full Text: DOI