Computer aided proving in geometry

Zlatan Magajna
[email protected]
Pedagoška fakulteta, Univerza v Ljubljani

Povzetek delavnice

V delavnici bomo spoznali osnove programa OK Geometry za analiziranje dinamičnih geometrijskih konstrukcij. Predstavili bomo različici programa, ki sta namenjeni dijakom in učiteljem matematike.

• Prikazali bomo preprosto analizo geometrijskih konstrukcij, ki jih izdelamo z znanimi programi za dinamično geometrijo: Cabri Geometry, GeoGebra ali Cinderella.  Iz katerega od navedenih programov bom uvozili geometrijsko konstrukcijo v OK Geometry, tu pa nas bo program opozoril na številne lastnosti (npr. skladnost kotov, skladnost trikotnikov, sorazmerje dolžin.), ki bi jih brez programa zlahka spregledali.
• V preprosti različici programa OK Geometry bomo tudi predstavili, kako dijaki lahko izdelajo geometrijski dokaz s pomočjo predloge, ki jo izdela učitelj.
• V nadaljevanju bomo predstavili, kako v programu OK Geometry rešujemo zahtevnejše probleme v ravninske geometrije. Osnovni pristop je ta, da v programu geometrijsko opišemo želeni cilj (npr. trikotnik, ki ustreza danim podatkom). Program skuša doseči cilj (npr. dobiti trikotnik z danimi podatki). Nadaljnja analiza najdene rešitve v OK Geometry nas opozori na mnoge lastnosti želenega cilja, kar nas lahko pripelje do prej nepoznane konstrukcijske rešitve in nemara tudi do dokaza pravilnosti postopka.

Ključne besede
dinamična geometrija, dokazovanje, geometrijske konstrukcije, reševanje geometrijskih problemov

Ciljna skupina: Učitelji matematike v osnovnih in vseh srednjih šolah. (Program OK Geometry je tudi v slovenščini.)

Časovni obseg delavnice:  90 minut.

Abstract

In the workshop we shall present OK Geometry, a computer program for analysing dynamic geometric constructions. Its intention is to facilitate the learning of proving geometry facts. We shall show first a simple use of OK Geometry. In order to prove a geometric property we first construct the related configuration on a dynamic geometry program (Cabry Geometry, GeoGebra or Cinderella). The output is then imported into OK Geometry where we are warned of several potentially relevant facts (e.g. congruent angles, equal cross-ratios). By logically connecting the potentially relevant facts we may build up a proof or find a solution to a problem. We shall also show how to solve more advanced problems, which a user cannot be work out within common programs of dynamic geometry. We try to solve such tasks in OK Geometry as implicit construction. A further analysis within OK Geometry of the obtained solution may lead to a solution of the problem in the sense of an explicit construction or a proof of some fact.

Key words
Dynamic geometry, proving, geometric constructions, solving geometry problems