Expressing properties in second- and third-order logic: hypercube graphs and SATQBF

Autoren Flavio Ferrarotti
Wei Ren
Jose Maria Turull Torres
Titel Expressing properties in second- and third-order 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 1368-9894 - Print ISSN 1367-0751
Monat April
Jahr 2014
Seiten 355-386
SCCH ID# 1418

It follows from the famous Fagin’s theorem that all problems in NP are expressible in existential second-order logic (9SO), and vice versa. Indeed, there are well-known 9SO characterizations of NPcomplete problems such as 3-colorability, 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 second-order 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 second-order sentences. Finally, we sketch a third-order logic sentence that defines the class SATQBF = Sk≥1SATQBFk. The sub-formulae used in the construction of these complex second- and third-order 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.