prikaz prve stranice dokumenta Primjene Coq alata za dokazivanje u matematici i računarstvu
No public access
master's thesis
Primjene Coq alata za dokazivanje u matematici i računarstvu
Zagreb: University of Zagreb, Faculty of Electrical Engineering and Computing, 2024. urn:nbn:hr:168:192892
Hren, Miho
University of Zagreb
Faculty of Electrical Engineering and Computing

Institutional repository: FER Repository

Cite this document

Hren, M. (2024). Primjene Coq alata za dokazivanje u matematici i računarstvu (Master's thesis). Zagreb: University of Zagreb, Faculty of Electrical Engineering and Computing. Retrieved from https://urn.nsk.hr/urn:nbn:hr:168:192892

Hren, Miho. "Primjene Coq alata za dokazivanje u matematici i računarstvu." Master's thesis, University of Zagreb, Faculty of Electrical Engineering and Computing, 2024. https://urn.nsk.hr/urn:nbn:hr:168:192892

Hren, Miho. "Primjene Coq alata za dokazivanje u matematici i računarstvu." Master's thesis, University of Zagreb, Faculty of Electrical Engineering and Computing, 2024. https://urn.nsk.hr/urn:nbn:hr:168:192892

Hren, M. (2024). 'Primjene Coq alata za dokazivanje u matematici i računarstvu', Master's thesis, University of Zagreb, Faculty of Electrical Engineering and Computing, accessed 23 November 2024, https://urn.nsk.hr/urn:nbn:hr:168:192892

Hren M. Primjene Coq alata za dokazivanje u matematici i računarstvu [Master's thesis]. Zagreb: University of Zagreb, Faculty of Electrical Engineering and Computing; 2024 [cited 2024 November 23] Available at: https://urn.nsk.hr/urn:nbn:hr:168:192892

M. Hren, "Primjene Coq alata za dokazivanje u matematici i računarstvu", Master's thesis, University of Zagreb, Faculty of Electrical Engineering and Computing, Zagreb, 2024. Available at: https://urn.nsk.hr/urn:nbn:hr:168:192892

Metadata
TitlePrimjene Coq alata za dokazivanje u matematici i računarstvu
Title (english)Applications of the Coq Proof Assistant in mathematics and computer science
AuthorMiho Hren
MentorAnte Đerek (mentor)
Committee memberAnte Đerek (predsjednik povjerenstva)
Committee memberStjepan Groš (član povjerenstva)
Committee memberAlan Jović (član povjerenstva)
GranterUniversity of Zagreb
Faculty of Electrical Engineering and Computing
Zagreb
Defense date and country2024-07-03, Croatia
Abstract
Coq je interaktivni dokazivač teorema temeljen na teoriji tipova. U ovom radu primijenili smo alat Coq na zadatak formalizacije logike prvog reda s induktivnim definicijama FOL_ID. Nadalje, definirali smo standardne modele i dokazni sustav LKID za logiku FOL_ID te dokazali neka njihova svojstva. Također smo neformalno prikazali cikličke dokaze u kontekstu logike FOL_ID. Sve definicije i leme u radu ilustrirali smo primjerima te formalizacijom u Coqu.
Abstract (english)
Coq is an interactive theorem prover based on type theory. In this thesis we applied the Coq Proof Assistant to the task of formalizing first order logic with inductive definitions FOL_ID. Furthermore, we defined standard models and the LKID proof system for FOL_ID, and we proved some of their properties. We also informally presented cyclic proofs in the context of FOL_ID. We illustrated all the definitions and lemmas in this thesis with examples and formalizations in Coq.
Keywords
Keywords (english)
Languagecroatian
URN:NBNurn:nbn:hr:168:192892
Study programmeTitle: Computing
Study programme type: university
Study level: graduate
Academic / professional title: magistar/magistra inženjer/inženjerka računarstva (magistar/magistra inženjer/inženjerka računarstva)
Type of resourceText
File originBorn digital
Access conditionsClosed access
Terms of useLicence In copyright icon
Public note
Created on2024-10-12 20:49:23