Provider: DSpace RIS Export
Database: Massey Research Online (MRO) Production Instance
Content: text/plain; charset="UTF-8"
TY - THES
AB - 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.
N2 - 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.
M3 - Masters
PY - 2011
KW - Boolean logic
KW - Satisfiability problem
KW - Computer algorithms
KW - Logic languages
PB - Massey University
AU - Ren, Wei
AU - Ren, Wei
TI - 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
VL - Master of Information Science (M.Inf.Sc.)
DA - 2011
UR - http://hdl.handle.net/10179/2629
ER -