Nested Boolean functions or Boolean programs are an alternative to the quantified Boolean formula (QBF) characterization of polynomial space. The idea is to start with a set of Boolean functions given as propositional formulas and to define new functions as compositions or instantiations of previously defined ones. We investigate the relationship between function instantiation and quantification and present a compact representation of models and countermodels of QBFs with and without free variables as nested Boolean functions. The representation is symmetric with respect to Skolem models and Herbrand countermodels. For a formula with free variables, it can describe both kinds of models simultaneously in one complete equivalence model which can be Skolem or Herbrand depending on actual assignments to the free variables. © 2013 Springer-Verlag.
CITATION STYLE
Bubeck, U., & Kleine Büning, H. (2013). Nested Boolean functions as models for quantified Boolean formulas. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7962 LNCS, pp. 267–275). https://doi.org/10.1007/978-3-642-39071-5_20
Mendeley helps you to discover research relevant for your work.