Kiintopistelogiikoista

Abstract

Tässä tutkielmassa käsitellään kiintopistelogiikoiden ja vaativuusteorian välisiä yhteyksiä. Kiintopistelogiikoilla tarkoitetaan ensimmäisen kertaluvun predikaattilogiikan laajennuksia, ja ne määritellään tutkielman alkupuolella. Tutkielmassa keskeisessä roolissa ovat pienin, inflatorinen ja osittainen kiintopistelogiikka. Vaativuusteorian puolelta esitellään deterministiset Turingin koneet, joita käytetään arvioimaan laskennan vaativuutta. Mielenkiinnon kohteita ovat polynomisen tilan ja polynomisen ajan vaativuusluokat PSPACE ja PTIME. Tutkielman loppupuolella todistetaan, että osittainen kiintopistelogiikka karakterisoi polynomisen tilavaativuusluokan PSPACE. Todistuksessa hyödynnetään järjestettyjä malleja koodattuna tilavaativuusluokkaan kuuluvien Turingin koneiden syötteiksi. Tällöin voidaan osoittaa, että aina kun polynomisesti tilarajoitettu Turingin kone hyväksyy jonkin järjestettyjen mallien luokan, niin on olemassa osittaisen kiintopistelogiikan lause, joka määrittelee kyseisen luokan. Toiseen suuntaan todistetaan, että jos osittaisen kiintopistelogiikan lause määrittelee jonkin järjestettyjen mallien luokan, niin on olemassa polynomisesti tilarajoitettu Turingin kone, joka hyväksyy syötteenään täsmälleen kyseisen luokan mallit. Vastaavaan tapaan todistetaan, että inflatorinen kiintopistelogiikka karakterisoi polynomisen aikavaativuusluokan PTIME.