Show simple item record

dc.contributor.authorRen, Wei
dc.contributor.authorRen, Wei
dc.date.accessioned2011-08-24T02:10:29Z
dc.date.available2011-08-24T02:10:29Z
dc.date.issued2011
dc.identifier.urihttp://hdl.handle.net/10179/2629
dc.description.abstractIn 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.en_US
dc.publisherMassey Universityen_US
dc.rightsThe Authoren_US
dc.subjectBoolean logicen_US
dc.subjectSatisfiability problemen_US
dc.subjectComputer algorithmsen_US
dc.subjectLogic languagesen_US
dc.titleOn 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 Zealanden_US
dc.typeThesisen_US
thesis.degree.disciplineInformation Science
thesis.degree.grantorMassey University
thesis.degree.levelMasters
thesis.degree.nameMaster of Information Science (M.Inf.Sc.)


Files in this item

Icon
Icon

This item appears in the following Collection(s)

Show simple item record