Davis and Putnam meet Henkin: solving DQBF with resolution
type: Item
instance of: scholarly article
title: Davis and Putnam meet Henkin: solving DQBF with resolution
DOI: 10.1007/978-3-030-80223-3_4
author: Joshua Blinkhorn
author: Tomáš Peitl
author: Friedrich Slivovsky
publication date: 2022-03-22T00:00:00Z
Mathematics Subject Classification ID: 68Q25
Mathematics Subject Classification ID: 68R07
Mathematics Subject Classification ID: 68T20
zbMATH DE Number: 7495564
describes a project that uses: dCAQE
MaRDI profile type: Publication
full work available at URL: 978-3-030-80223-3 4
OpenAlex ID: W3185782780
cites work: Lower bounds for multiplayer noncooperative games of incomplete information
cites work: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
cites work: Building strategies into QBF proofs
cites work: Theory and Applications of Satisfiability Testing
cites work: Dependency Quantified Horn Formulas: Models and Complexity
cites work: Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
cites work: Small Stone in Pool
cites work: Q4411139
cites work: A Computing Procedure for Quantification Theory
cites work: Encodings of Bounded Synthesis
cites work: Resolution for quantified Boolean formulas
cites work: A structure-preserving clause form translation
cites work: Incremental Determinization
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Q4131648
cites work: Clausal abstraction for DQBF
cites work: Q5593816
description: scientific article; zbMATH DE number 7495564