Automatsko proveravanje neformalnih dokaza teorema srednjoškolske geometrije

Abstract

Dokazivanje teorema uz pomoć računara je oblast kojoj se poklanja sve više pažnje u poslednjih nekoliko desetina godina. Programi za dokazivanje teorema se iz dana u dan sve više razvijaju, postaju fleksibilniji i dokazuju sve teže teoreme. Njihov razvoj je često vođen idejom što jednostavnijeg korišćenja i sa ciljem približavanja novim korisnicima. Uprkos tome, upotreba programa za dokazivanje teorema nije toliko rasprostranjena među širom populacijom kao što su učenici srednjih škola i studenti. Program prikazan u ovom radu ima za cilj približavanje oblasti dokazivanja teorema uz pomoć računara upravo njima. Program omogućava automatsko proveravanje neformalnih dokaza teorema srednjoškolske geometrije i generiše formalni dokaz teoreme proveriv uz pomoć računara kao i dokaz zapisan na srpskom jeziku. Biće prikazana njegova upotreba na dokazima desetak teorema iz udžbenika za srednju školu. Veoma je jednostavan za korišćenje tako da ga mogu upotrebljavati čak i korisnici koji nemaju nikakvo iskustvo sa dokazivanjem teorema uz pomoć računara. Pored primena u obrazovanju, program može biti koristan i matematičarima prilikom generisanja novih dokaza.