Izdelava in uporaba dokazovalnega pomočnika

diplomsko delo

Blaž Zupančič (Author), Andrej Bauer (Mentor)

Abstract

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.

Keywords

dokazovalni pomočnik;teorija tipov;interdisciplinarni študij;univerzitetni študij;diplomske naloge;

Data

Language:	Slovenian
Year of publishing:	2023
Typology:	2.11 - Undergraduate Thesis
Organization:	UL FMF - Faculty of Mathematics and Physics
Publisher:	[B. Zupančič]
UDC:	004:51(043.2)
COBISS:	150155779
Views:	203
Downloads:	52
Average score:	0 (0 votes)
Metadata:

Other data

Secondary language:	English
Secondary title:	Implementation and use of a proof assistant
Secondary 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.
Secondary keywords:	proof assistant;type theory;computer science;computer and information science;computer science and mathematics;interdisciplinary studies;diploma;Matematika;Računalništvo;Univerzitetna in visokošolska dela;
Type (COBISS):	Bachelor thesis/paper
Study programme:	1000407
Thesis comment:	Univ. v Ljubljani, Fak. za računalništvo in informatiko
Pages:	37 str.
ID:	18700864