Expressing properties in second and thirdorder logic: hypercube graphs and SATQBF
Autoren 
Flavio Ferrarotti Wei Ren Jose Maria Turull Torres 
Editoren 

Titel  Expressing properties in second and thirdorder logic: hypercube graphs and SATQBF 
Typ  Artikel 
Journal  Logic Journal of the IGPL: Special Issue: The Proceedings of the XVI EBL  16th Brazilian Logic Conference 2011 
Nummer  2 
Band  22 
DOI  10.1093/jigpal/jzt025 
ISSN  Online ISSN 13689894  Print ISSN 13670751 
Monat  April 
Jahr  2014 
Seiten  355386 
Abstract  It follows from the famous Fagin’s theorem that all problems in NP are expressible in existential secondorder logic (9SO), and vice versa. Indeed, there are wellknown 9SO characterizations of NPcomplete problems such as 3colorability, Hamiltonicity and clique. Furthermore, the 9SO sentences that characterize those problems are simple and elegant. However, there are also NP problems that do not seem to possess equally simple and elegant 9SO characterizations. In this work, we are mainly interested in this latter class of problems. In particular, we characterize in secondorder logic the class of hypercube graphs and the classes SATQBFk of satisfiable quantified Boolean formulae with k alternations of quantifiers. We also provide detailed descriptions of the strategies followed to obtain the corresponding nontrivial secondorder sentences. Finally, we sketch a thirdorder logic sentence that defines the class SATQBF = Sk≥1SATQBFk. The subformulae used in the construction of these complex second and thirdorder logic sentences, are good candidates to form part of a library of formulae. Same as libraries of frequently used functions simplify the writing of complex computer programs, a library of formulae could potentially simplify the writing of complex second and thirdorder queries, minimizing the probability of error. 