Henkin quantifiers and Boolean formulae: A certification perspective of DQBF

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