prikaz prve stranice dokumenta Automatski dokazivači teorema
  Preuzmi
PDF 416.72 KB
diplomski rad
Automatski dokazivači teorema
Zagreb: Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, 2021. urn:nbn:hr:217:410453
Živković, Alen
Sveučilište u Zagrebu
Prirodoslovno-matematički fakultet
Matematički odsjek

Institucijski repozitorij: Repozitorij Prirodoslovno-matematičkog fakulteta

Citirajte ovaj rad

Živković, A. (2021). Automatski dokazivači teorema (Diplomski rad). Zagreb: Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet. Preuzeto s https://urn.nsk.hr/urn:nbn:hr:217:410453

Živković, Alen. "Automatski dokazivači teorema." Diplomski rad, Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, 2021. https://urn.nsk.hr/urn:nbn:hr:217:410453

Živković, Alen. "Automatski dokazivači teorema." Diplomski rad, Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, 2021. https://urn.nsk.hr/urn:nbn:hr:217:410453

Živković, A. (2021). 'Automatski dokazivači teorema', Diplomski rad, Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, citirano: 23.12.2024., https://urn.nsk.hr/urn:nbn:hr:217:410453

Živković A. Automatski dokazivači teorema [Diplomski rad]. Zagreb: Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet; 2021 [pristupljeno 23.12.2024.] Dostupno na: https://urn.nsk.hr/urn:nbn:hr:217:410453

A. Živković, "Automatski dokazivači teorema", Diplomski rad, Sveučilište u Zagrebu, Prirodoslovno-matematički fakultet, Zagreb, 2021. Dostupno na: https://urn.nsk.hr/urn:nbn:hr:217:410453

Za citiranje koristite ovu mrežnu adresu: https://urn.nsk.hr/urn:nbn:hr:217:410453
Podaci o radu
NaslovAutomatski dokazivači teorema
Naslov (engleski)Automatic proof assistant of theorems
AutorAlen Živković
MentorMladen Vuković (mentor)
Član povjerenstvaMladen Vuković (predsjednik povjerenstva)
Član povjerenstvaVedran Čačić (član povjerenstva)
Član povjerenstvaGoranka Nogo (član povjerenstva)
Član povjerenstvaMea Bombardelli (član povjerenstva)
Ustanova koja je dodijelila
akademski / stručni stupanj		Sveučilište u Zagrebu
Prirodoslovno-matematički fakultet
(Matematički odsjek)
Zagreb
Datum i država obrane2021-09-22, Hrvatska
Znanstveno / umjetničko
područje, polje i grana		PRIRODNE ZNANOSTI
Matematika
Sažetak
U ovom radu proučavamo automatski dokazivač teorema HERBY. Najprije se bavimo teorijskom pozadinom njegovog rada i uvodimo pojmove Herbrandove baze i Herbarandovog univerzuma da bi došli do ključnog rezultata, Herbrandovog teorema. Iz jedne verzije Herbrandovog teorema dobivamo način na koji program HERBY dokazuje teoreme, tj. konstrukcijom zatvorenog semantičkog stabla. Zatim proučavamo reprezentaciju logike prvog reda unutar programa HERBY te pretvaranje formula logike prvog reda u klauzule kako bismo mogli programu HERBY teorem zadati u željenom obliku. Opisujemo nekoliko heuristika koje čine konstrukciju zatvorenog semantičkog stabla efikasnijom. Napokon pokrećemo program HERBY te pomoću njega dokazujemo dva teorema. Za svaki teorem skiciramo zatvoreno semantičko stablo pomoću kojeg smo ga dokazali.
Sažetak (engleski)
In this paper we present the proof assistant HERBY. Firstly, we take a look into the theoretical basis of its work. We introduce the Herbrand base and the Herbrand universe to arrive at the key conjecture, Herbrand theorem. One version of the theorem serves as an insight into the method HERBY uses to prove theorems, which is by constructing closed semantic trees. We then present a representation of first order logic formulas within HERBY and we study the transformation of first order logic formulas into clauses as they are the form theorems need to take to be used as input. We observe some of the heuristics that are used for efficiency reasons in constructing a closed semantic tree. Finally, we run and test HERBY by proving two theorems. For each of the theorems we offer a sketch of the closed semantic tree used to prove it.
Ključne riječi
Ključne riječi (engleski)
Jezikhrvatski
URN:NBNurn:nbn:hr:217:410453
Studijski programNaziv: Računarstvo i matematika
Vrsta studija: sveučilišni
Stupanj studija: diplomski
Akademski / stručni naziv: magistar/magistra računarstva i matematike (mag. inf. et math.)
Vrsta resursaTekst
Način izrade datotekeIzvorno digitalna
Prava pristupaOtvoreni pristup
Uvjeti korištenjaIkona licence Zaštićeno autorskim pravom.
Datum i vrijeme pohrane2021-11-09 12:50:19