Izdelava in uporaba dokazovalnega pomočnika

Zupančič, Blaž (author), 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.

• Language: Slovenian
• Keywords: dokazovalni pomočnik, teorija tipov
• Work type: Bachelor thesis/paper
• Typology: 2.11 - Undergraduate Thesis
• Organization: FRI - Faculty of Computer and Information Science ; FMF - Faculty of Mathematics and Physics
• Year: 2023
• PID: 20.500.12556/RUL-145593
• COBISS.SI-ID: 150155779
• Publication date in RUL: 24.04.2023

Secondary language

• Language: English
• Title: Implementation and use of a proof assistant

Abstract

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.

• Keywords: proof assistant, type theory