Primjene Coq alata za dokazivanje u matematici i računarstvu

Hren, Miho

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

APA 6th Edition

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

MLA 8th Edition

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

Chicago 17th Edition

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

Harvard

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: 10.11.2024., https://urn.nsk.hr/urn:nbn:hr:168:192892

Vancouver

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 10.11.2024.] Dostupno na: https://urn.nsk.hr/urn:nbn:hr:168:192892

IEEE

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

Naslov	Primjene Coq alata za dokazivanje u matematici i računarstvu
Naslov (engleski)	Applications of the Coq Proof Assistant in mathematics and computer science
Autor	Miho Hren
Mentor	Ante Đerek (mentor)
Član povjerenstva	Ante Đerek (predsjednik povjerenstva)
Član povjerenstva	Stjepan Groš (član povjerenstva)
Član povjerenstva	Alan 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 obrane	2024-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)
Jezik	hrvatski
URN:NBN	urn:nbn:hr:168:192892
Studijski program	Naziv: 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 resursa	Tekst
Način izrade datoteke	Izvorno digitalna
Prava pristupa	Zatvoreni pristup
Uvjeti korištenja
Javna napomena
Datum i vrijeme pohrane	2024-10-12 20:49:23