Metoda tableauxa za modalnu logiku

Modalna logika motivirana je potrebom da se formaliziraju nužnost i mogućnost, znanje i vjerovanje, dokazivost i mnoga druga svojstva koja se mogu smatrati operatorima na logičkim sudovima. Unatoč jednostavnoj sintaksi koja osigurava odlučivost, modalna logika svojom izražajnošću predstavlja vrlo jako sredstvo za opis relacijskih struktura. Tradicionalno izlaganje logičkih formalizama obuhvaća definicije sintakse i semantike, te njihovo povezivanje putem teorema adekvatnosti i potpunosti odgovarajućeg hilbertovskog aksiomatskog sistema. Radi ekonomičnosti dokaza ključnih teorema, aksiomatski sistemi su minimalni, odnosno koriste vrlo malo pravila zaključivanja. Zbog toga su formalni dokazi takvih sistema intuitivno vrlo teško razumljivi. Metoda tableauxa ili semantičkih stabala jedna je metoda testiranja ispunjivosti logičkih formula (tzv. glavni test). Ako je adekvatan i potpun, test metodom semantičkog stabla predstavlja alternativni sistem dokazivanja, jer se glavni test za valjanu formulu može smatrati njenim dokazom. Semantička stabla intuitivno su jasnija od dokaza u hilbertovskim aksiomatskim sistemima. U radu je opisana metoda tableauxa za osnovni modalni jezik i dokazani su teoremi adekvatnosti i potpunosti. Rad završava diskusijom o pitanju odlučivosti.