Automatski dokazivači teorema

diplomski rad

• Naslov (engleski): Automatic proof assistant of theorems
• Autor: Alen Živković
• Mentor: Mladen Vuković (mentor)
• Član povjerenstva: Mladen Vuković (predsjednik povjerenstva)
• Član povjerenstva: Vedran Čačić (član povjerenstva)
• Član povjerenstva: Goranka Nogo (član povjerenstva)
• Član povjerenstva: Mea 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 obrane: 2021-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: automatski dokazivač teorema HERBY; Herbranda baza; Herbarandov univerzum; Herbrandov teorem; zatvoreno semantičko stablo
• Ključne riječi (engleski): proof assistant HERBY; Herbrand base; Herbrand universe; Herbrand theorem; closed semantic trees
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:217:410453
• Studijski program: Naziv: 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 resursa: Tekst
• Način izrade datoteke: Izvorno digitalna
• Prava pristupa: Otvoreni pristup
• Datum i vrijeme pohrane: 2021-11-09 12:50:19