Izdelava in uporaba dokazovalnega pomočnika

diplomsko delo

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

Povzetek

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.

Ključne besede

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

Podatki

Jezik:	Slovenski jezik
Leto izida:	2023
Tipologija:	2.11 - Diplomsko delo
Organizacija:	UL FMF - Fakulteta za matematiko in fiziko
Založnik:	[B. Zupančič]
UDK:	004:51(043.2)
COBISS:	150155779
Št. ogledov:	203
Št. prenosov:	52
Ocena:	0 (0 glasov)
Metapodatki:

Ostali podatki

Sekundarni jezik:	Angleški jezik
Sekundarni naslov:	Implementation and use of a proof assistant
Sekundarni povzetek:	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.
Sekundarne ključne besede:	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;
Vrsta dela (COBISS):	Diplomsko delo/naloga
Študijski program:	1000407
Komentar na gradivo:	Univ. v Ljubljani, Fak. za računalništvo in informatiko
Strani:	37 str.
ID:	18700864