Results on Computational Logics : Complexity, Expressivity and Model Theory

Abstract

Laskennalliset logiikat ovat logiikoita, joilla on joko hyvät laskennalliset ominaisuudet tai joita voidaan käyttää laskennan mallintamiseen. Tässä väitöskirjassa tarkastelemme useita laskennallisia logiikoita ja esitämme uusia tuloksia niiden ilmaisukyvystä, malliteoriasta ja laskennallisesta vaativuudesta.

Väitöskirja koostuu kolmesta osasta. Ensimmäisessä osassa tutkimme Craigin interpolaatiota (CIP) guarded fragmentin (GF) fragmenteille. Osoitamme, että guarded fragmentin uniformi yksiulotteinen fragmentti omaa Craigin interpolaatio-ominaisuuden. Näytämme myös, että sekä uniformius että yksiulotteisuus ovat välttämättömiä: pelkkä yksiulotteinen GF tai pelkkä uniformi GF ei omaa CIP:tä. Toisaalta osoitamme, että uniformi GF sallii interpolantit koko GF:ssä. Lisäksi näytämme, että uniformin GF:n toteutuvuusongelma on NExpTıme-täydellinen.

Toisessa osassa tutkimme polyadisten Boolen modaalilogiikoiden laskennallista vaativuutta. Osoitamme, että negaation sisältävän polyadisen modaalilogiikan toteutuvuusongelma on ExpTıme-täydellinen. Osoitamme myös, että permutaatiot sisältävän polyadisen Boolen modaalilogiikan toteutuvuusongelma on ExpTıme-täydellinen kiinnitetyllä äärellisellä aakkostolla. Lisäksi näytämme, että tämän logiikan mallintarkistusongelman yhdistetty vaativuus on PTıme-täydellinen.

Kolmannessa osassa kehitämme staattisen laskennallisen logiikan (SCL) teoriaa. Osoitamme, että SCL on ekvivalentti pienimmän kiintopisteen logiikan fragmentin kanssa. Esittelemme rajoitetun SCL:n, joka on SCL:n semanttinen variantti, ja todistamme sen olevan aidosti vähemmän ilmaisuvoimainen kuin SCL. Osoitamme myös, että rekursiivisesti saturoituneissa malleissa näillä kahdella logiikalla on sama ilmaisuvoima. Näytämme, että molempien logiikoiden kahden muuttujan fragmenttien validiteettiongelmat ovat coNExpTıme-täydellisiä, kun taas niiden toteutuvuusongelmat ovat ratkeamattomia. Lopuksi todistamme useita SCL:n malliteoreettisia ominaisuuksia ja liitämme ne Lindströmin toiseen lauseeseen.

Computational logics are logics that either have good computational properties or they can be used to model computation. In this thesis we investigate several computational logics, presenting new results on their expressive power, model theory and computational complexity.

This thesis consist of three parts. The first part studies Craig interpolation for fragments of the guarded fragment (GF). We prove that the uniform one-dimensional fragment of GF has the Craig interpolation property (CIP). We demonstrate that both uniformity and one-dimensionality are necessary requirements by showing that neither the one-dimensional GF nor the uniform GF alone possesses CIP. However, we show that uniform GF admits interpolants in the full GF. Additionally, we show that the satisfiability problem for uniform GF is NExpTıme-complete.

The second part investigates the computational complexity of polyadic Boolean modal logics. We prove that the satisfiability problem for polyadic modal logic with negation is ExpTıme-complete. Furthermore, we establish that polyadic Boolean modal logic with permutations has an ExpTıme-complete satisfiability problem when the underlying vocabulary is fixed and finite. We also show that the combined complexity of the model checking problem for this logic is PTıme-complete.

The third part develops the background theory of static computation logic (SCL). We establish that SCL is equivalent to a fragment of least fixed point logic. We introduce bounded SCL, which is a semantical variant of SCL, and prove that it is stricly less expressive than SCL. We also show that over recursively saturated structures the two logics have equal expressive power. We establish that the validity problems for the two-variable fragments of both logics are coNExpTıme-complete, while their satisfiability problems are undecidable. Finally, we prove several model-theoretic properties of SCL and link them to Lindström’s second theorem.