Sažetak
U ovom radu bavimo se metodama za dokazivanje odlučivosti modalnih logika. Pitanje odlučivosti problema ekvivalentno je pitanju mogućnosti stvaranja računalnog programa koji za svaku instancu tog problema uvijek ispiše rješenje. Kao takvo, posebno je bitno u današnjem dobu konstantnog razvoja računala. Prvo poglavlje pruža uvod u normalne modalne logike. Definiramo sintaksu i semantiku osnovnog modalnog jezika te neke sisteme modalne logike. Zatim, u drugom poglavlju definiramo svojstvo konačnih modela te pokazujemo korisnost tog svojstva za dokazivanje odlučivosti modalnih logika. Metoda dokazivanja odlučivosti koja koristi svojstvo konačnih modela naziva se metoda konačnih modela. Navest ćemo i neka ograničenja te metode. Točnije, dokazat ćemo da ne posjeduju svi odlučivi sistemi modalne logike svojstvo konačnih modela. Navedeno ograničenje prirodno povlači da trebamo razmotriti i neke druge metode. U trećem poglavlju dajemo dvije alternative metodi konačnih modela. To su metoda interpretacije i metoda kvazimodela. Dokazujemo odlučivost logike KvB na dva načina upravo koristeći te dvije metode. U zadnjem, četvrtom poglavlju prvo definiramo sintaksu i semantiku osnovnog temporalnog jezika. Zatim, definiramo temporalnu logiku KtN i metodom mozaika dokazujemo odlučivost te logike.
Ključne riječi
modalna logika odlučivost svojstvo konačnih modela
