کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
438331 | 690259 | 2014 | 15 صفحه PDF | دانلود رایگان |
![عکس صفحه اول مقاله: Henkin quantifiers and Boolean formulae: A certification perspective of DQBF Henkin quantifiers and Boolean formulae: A certification perspective of DQBF](/preview/png/438331.png)
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.
Journal: Theoretical Computer Science - Volume 523, 27 February 2014, Pages 86–100