Prirodna dedukcija, preko interaktivnog dokazivanja do LaTeX dokaza

Abstract

Proces pisanja dokaza u prirodnoj dedukciji je uglavnom pravolinijski, sa izuzecima primene pravila koja dovode do grananja u dokazima. Na papiru se gradi stablo dokaza, a za potrebe pisanja matematičkih udžbenika potrebno je pažljivo prepisati dati dokaz u LATEX format. Kako se dužina dokaza može uvećavati poprilično brzo, kako matematičar napreduje i savladava dokaze težih teorema, javlja se rizik od pravljenja grešaka prilikom kucanja poprilično komplikovanog LATEX koda koji se koristi za generisanje stabla dokaza. Sa idejom olakšavanja ovog procesa i povećanja sigurnosti u generisanje LaTeX dokaza u prirodnoj dedukciji, kreiran je dokazivač Theodor koji će biti prikazan u ovom radu. Interaktivni dokazivač teorema Theodore, koristi isključivo pravila prirodne dedukcije, i može dokazivati teoreme logike prvog reda. Napisan je u jeziku Haskell i izvršava se u interaktivnom okruženju GHCi. U toku rada dokazivača, tekući cilj dokaza se transformiše dok ne dodđemo do praznog cilja. Na kraju rada dokazivača automatski se kreira LATEX drvo dokaza u prirodnoj dedukciji na osnovu interaktivno kreiranog dokaza u stilu uobičajenom za matematičke udžbenike