Davis and Putnam meet Henkin: solving DQBF with resolution (Q2118283): Difference between revisions

@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-030-80223-3_4
+Normal rank
@@ Property / OpenAlex ID @@
+W3185782780
@@ Property / OpenAlex ID: W3185782780 / rank @@
+Normal rank
@@ Property / cites work @@
+Lower bounds for multiplayer noncooperative games of incomplete information
+Normal rank
@@ Property / cites work @@
+Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
+Normal rank
@@ Property / cites work @@
+Building strategies into QBF proofs
@@ Property / cites work: Building strategies into QBF proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Dependency Quantified Horn Formulas: Models and Complexity
+Normal rank
@@ Property / cites work @@
+Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
+Normal rank
@@ Property / cites work @@
+Small Stone in Pool
@@ Property / cites work: Small Stone in Pool / rank @@
+Normal rank
@@ Property / cites work @@
+Q4411139
@@ Property / cites work: Q4411139 / rank @@
+Normal rank
@@ Property / cites work @@
+A Computing Procedure for Quantification Theory
@@ Property / cites work: A Computing Procedure for Quantification Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Encodings of Bounded Synthesis
@@ Property / cites work: Encodings of Bounded Synthesis / rank @@
+Normal rank
@@ Property / cites work @@
+Resolution for quantified Boolean formulas
@@ Property / cites work: Resolution for quantified Boolean formulas / rank @@
+Normal rank
@@ Property / cites work @@
+A structure-preserving clause form translation
@@ Property / cites work: A structure-preserving clause form translation / rank @@
+Normal rank
@@ Property / cites work @@
+Incremental Determinization
@@ Property / cites work: Incremental Determinization / rank @@
+Normal rank
@@ Property / cites work @@
+Graph-Based Algorithms for Boolean Function Manipulation
+Normal rank
@@ Property / cites work @@
+Q4131648
@@ Property / cites work: Q4131648 / rank @@
+Normal rank
@@ Property / cites work @@
+Clausal abstraction for DQBF
@@ Property / cites work: Clausal abstraction for DQBF / rank @@
+Normal rank
@@ Property / cites work @@
+Q5593816
@@ Property / cites work: Q5593816 / rank @@
+Normal rank