Izdelava in uporaba dokazovalnega pomočnika

Zupančič, Blaž (avtor), Bauer, Andrej (mentor)

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.

• Jezik: Slovenski jezik
• Ključne besede: dokazovalni pomočnik, teorija tipov
• Vrsta gradiva: Diplomsko delo/naloga
• Tipologija: 2.11 - Diplomsko delo
• Organizacija: FRI - Fakulteta za računalništvo in informatiko; FMF - Fakulteta za matematiko in fiziko
• Leto izida: 2023
• PID: 20.500.12556/RUL-145593
• COBISS.SI-ID: 150155779
• Datum objave v RUL: 24.04.2023

Sekundarni jezik

• Jezik: Angleški jezik
• Naslov: Implementation and use of a proof assistant

Izvleček

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.

• Ključne besede: proof assistant, type theory