Automatic Verification of Regular Constructions in Dynamic Geometry Systems
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
- PDF / 416,962 Bytes
- 13 Pages / 430 x 660 pts Page_size
- 84 Downloads / 231 Views
Faculty of Mathematics, University of Belgrade Studentski trg 16, 11000 Belgrade, Serbia [email protected] Department of Mathematics, University of Coimbra 3001-454 Coimbra, Portugal [email protected]
Abstract. 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.
1
Introduction
Dynamic geometry software (e.g., Cinderella, [24,26], Geometer’s Sketchpad, [10,27] Cabri, [14,25]) visualise geometric objects and link formal, axiomatic nature of geometry (most often — Euclidean) with its standard models (e.g., Cartesian model) and corresponding illustrations. The common experience is that dynamic geometry software significantly helps students to acquire knowledge about geometric objects and, more generally, for acquiring mathematical rigour. However, most (if not all) of these programs use only geometric concepts interpreted via concrete instances in Cartesian plane. Namely, a construction is always associated with concrete fixed points (with concrete Cartesian coordinates). In such environments, some constructions (usually by ruler and compass) are illegal (e.g., if they attempt to use the intersection of two parallel lines), but
This work was partially supported by Serbian Ministry of Science and Technology grant 144030. Also, partially supported by the programme POSC, by the Centro International de Matem´ atica (CIM), under the programme “Research in Pairs”, while visiting Coimbra University under the Coimbra Group Hospitality Scheme. This work was partially supported by programme POSC.
F. Botana and T. Recio (Eds.): ADG 2006, LNAI 4869, pp. 39–51, 2007. c Springer-Verlag Berlin Heidelberg 2007
40
P. Janiˇci´c and P. Quaresma
the question if such construction is always illegal or it is illegal only for given particular fixed points is left open (if a construction is always possible, we will call it regular). Indeed, for answering such question, one has to use deductive reasoning, and not only a semantic check for the special case. Consider one simple example: given (by Cartesian coordinates) three fixed distinct points A, B, C, we can construct a point D as an image of point C in translation TAB ; later on, if we try to construct an intersection of lines AC and BD, we will discover that
Data Loading...
