Davis and Putnam meet Henkin: solving DQBF with resolution
From MaRDI portal
(Redirected from Davis and Putnam meet Henkin: solving DQBF with resolution)
Cites work
- A Computing Procedure for Quantification Theory
- A structure-preserving clause form translation
- Building strategies into QBF proofs
- Clausal abstraction for DQBF
- Dependency Quantified Horn Formulas: Models and Complexity
- Encodings of bounded synthesis
- Graph-Based Algorithms for Boolean Function Manipulation
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- scientific article; zbMATH DE number 3560737 (Why is no real title available?)
- scientific article; zbMATH DE number 1946853 (Why is no real title available?)
- scientific article; zbMATH DE number 3313427 (Why is no real title available?)
- Incremental determinization
- Lower bounds for multiplayer noncooperative games of incomplete information
- Resolution for quantified Boolean formulas
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
- Small Stone in pool
- Theory and Applications of Satisfiability Testing
Cited in
(6)- A resolution proof system for dependency stochastic Boolean satisfiability
- Transforming quantified Boolean formulas using biclique covers
- QBF merge resolution is powerful but unnatural
- Hard QBFs for merge resolution
- Extending merge resolution to a family of QBF-proof systems
- On the interplay of cube learning and dependency schemes in QCDCL proof systems
This page was built for publication: Davis and Putnam meet Henkin: solving DQBF with resolution
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2118283)
