Odlučivost modalnih logika

diplomski rad

• Autor: Tamara Bistrović
• Mentor: Mladen Vuković (mentor)
• Član povjerenstva: Mladen Vuković (predsjednik povjerenstva)
• Član povjerenstva: Vedran Čačić (član povjerenstva)
• Član povjerenstva: Marko Horvat (član povjerenstva)
• Član povjerenstva: Zvonko Iljazović (član povjerenstva)
• Ustanova koja je dodijelila akademski / stručni stupanj: Sveučilište u Zagrebu; Prirodoslovno-matematički fakultet; Zagreb
• Datum i država obrane: 2020-09-28, Hrvatska
• Znanstveno / umjetničko područje, polje i grana: PRIRODNE ZNANOSTI; Matematika

Sažetak

Osnovni modalni jezik je proširenje alfabeta propozicionalne logike modalnim operatorom mogućnosti \( \lozenge\). Unatoč toj sintaktičkoj sličnosti s logikom sudova, modalne logike su u suštini fragmenti logika prvog i drugog reda. Zato se postavlja pitanje što možemo zaključiti o njihovoj odlučivosti. Cilj ovog rada je dokazivanje odlučivosti većeg broja normalnih modalnih logika koristeći njihovo svojstvo konačnih modela. U prvom poglavlju opisujemo osnove sintakse i semantike osnovnog modalnog jezika. Normalne modalne logike su skupovi formula osnovnog modalnog jezika koje su dobivene iz aksioma primjenom pravila izvoda. Najmanja normalna modalna logika je K, a njena proširenja se dobivaju dodavanjem poželjnih aksioma. U drugom poglavlju dokazujemo da osnovni modalni jezik ima svojstvo konačnih modela. To znači da je svaka ispunjiva formula osnovnog modalnog jezika ispunjiva i na konačnom modelu. Svojstvo konačnih modela imaju i mnoge normalne modalne logike i ono se dokazuje koristeći dvije metode: selekcije i filtracije. Promatramo i svojstvo konačnih okvira iz razloga što su okviri pogodniji za pokazivanje valjanosti formula. Naposljetku dokazujemo ekvivalentnost ta dva svojstva. U posljednjem poglavlju objašnjavamo način na koji prikazujemo modalnu logiku na traci Turingovog stroja. Uvodimo dvije strategije za dokazivanje odlučivosti logika. One se razlikuju po načinu na koji je logika zadana: semantički kao logika neke klase okvira ili sintaktički aksiomima. Obje strategije se zasnivaju na svojstvu konačnih modela i daju rezultate za puno poznatih modalnih logika uključujući i sva proširenja logike S4:3.

Sažetak (engleski)

The basic modal language extends the alphabet of the propositional logic using a modal operator of possibility \(\lozenge\). Although they share syntax similarity with propositional logic, modal logics are basically fragments of first- and second-order logics. That implies the question of their decidability. The main goal of this work is to prove that a lot of normal modal logics are decidable using their finite model property. In the first chapter we describe the fundamentals of the basic modal language syntax and semantics. A normal modal logic is a set of basic modal language formulas which are generated from the axioms using rules of proof. The smallest normal modal logic is K. Its extensions are created by adding more axioms. In the second chapter we prove that the basic modal language has the finite model property. That means that every satisfiable formula of the basic modal language is satisfiable on some finite model. Many normal modal logics have the finite model property. We prove that by using two di erent methods: selection and filtration. We observe the finite frame property as well because frames are more suited for showing the validity of formulas. Lastly, we prove the equality between those two properties. In the final chapter we explain the manner in which we represent modal logic on the tape of a Turing machine. We introduce two strategies for proving the decidability of logics. They di er by the way the logic is specified: semantically as the logic of some class of frames or syntactically by axioms. Both strategies are based on the finite model property and they hand results for many known modal logics including all extensions of logic S4:3.

• Ključne riječi: modalni jezik; konačni model
• Ključne riječi (engleski): the basic modal language; finite model
• Jezik: hrvatski
• URN:NBN: urn:nbn:hr:217:204518
• 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: 2020-12-01 15:12:32