Henkin quantifiers and Boolean formulae

Abstract

Henkin quantifiers, when applied on Boolean formulae, yielding the so-called dependency quantified Boolean formulae (DQBF), offer succinct descriptive power specifying variable dependencies. Despite their natural applications to games with incomplete information, logic synthesis with constrained input dependencies, etc., DQBF remain a relatively unexplored subject however. This paper investigates their basic properties, including formula negation and complement, formula expansion, and prenex and non-prenex form conversions. In particular, the proposed DQBF formulation is established from a synthesis perspective concerned with Skolem-function models and Herbrand-function countermodels. © 2012 Springer-Verlag.