Eliminációs támogatás a GeoGebra Kapcsolat eszközéhez

Háttér A Kapcsolat Eszköz: El®készületek Alkalmazások

Eliminációs támogatás a GeoGebra Kapcsolat eszközéhez Kovács Zoltán

Szegedi Tudományegyetem, Bolyai Intézet Analízis Tanszék

Johannes Kepler Universität, Linz Institut für Didaktik der Mathematik Research Instute for Symbolic Computations

Bolyai Intézet, PhD szeminárium 2015. szeptember 8.

Kovács Zoltán

Eliminációs támogatás a GeoGebra Kapcsolat eszközéhez


Kivonat Több számítógépes dinamikus geometriai rendszer (DGS) is nyújt támogatást ahhoz, hogy (f®ként euklideszi) geometriai szerkesztések objektumai között kapcsolatokat olvassunk le. Ilyenek lehetnek pl. a párhuzamosság, a mer®legesség vagy az egybevágóság. A GeoGebra 5.0-s változatának Kapcsolat eszköze a korábban is létez® numerikus ellen®rzésen kívül már szimbolikus módon is képes ezen összefüggések leolvasására, valamint olyan szintetikus feltételrendszer megfogalmazására, amellyel precíz geometriai tétel mondható ki. A háttérszámítások a legjobb nyílt forrású megoldásokon (Singular, Giac) alapulnak, melyek Gröbner bázisok segítségével képesek a függ® változókat hatékonyan eliminálni. Az algebrai kimeneteket a GeoGebra végül olyan elegend® feltételekké alakítja, amelyekkel a vizsgált tulajdonság fennállása középiskolások számára is olvasható formájú geometriai tételként jeleníthet® meg. Kovács Zoltán



Áttekintés

1

Háttér

2

A Kapcsolat Eszköz: El®készületek GeoGebra 4.4 Algebrai átírás: Példa Algoritmusok

3

Alkalmazások

Kovács Zoltán



Disszertáció Kooperáció, korábbi munkák Publikációk

Célkit¶zések

1

Lehet-e számítógépes támogatást adni elemi geometriai tételek bizonyításának tanításához? Ha igen, hogyan?

2

Milyen nehézségek léphetnek fel egy alkalmas oktató szoftver létrehozásakor, beleértve 1 2 3

3

a felhasználói interfész tervezését, a tanár és a diák szerepét a szoftver felhasználása során, ill. az alkalmazott algoritmusokat és implementációs problémákat?

Milyen jelleg¶ számítógéppel segített gyakorlófeladatokat lehet a középiskolában alkalmazni ebben a témakörben?

Kovács Zoltán




Kooperáció

M. Hohenwarter (2009) T. Recio (2010) F. Botana (2011) Johannes Kepler Universität, IDM + RISC (2012) B. Parisse (2013)

Kovács Zoltán




Vizsgált módszerek

B. Buchberger, B. Kutzler & S. Stifter (1986); D. Kapur (1986) S. C. Chou (1987)

←

J. Narboux (2007)

W. T. Wu (1978)

←

A. Tarski (1983)

Z. Ye, S. C. Chou & X. S. Gao (2010) T. Recio (2011)

Kovács Zoltán




Komputeralgebra-rendszerek

G. M. Greuel & G. Pster (Singular) B. Parisse (Giac)

Kovács Zoltán




Oktatás

Hajnal I., Némethy K. (1988) M. de Villiers (1990) M. Hohenwarter (GeoGebra, 2001)

Kovács Zoltán




Publikációk (20122013) F. Botana, F., Z. Kovács & S. Weitzhofer (2012).

Implementing theorem proving in GeoGebra by using a Singular webservice. In Proceedings EACA 2012,

Libro de Resúmenes del XIII Encuentro de Álgebra Computacional y Aplicaciones, p. 6770. Univ. Alcalá, Spain.

Implementing theorem proving in GeoGebra by using exact check of a statement in a bounded number of test cases. In Proceedings

Z. Kovács, T. Recio & S. Weitzhofer (2012).

EACA 2012, Libro de Resúmenes del XIII Encuentro de Álgebra Computacional y Aplicaciones, p. 123126. Univ. Alcalá, Spain. G. Ancsin, M. Hohenwarter & Z. Kovács (2013).

GeoGebra goes web. The Electronic Journal of Mathematics and Technology, 7(6):412418.

Kovács Zoltán




Publikációk (2014)

F. Botana & Z. Kovács (2014).

A Singular web service for geometric computations. Annals of Mathematics and Articial Intelligence, p. 112. Z. Kovács (2014). The portfolio prover in GeoGebra 5.

In F. Botana & P. Quaresma (eds.), Proceedings of the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), 9-11 July 2014, p. 191205. Univ. Coimbra, Portugal. M. Hohenwarter, M. Borcherds, G. Ancsin, B. Bencze, M. Blossier, A. Delobelle, C. Denizet, J. Éliás, Á. Fekete, L. Gál, Z. Kone£ný, Z. Kovács, S. Lizelfelner, B. Parisse & G. Sturr (2014).

GeoGebra 5.

Kovács Zoltán




Publikációk (2015) Z. Kovács & B. Parisse (2015). Giac and GeoGebra improved Gröbner basis computations. In J. Gutierrez, J. Schicho & M. Weimann (eds.), Computer Algebra and Polynomials, Lecture Notes in Computer Science, p. 126138. Springer.

F. Botana, M. Hohenwarter, P. Jani£i¢, Z. Kovács, I. Petrovi¢, T. Recio & S. Weitzhofer (2015).

Automated theorem proving in GeoGebra: Current achievements. Journal of Automated Reasoning, 55(1):3959. Z. Kovács (2015). The Relation Tool in GeoGebra 5. In F. Botana & P. Quaresma (eds.), Post-conference Proceedings of

the 10th International Workshop on Automated Deduction in Geometry (ADG 2014), 9-11 July 2014, Lecture Notes in Computer Science, p. 5371. Springer. Kovács Zoltán



GeoGebra 4.4 Algebrai átírás: Példa Algoritmusok

Outline

1

Háttér

2


3

Alkalmazások

Kovács Zoltán




A Kapcsolat Eszköz a GeoGebra 4.4-ben

Kovács Zoltán




A Kapcsolat Eszköz a GeoGebra 4.4-ben (Nyomvonal)

Kovács Zoltán




A Kapcsolat Eszköz a GeoGebra 4.4-ben (Nyomvonal)

Kovács Zoltán




Outline

1

Háttér

2


3

Alkalmazások

Kovács Zoltán




Algebrai átírás (feltételek)

Kovács Zoltán




Alg. átírás (felt. és negált konklúzió, Rabinowitsch-trükk)

((v13 − v15 ) · v17 − 1) · ((v14 − v16 ) · v17 − 1) = 0

Kovács Zoltán





((v13 − v15 ) · v17 − 1) · ((v14 − v16 ) · v17 − 1) = 0

Kovács Zoltán









(v13 − v15 ) ·v17 − 1 · ((v14 − v16 ) · v17 − 1) = 0 |{z} | {z } ∨ v =v {z } | v 6=v 13

15

13

15

Kovács Zoltán




Komputeralgebra: A függ® változók eliminációja (ellenpélda)

((v13 − v15 ) · v17 − 1) · ((v14 − v16 ) · v17 − 1) = 0 ||| v5 v4 − v6 v3 − v5 v2 + v3 v2 + v6 v1 − v4 v1 = 0

Kovács Zoltán


Háttér

GeoGebra 4.4

A Kapcsolat Eszköz: El®készületek

Algebrai átírás: Példa

Alkalmazások

Algoritmusok

Geometriai interpretáció

v5 v4 − v6 v3 − v5 v2 + v3 v2 + v6 v1 − v4 v1

=0

m

v1 v3

v2 v4

1 1

v5

v6

1

=0

m Az A(v1 , v2 ), B (v3 , v4 ), C (v5 , v6 ) háromszög elfajuló (a területe 0).

Kovács Zoltán




Outline

1

Háttér

2


3

Alkalmazások

Kovács Zoltán




A BizonyításRészletek algoritmus (Recio-Vélez, 1996, b®v.) 1

v , . . . változókkal, A(0, 0) x ponttal. A független változók egy rögzített sorrendje szerint E -b®l elimináljuk a függ® A

K = ( F1 , . . . ; K )

input kérdés átírása

E

egyenletrendszerré

1

reductio ad absurdum, Rabinowitsch-trükkel és

2

változókat valamely CAS (Giac/Singular) meghívásával. 3

Az

E 0 ekvivalens egyenletrendszer átírása polinomiális tényez®k szorzataként. (A

magasabb fokú tényez®k fokszámának 1-re lapítása.)

4 5 6

E 0 = {1 = 0}, akkor az output: mindig igaz. E 0 = {0 = 0}, akkor az output: hamis. 0 Különben az E minden p = 0 polinomegyenletére, legyen Pp := 0 a kezdeti pontszám, p minden t tényez®jére, ha t -nek adható geom. interpr., akkor annak egyszer¶ségi et 0 pontszámát adjuk Pp -hez, kül. töröljük a p = 0 egyenletet E -b®l. 0 Ha E = {xP − xQ = 0, yP − yQ = 0} valamely szabad P és Q pontokra, akkor az output: igaz ha P 6= Q . 0 Ha van, válasszuk azt a p = 0 egyenletet E -b®l, amelyhez a legkisebb Pp < ∞ Ha Ha

1 2

7

8

pontszám tartozik, az output: a tényez®k negált geom. interpr. konjunkciója. 9

Különben az output: igaz bizonyos feltételek mellett. Kovács Zoltán




Teszteredmények (BizonyításRészletek) Teszt neve | GB (Singular) | GB (Giac) | Wu (OpenGeoProver) | Auto

Kovács Zoltán




A Bizonyít algoritmus (CoxLittleO'Shea)

1

2

K = (F1 , . . . ; K ) input kérdés átírása E egyenletrendszerré v1 , . . . változókkal, reductio ad absurdum, Rabinowitsch-trükkel, A(0, 0) és B (0, 1) x pontokkal. A

A független v1 , . . . , vt változók átnevezése algebrailag független (transzcendens)

3

V1 , . . . , Vt

változókra.

Döntsük el Singularral, hogy E (a vt +1 , . . . , vn változókban) ellentmondásos-e

4

Singularral

Q(V1 , . . . , Vt )-beli

együtthatókkal.

Ha igen, az output: igaz, ha nem: hamis.

Kovács Zoltán



A Bizonyít algoritmus a 1

A

K = (F1 , . . . ; K )


Giac rendszerrel

input kérdés átírása E egyenletrendszerré

v1 , . . . változókkal, reductio ad absurdum, Rabinowitsch-trükkel, A(0, 0) és B (0, 1) x pontokkal. 2

Legyen N a szabad pontok száma. Ha N

≥ 3,

minden egyes

X , Y , Z szabad ponthármasra b®vítsük E -t az X , Y , Z háromszög nem elfajuló feltétel egyenletével. 3

Döntsük el a Giac rendszerrel, hogy E ellentmondó-e.

4

Ha igen, az output: igaz.

Tétel

K = (F1 , . . . ; K ) egy kérdés. Legyen KF = (F1 , . . . , F ; T ) egy újabb K az F (nem elfajulást rögzít®) feltétellel b®vül. Ekkor K általában igaz akkor és csak akkor, ha KF is általában igaz.

Legyen

kérdés, melyben

Kovács Zoltán


Háttér

GeoGebra 4.4

A Kapcsolat Eszköz: El®készületek

Algebrai átírás: Példa

Alkalmazások

Algoritmusok

A Kapcsolat Eszköz algoritmus Input: kérdés

B := Bizonyít[kérdés]

hamis

nem általában igaz

B?

BR := BizonyításRészletek[kérdés]

igaz bizonyos feltételek mellett

Belső hiba BR ?

igaz {hamis}

B?

{igaz}

mindig igaz

nem definiált

általában igaz

B? igaz

lehet, hogy általában is igaz

nem

Csak olyan elfajuló feltételek szerepelnek, amelyeknek van egyszerű geometriai jelentésük?

igen igaz bizonyos feltételek egyszerre teljesülésekor: ezek listája

Kovács Zoltán



A Kapcsolat Eszköz alkalmazása

7 elemi geometriai tétel vizsgálata a Kapcsolat Eszközzel (GeoGebraBook) A kilencpontos kör: példa összetettebb elfajuló feltételekre

Kovács Zoltán



Oktatási alkalmazás? . . .Az

iskolákban a dinamikus geometriai rendszerek a

korábbinál jóval könnyebben hozzáférhet®ek. Ez arra hívja fel a gyelmet, hogy a sejtés és a bizonyítás közötti határvonal a diákok számára egyre kevésbé nyilvánvaló. . . Ezekkel a rendszerekkel könnyen és gyorsan ellen®rizhet® nagyon nagy számú esetre, hogy az állítás valóban fennáll, ezért a diákok sokkal könnyebben látják a matematikai tulajdonságokat, s így nincs igényük többé arra, hogy bármit is ténylegesen bebizonyítsanak. (Lin, Yang, Lee, Tabach and G. Stylianides, Principles of Task Design for Conjecturing and Proving, Springer, 2012, 305326.)

Kovács Zoltán


Eliminációs támogatás a GeoGebra Kapcsolat eszközéhez

Recommend Documents