On the descriptive complexity of satisfiability on quantified Boolean formulas : a thesis presented in partial fulfilment of the requirements for the degree of Master of Information Sciences at Massey University, Wellington, New Zealand

Abstract

In the present thesis, we deal with the construction of non trivial formulas in higher order logic languages. In particular, we focus on using SO (Second-Order logic) and TO (Third-Order logic) to express SATQBFk, and SATQBF respectively. First of all, we explain the relationship between logic languages and complexity classes. Then we give formal definitions and examples for FO (First-Order), SO and HO (i≥2) (Higher-Order logic). It is known that, for every k ≥1, SATQBFk is a complete problem for the level Σ [superscript P subscript k] of PH (Polynomial-time hierarchy), and that SATQBF is a complete problem for PSPACE. As the expressibility of SO is known to equal the class PH, then we know that there must be an SO formula which can express SATQBFk. On the other hand, PSPACE is known to be equal in expressive power to SO with the addition of a second order transitive closure quantifier, which is widely conjectured to be strictly more expressive than SO alone. As TO includes PSPACE , this means that there must be a TO formula that can express SATQBF . Here we give first a top down explanation on the use of SO to express SATQBFk. A detailed SO formula is presented. We then give a top down presentation of the sketch of a TO formula for SATQBF.