АУТОМАТСКО ПРОВЕРАВАЊЕ НЕФОРМАЛНИХ ДОКАЗА ТЕОРЕМА СРЕДЊОШКОЛСКЕ ГЕОМЕТРИЈЕ

Сажетак

Доказивање теорема уз помоћ рачунара је област којој се поклања све више пажње у последњих неколико десетина година. Програми за доказивање теорема се из дана у дан све више развијају, постају флексибилнији и доказују све теже теореме. Њихов развој је често вођен идејом што једноставнијег коришћења и са циљем приближавања новим корисницима. Упркос томе, употреба програма за доказивање теорема није толико распрострањена међу широм популацијом као што су ученици средњих школа и студенти. Програм приказан у овом раду има за циљ приближавање области доказивања теорема уз помоћ рачунара управо њима. Програм омогућава аутоматско проверавање неформалних доказа теорема средњошколске геометрије и генерише формални доказ теореме проверив уз помоћ рачунара као и доказ записан на српском језику. Биће приказана његова употреба на доказима десетак теорема из уџбеника за средњу школу. Веома је једноставан за коришћење тако да га могу употребљавати чак и корисници који немају никакво искуство са доказивањем теорема уз помоћ рачунара. Поред примена у образовању, програм може бити користан и математичарима приликом генерисања нових доказа.