Unapređivanje razumevanja dokaza teorema pomoću interaktivnih dokazivača

Abstract

Osnovni koncepti matematike i njihova svojstva se standardno opisuju teoremama. Razumevanje dokaza teorema, kao i kreiranje dokaza teorema je često neophodno za uspešno usvajanje znanja i praćenje gradiva. U poslednjih par decenija se sve češće koriste interaktivni dokazivači teorema, programi namenjeni detaljnom zapisivanju i dokazivanju teorema koji garantuju, odnosno proveravaju, korektnost napisanih dokaza. Preciznost koja je neophodna za rad sa interaktivnim dokazivačima i povratne informacije koje se dobijaju, mogu imati veliki benefit za razumevanje matematičkih koncepata i primene osnovnih logičkih pravila. Pažljiv odabir matematičkih i informatičkih oblasti može biti korišćen da studenti savladaju osnove formalnog dokazivanja teorema, bez prethodnog predznanja iz kurseva matematičke logike. Ovaj pristup je korišćen u okviru kursa "Uvod u interaktivno dokazivanje teorema", na četvrtoj godini Matematičkog fakulteta uz interaktivni dokazivač teorema Isabelle. Pozitivni rezultati kursa su vidljivi kroz veliki skup seminarskih radova, među kojima su formalizovani zadaci sa rešenjima sa matematičkih olimpijada, kao i verifikovani odred-eni algoritmi i strukture podataka.