Računalna formalizacija matematičkih dokaza

master's thesis

• Title (english): Computer formalization of mathematical proofs
• Author: Ivona Čižić
• Mentor: Vedran Čačić (mentor)
• Committee member: Vedran Čačić (predsjednik povjerenstva)
• Committee member: Goranka Nogo (član povjerenstva)
• Committee member: Marko Horvat (član povjerenstva)
• Committee member: Zvonko Iljazović (član povjerenstva)
• Granter: University of Zagreb; Faculty of Science; (Department of Mathematics); Zagreb
• Defense date and country: 2023-09-22, Croatia
• Scientific / art field, discipline and subdiscipline: NATURAL SCIENCES; Mathematics

Abstract

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.

Abstract (english)

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.

• Keywords: Coq; funkcijski programski jezik; račun induktivnih konstrukcija
• Keywords (english): Coq; functional programming language; Calculus of Inductive Constructions (CIC)
• Language: croatian
• URN:NBN: urn:nbn:hr:217:012282
• Study programme: Title: Computer Science and Mathematics; Study programme type: university; Study level: graduate; Academic / professional title: sveučilišni magistar računarstva i matematike (sveučilišni magistar računarstva i matematike)
• Type of resource: Text
• File origin: Born digital
• Access conditions: Open access
• Created on: 2024-01-30 13:19:30