Izdelava in uporaba dokazovalnega pomočnikaZupančič, Blaž (Avtor) Bauer, Andrej (Mentor) dokazovalni pomočnikteorija tipovDokazovalni pomočnik je računalniški program za izdelavo formalnih matematičnih dokazov. To diplomsko delo obravnava izdelavo in uporabo preprostega tovrstnega programa. Za osnovo dokazovalnega pomočnika smo vzeli implementacijo minimalistične teorije tipov, ki jo je v programskem jeziku OCaml razvil prof. dr. Andrej Bauer. Njegovo implementacijo smo razširili s tipom naravnih števil in tipi identifikacij, da smo lahko v njej izrazili in dokazali osnovne lastnosti seštevanja.20232023-04-24 09:30:00Diplomsko delo/naloga145593VisID: 34994COBISS_ID: 150155779sl