Računalna formalizacija matematičkih dokaza

diplomski rad

• Naslov (engleski): Computer formalization of mathematical proofs
• Autor: Ivona Čižić
• Mentor: Vedran Čačić (mentor)
• Član povjerenstva: Vedran Čačić (predsjednik povjerenstva)
• Član povjerenstva: Goranka Nogo (član povjerenstva)
• Član povjerenstva: Marko Horvat (član povjerenstva)
• Član povjerenstva: Zvonko Iljazović (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Prirodoslovno-matematički fakultet; (Matematički odsjek); Zagreb
• Datum i država obrane: 2023-09-22, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: PRIRODNE ZNANOSTI; Matematika

Sažetak

U prvom poglavlju upoznajemo Coq kao funkcijski programski jezik. Poglavlje završavamo primjerom rješavanja problema nalaženja najduljeg zajedničkog podniza neka dva niza u Coqu. Drugo poglavlje posvećujemo Računu induktivnih konstrukcija (CIC). Opisujemo formalizam koji stoji u pozadini Coqa. U trećem poglavlju navodimo osnovne smjernice pri konstruiranju dokaza, s fokusom na logičke veznike i kvantifikatore. Kroz primjere asocijativnosti disjunkcije i nekih koraka u dokazu iracionalnosti broja \(\sqrt{2}\), upoznajemo se s najčešće korištenim taktikama.

Sažetak (engleski)

In first chapter we are introduced to Coq as a functional programming language. The chapter ends with an example where we show how to solve the problem of finding the longest common subsequence of two given sequences using Coq. We devoted the second chapter to The Calculus of Inductive Constructions (CIC). Here we are describing the formalism upon which Coq is based on. In the third chapter, we are providing the basic guidlines to constructing proofs with focus on the logical connectives and quantifiers. We are getting to know the most often used tactics through the examples of associativity of disjunction and some of the steps in the proof that \(\sqrt{2}\) is irrational number.

• Ključne riječi: Coq; funkcijski programski jezik; račun induktivnih konstrukcija
• Ključne riječi (engleski): Coq; functional programming language; Calculus of Inductive Constructions (CIC)
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:217:012282
• Studijski program: Naziv: Računarstvo i matematika; Vrsta studija: sveučilišni; Stupanj studija: diplomski; Akademski / stručni naziv: sveučilišni magistar računarstva i matematike (univ. mag. inf. et math.)
• Vrsta resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Otvoreni pristup
• Datum i vrijeme pohrane: 2024-01-30 13:19:30