Title Metoda tableauxa za modalnu logiku Author Tin Babić Mentor Tin Perkov (mentor)Mentor Mladen Vuković (mentor)Committee member Tin Perkov (predsjednik povjerenstva)Committee member Mladen Vuković (član povjerenstva)Committee member Vedran Čačić (član povjerenstva)Committee member Zvonko Iljazović (član povjerenstva)Granter University of Zagreb Defense date and country 2018-11-28, Croatia Scientific / art field, NATURAL SCIENCES Abstract Ovaj rad proučava jednu od metoda za dobivanje modela logičkih formula koju nazivamo metoda tableauxa ili glavni test. Zanimljiva nam je zbog algoritamskog pristupa kojim je možemo opisati i time vrlo lako prenijeti na računalo. Od posebnog značaja je opis te metode za vrstu logike znanu kao modalna logika. Rad je podijeljen na četiri poglavlja. Prvo poglavlje upoznaje nas sa sintaksom i semantikom osnovnog modalnog jezika. Ističemo sličnosti i razlike s logikom sudova, ponajprije u pojmu istinitosti formula. Ovdje veliku ulogu imaju modalni operatori koji su detaljno obrađeni. Kraj prvog poglavlja iznosi cilj rada: dobivanje efikasnog postupka (algoritma) za pronalazak modela u kojem je neka formula osnovnog modalnog jezika ispunjiva. Također, navodimo vezu ispunjivosti i valjanosti formula i zaključujemo kako je naš algoritam moguće primijeniti i na ispitivanje ispunjivosti i na ispitivanje valjanosti dane formule. Drugo poglavlje započinje klasifikacijom formula u nama zanimljive skupine. Ovakav pristup prvi je upotrijebio Smullyan u [8]. On spominje \(\alpha\) i \(\beta\) klase formula koje mi malo drugačije nazivamo, ali ideja je ista. Nastavlja se uvođenjem pravila metode tableauxa za logiku sudova i osnovnih pojmova potrebnih za njeno shvaćanje. Bitno je spomenuti kako su ova pravila sintaktičkog oblika, a semantičko značenje dajemo na kraju poglavlja dokazujući dva vrlo važna teorema: adekvatnost i potpunost. Adekvatnost metode tableauxa povezuje pojmove zatvorenog stabla i neispunjivosti formule za koju je to semantičko stablo izgrađeno, štoviše, ako za formulu imamo zatvoreno stablo, tada je ona sigurno neispunjiva. Potpunost ide obrnutim smjerom, za neispunjivu formulu iz ovog teorema slijedi da se sva semantička stabla zatvore. Dobiveni rezultat nam daje slobodu u primjeni sintaktičkog algoritma, recimo na računalu, a semantička interpretacija ne izostaje. Treće poglavlje proširuje naše klase još jednom, a to su nasljedne formule. Ova klasa sadrži sve formule dobivene primjenom modalnog operatora na neku formulu osnovnog modalnog jezika i njihove negacije. Uvodi se pojam proširenog zatvorenja i dokazuje njegova konačnost. U nastavku iznosimo prilagođenu metodu tableauxa korištenjem one iz drugog poglavlja i pokazujemo njezine nedostatke. Navodimo pravila nove metode tableauxa kojom se rješavamo tih nedostataka. Metoda iz drugog poglavlja važan je dio ove naše nove metode te razumijevanje drugog poglavlja uvelike pomaže u razumijevanju trećeg. Kao i u drugom poglavlju, ova pravila su sintaktičkog oblika i lako primjenjiva na računalu. Nastavak trećeg poglavlja sadrži dokaz adekvatnosti i potpunosti naše nove metode za osnovni modalni jezik. Od posebnog značaja su pojmovi Hintikkine strukture i označenog grafa. Dokazom tih dvaju teorema ponovno je dobivena veza sintakse i semantike, ali za kompliciraniji osnovni modalni jezik. Četvrto poglavlje proučava pitanje odlučivosti. Definiramo Turingov stroj. U nastavku se definira Turing-odlučivost i pokazuje kako su problemi koje rješavaju obje metode predstavljene u ovom radu odlučivi, za razliku od analognog problema u logici prvog reda. Posebno, želio bih se zahvaliti svojem mentoru, doc. dr. sc. Tinu Perkovu na iznimnom strpljenju i ne malom broju sugestija bez kojih ovaj rad ne bi bio moguć. Također, zahvaljujem se i suvoditelju, izv. prof. dr. sc. Mladenu Vukoviću na vrlo zanimljivim predavanjima kojima je i potaknuo moju želju za proširenjem znanja o logici bez kojih ne bi bilo ovog rada.
Abstract (english) In this thesis we examine one of the methods of acquiring a model for logical formulae known as tableaux. We are interested in it because of an algorithmic approach with which it can be described and easily transferred to a computer. Special attention is given to describing said method for a particular type of logic known as modal logic. The thesis consists of four chapters. In the first chapter we are introduced to the syntax and semantics of basic modal language. We highlight the similarities and differences with propositional logic, especially in the definition of truth. Great care is taken to explain modal operators as they play an essential part of the basic modal language. The end of first chapter states the goal of this thesis: providing an effective algorithm for finding a model in which a formula of the basic modal language is satisfiable. Moreover, we give a link between the concept of satisfiability and validity of formulae and conclude the effectiveness of our algorithm for finding both. Second chapter begins with a classification of formulae to relevant groups. This approach was first introduced by Smullyan in [8]. He uses \(\alpha\) and \(\beta\) classes of formulae that we denote slightly different, albeit the main concept stays the same. We continue by introducing the rules of the tableaux method for propositional logic and other basic concepts needed. We emphasize that these rules are strictly syntactic in nature. The semantic meaning follows at the end of the chapter from the proof of two very important theorems: soundness and completeness. Soundness of the tableaux method links the concept of closed tree and unsatisfiability of formulae of which said tree is built from, moreover, it follows that if a formula has a closed tree, then it is unsatisfiable. Completeness gives us the converse: for an unsatisfiable formula all trees must close. This result gives us the freedom to use the syntactic rules of the algorithm, for example on a computer, and the implied semantic meaning stays with it. Third chapter expands our classification by one more class, and that is successor formulae. This class consists of all formulae built by applying a modal operator on some formula of the basic modal language and their negations. We introduce the concept of expanded closure and we prove that it is finite. Continuing on, we state a modified tableaux method from chapter two and show its drawbacks. We state the rules of a new tableaux method that will strive to fix the drawbacks mentioned earlier. The tableaux method from chapter two is an integral part of our new method. As such, understanding of concepts in chapter two is imperative for the proper understanding in chapter three. As in chapter two, these rules are syntactic in nature and easily transferable to a computer. The continuation of chapter three consists of the proof of soundness and completeness of our new method for basic modal language. Important concepts to remember are Hintikka structures and labelled graphs. By concluding these proofs we have given a link between the syntactic rules and semantic meaning, but for a more complicated, basic modal language. Chapter four deals with the question of decidability. We state what a Turing machine and Turing-decidability are. We then proceed to show that both of the problems solved by the methods examined here are decidable in contrast to the same problem in first order logic which is not decidable. Finally, I would like to thank my mentor, assist. prof. Tin Perkov for his boundless patience and a variety of suggestions that have made this thesis possible. Furthermore, I would also like to thank my co-mentor, assoc. prof. Mladen Vuković, for very interesting lectures that made me want to expand my knowledge of logic, without which this thesis would not be possible.
Keywords
model logičkih formula
metoda tableauxa
algoritamski pristup
modalna logika
logika sudova
Hintikkina struktura
Turingov stroj
Turing odlučivost
Keywords (english)
model for logical formulae
tableaux method
algorithmic approach
modal logic
propositional logic
Hintikka structure
Turing machine
Turing decidability
Language croatian URN:NBN urn:nbn:hr:217:064447 Study programme Title: Computer Science and Mathematics Type of resource Text File origin Born digital Access conditions Open access Terms of use Created on 2019-03-01 12:28:17
