prikaz prve stranice dokumenta Automatski dokazivači teorema
  Download
PDF 416.72 KB
master's thesis
Automatski dokazivači teorema
Zagreb: University of Zagreb, Faculty of Science, 2021. urn:nbn:hr:217:410453
Živković, Alen
University of Zagreb
Faculty of Science
Department of Mathematics

Institutional repository: Repository of the Faculty of Science

Cite this document

Živković, A. (2021). Automatski dokazivači teorema (Master's thesis). Zagreb: University of Zagreb, Faculty of Science. Retrieved from https://urn.nsk.hr/urn:nbn:hr:217:410453

Živković, Alen. "Automatski dokazivači teorema." Master's thesis, University of Zagreb, Faculty of Science, 2021. https://urn.nsk.hr/urn:nbn:hr:217:410453

Živković, Alen. "Automatski dokazivači teorema." Master's thesis, University of Zagreb, Faculty of Science, 2021. https://urn.nsk.hr/urn:nbn:hr:217:410453

Živković, A. (2021). 'Automatski dokazivači teorema', Master's thesis, University of Zagreb, Faculty of Science, accessed 02 July 2024, https://urn.nsk.hr/urn:nbn:hr:217:410453

Živković A. Automatski dokazivači teorema [Master's thesis]. Zagreb: University of Zagreb, Faculty of Science; 2021 [cited 2024 July 02] Available at: https://urn.nsk.hr/urn:nbn:hr:217:410453

A. Živković, "Automatski dokazivači teorema", Master's thesis, University of Zagreb, Faculty of Science, Zagreb, 2021. Available at: https://urn.nsk.hr/urn:nbn:hr:217:410453

Metadata
TitleAutomatski dokazivači teorema
Title (english)Automatic proof assistant of theorems
AuthorAlen Živković
MentorMladen Vuković (mentor)
Committee memberMladen Vuković (predsjednik povjerenstva)
Committee memberVedran Čačić (član povjerenstva)
Committee memberGoranka Nogo (član povjerenstva)
Committee memberMea Bombardelli (član povjerenstva)
GranterUniversity of Zagreb
Faculty of Science
(Department of Mathematics)
Zagreb
Defense date and country2021-09-22, Croatia
Scientific / art field,
discipline and subdiscipline		NATURAL SCIENCES
Mathematics
Abstract
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.
Abstract (english)
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.
Keywords
Keywords (english)
Languagecroatian
URN:NBNurn:nbn:hr:217:410453
Study programmeTitle: Computer Science and Mathematics
Study programme type: university
Study level: graduate
Academic / professional title: magistar/magistra računarstva i matematike (magistar/magistra računarstva i matematike)
Type of resourceText
File originBorn digital
Access conditionsOpen access
Terms of useLicence In copyright icon
Created on2021-11-09 12:50:19