prikaz prve stranice dokumenta Primjene Coq alata za dokazivanje u matematici i računarstvu
Rad nije dostupan
diplomski rad
Primjene Coq alata za dokazivanje u matematici i računarstvu
2024. urn:nbn:hr:168:192892
Hren, Miho
Sveučilište u Zagrebu
Fakultet elektrotehnike i računarstva

Citirajte ovaj rad

Hren, M. (2024). Primjene Coq alata za dokazivanje u matematici i računarstvu (Diplomski rad). Zagreb: Sveučilište u Zagrebu, Fakultet elektrotehnike i računarstva. Preuzeto s https://urn.nsk.hr/urn:nbn:hr:168:192892

Hren, Miho. "Primjene Coq alata za dokazivanje u matematici i računarstvu." Diplomski rad, Sveučilište u Zagrebu, Fakultet elektrotehnike i računarstva, 2024. https://urn.nsk.hr/urn:nbn:hr:168:192892

Hren, Miho. "Primjene Coq alata za dokazivanje u matematici i računarstvu." Diplomski rad, Sveučilište u Zagrebu, Fakultet elektrotehnike i računarstva, 2024. https://urn.nsk.hr/urn:nbn:hr:168:192892

Hren, M. (2024). 'Primjene Coq alata za dokazivanje u matematici i računarstvu', Diplomski rad, Sveučilište u Zagrebu, Fakultet elektrotehnike i računarstva, citirano: 19.10.2024., https://urn.nsk.hr/urn:nbn:hr:168:192892

Hren M. Primjene Coq alata za dokazivanje u matematici i računarstvu [Diplomski rad]. Zagreb: Sveučilište u Zagrebu, Fakultet elektrotehnike i računarstva; 2024 [pristupljeno 19.10.2024.] Dostupno na: https://urn.nsk.hr/urn:nbn:hr:168:192892

M. Hren, "Primjene Coq alata za dokazivanje u matematici i računarstvu", Diplomski rad, Sveučilište u Zagrebu, Fakultet elektrotehnike i računarstva, Zagreb, 2024. Dostupno na: https://urn.nsk.hr/urn:nbn:hr:168:192892

Za citiranje koristite ovu mrežnu adresu: https://urn.nsk.hr/urn:nbn:hr:168:192892
Prijavite se u repozitorij kako biste mogli spremiti objekt u svoju listu.
Podaci o radu
NaslovPrimjene Coq alata za dokazivanje u matematici i računarstvu
Naslov (engleski)Applications of the Coq Proof Assistant in mathematics and computer science
AutorMiho Hren
MentorAnte Đerek (mentor)
Član povjerenstvaAnte Đerek (predsjednik povjerenstva)
Član povjerenstvaStjepan Groš (član povjerenstva)
Član povjerenstvaAlan Jović (član povjerenstva)
Ustanova koja je dodijelila
akademski / stručni stupanj		Sveučilište u Zagrebu
Fakultet elektrotehnike i računarstva
Zagreb
Datum i država obrane2024-07-03, Hrvatska
Sažetak
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.
Sažetak (engleski)
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.
Ključne riječi
Ključne riječi (engleski)
Jezikhrvatski
URN:NBNurn:nbn:hr:168:192892
Studijski programNaziv: Računarstvo
Vrsta studija: sveučilišni
Stupanj studija: diplomski
Akademski / stručni naziv: magistar/magistra inženjer/inženjerka računarstva (mag.ing.comp.)
Vrsta resursaTekst
Način izrade datotekeIzvorno digitalna
Prava pristupaZatvoreni pristup
Uvjeti korištenjaIkona licence Zaštićeno autorskim pravom.
Javna napomena
Datum i vrijeme pohrane2024-10-12 20:49:23