20.500.12556/RUL-145593 Izdelava in uporaba dokazovalnega pomočnika Implementation and use of a proof assistant Dokazovalni 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. A proof assistant is a software tool for development of formal proofs. This thesis demonstrates implementation and use of one such tool. As the basis of our proof assistant we used an implementation of a minimalist type theory developed by prof. dr. Andrej Bauer using the OCaml programming language. We expanded his implementation with the type of natural numbers and identity types which allowed us to express and prove the basic properties of addition. dokazovalni pomočnik teorija tipov proof assistant type theory true false false Slovenski jezik Angleški jezik Diplomsko delo/naloga 2023-04-24 09:30:00 2023-04-24 09:30:03 2023-11-24 12:13:09 0000-00-00 00:00:00 2023 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 34994 150155779 Zupancic_Blaz_-_Implementacija_in_uporaba_dokazovalnega_pomocnika.pdf Zupancic_Blaz_-_Implementacija_in_uporaba_dokazovalnega_pomocnika.pdf 1 12E7523EBF60533326BCC33CCA2EFE04 63545d2c5d63849e535f935782087d20049938cc80dd04dc4e081137b707f55b a46201e6-e271-11ed-a314-00155dcfd717 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=168514 Fakulteta za računalništvo in informatiko Fakulteta za matematiko in fiziko 0 0 0