Automatski dokazivači teorema

master's thesis

• Title (english): Automatic proof assistant of theorems
• Author: Alen Živković
• Mentor: Mladen Vuković (mentor)
• Committee member: Mladen Vuković (predsjednik povjerenstva)
• Committee member: Vedran Čačić (član povjerenstva)
• Committee member: Goranka Nogo (član povjerenstva)
• Committee member: Mea Bombardelli (član povjerenstva)
• Granter: University of Zagreb; Faculty of Science; (Department of Mathematics); Zagreb
• Defense date and country: 2021-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: automatski dokazivač teorema HERBY; Herbranda baza; Herbarandov univerzum; Herbrandov teorem; zatvoreno semantičko stablo
• Keywords (english): proof assistant HERBY; Herbrand base; Herbrand universe; Herbrand theorem; closed semantic trees
• Language: croatian
• URN:NBN: urn:nbn:hr:217:410453
• Study programme: Title: 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 resource: Text
• File origin: Born digital
• Access conditions: Open access
• Created on: 2021-11-09 12:50:19