prikaz prve stranice dokumenta Računalna formalizacija matematičkih dokaza
  Download
PDF 280.38 KB
master's thesis
Računalna formalizacija matematičkih dokaza
Zagreb: University of Zagreb, Faculty of Science, 2023. urn:nbn:hr:217:012282
Čižić, Ivona
University of Zagreb
Faculty of Science
Department of Mathematics

Institutional repository: Repository of the Faculty of Science

Cite this document

Čižić, I. (2023). Računalna formalizacija matematičkih dokaza (Master's thesis). Zagreb: University of Zagreb, Faculty of Science. Retrieved from https://urn.nsk.hr/urn:nbn:hr:217:012282

Čižić, Ivona. "Računalna formalizacija matematičkih dokaza." Master's thesis, University of Zagreb, Faculty of Science, 2023. https://urn.nsk.hr/urn:nbn:hr:217:012282

Čižić, Ivona. "Računalna formalizacija matematičkih dokaza." Master's thesis, University of Zagreb, Faculty of Science, 2023. https://urn.nsk.hr/urn:nbn:hr:217:012282

Čižić, I. (2023). 'Računalna formalizacija matematičkih dokaza', Master's thesis, University of Zagreb, Faculty of Science, accessed 23 December 2024, https://urn.nsk.hr/urn:nbn:hr:217:012282

Čižić I. Računalna formalizacija matematičkih dokaza [Master's thesis]. Zagreb: University of Zagreb, Faculty of Science; 2023 [cited 2024 December 23] Available at: https://urn.nsk.hr/urn:nbn:hr:217:012282

I. Čižić, "Računalna formalizacija matematičkih dokaza", Master's thesis, University of Zagreb, Faculty of Science, Zagreb, 2023. Available at: https://urn.nsk.hr/urn:nbn:hr:217:012282

Metadata
TitleRačunalna formalizacija matematičkih dokaza
Title (english)Computer formalization of mathematical proofs
AuthorIvona Čižić
MentorVedran Čačić (mentor)
Committee memberVedran Čačić (predsjednik povjerenstva)
Committee memberGoranka Nogo (član povjerenstva)
Committee memberMarko Horvat (član povjerenstva)
Committee memberZvonko Iljazović (član povjerenstva)
GranterUniversity of Zagreb
Faculty of Science
(Department of Mathematics)
Zagreb
Defense date and country2023-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
Keywords (english)
Languagecroatian
URN:NBNurn:nbn:hr:217:012282
Study programmeTitle: 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 resourceText
File originBorn digital
Access conditionsOpen access
Terms of useLicence In copyright icon
Created on2024-01-30 13:19:30