Henkin quantifiers and Boolean formulae: a certification perspective of DQBF

DOI10.1016/j.tcs.2013.12.020zbMath1283.03032OpenAlexW2102022086MaRDI QIDQ2435315

Jie-Hong R. Jiang, Hui-Ju Katherine Chiang, Valeriy Balabanov

Publication date: 4 February 2014

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2013.12.020

zbMATH Keywords

Henkin quantifierresolutionconsensusquantified Boolean formulaSkolem functionHerbrand function

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic with extra quantifiers and operators (03C80)

Related Items

Hardness Characterisations and Size-width Lower Bounds for QBF Resolution, Preprocessing for DQBF, Solving dependency quantified Boolean formulas using quantifier localization, A resolution proof system for dependency stochastic Boolean satisfiability, Soundness of \(\mathcal{Q}\)-resolution with dependency schemes, Partial-order Boolean games: informational independence in a logic-based model of strategic interaction, Unnamed Item, Building strategies into QBF proofs, Pruning external minimality checking for answer set programs using semantic dependencies, Dependency Schemes for DQBF, Lifting QBF Resolution Calculi to DQBF, Reinterpreting dependency schemes: soundness meets incompleteness in DQBF, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, Davis and Putnam meet Henkin: solving DQBF with resolution, Certified DQBF solving by definition extraction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Henkin quantifiers and complete problems
• The polynomial-time hierarchy
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Resolution for quantified Boolean formulas
• Unified QBF certification and its applications
• Henkin Quantifiers and Boolean Formulae
• Equivalence and quantifier rules for logic with imperfect information
• Logic for Programming, Artificial Intelligence, and Reasoning
• Dependency Quantified Horn Formulas: Models and Complexity
• Lower bounds for multiplayer noncooperative games of incomplete information