How QBF expansion makes strategy extraction hard

DOI10.1007/978-3-030-51074-9_5OpenAlexW2997716221MaRDI QIDQ2096438

Leroy Chew, Judith Clymo

Publication date: 9 November 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-51074-9_5

zbMATH Keywords

proof complexityQBFfeasible interpolationQRATquantifier expansionstrategy extraction

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Hardness and optimality in QBF proof systems modulo NP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the complexity of cutting-plane proofs
• Some consequences of cryptographical conjectures for \(S_2^1\) and EF
• A little blocked literal goes a long way
• Understanding cutting planes for QBFs
• \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
• Resolution for quantified Boolean formulas
• Short proofs in QBF expansion
• The equivalences of refutational QRAT
• QRAT polynomially simulates \(\forall\)-Exp+Res
• Expansion-based QBF solving versus Q-resolution
• Lower Bounds
• Solving QBF with Counterexample Guided Refinement
• A Unified Proof System for QBF Preprocessing
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits
• The relative efficiency of propositional proof systems
• Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
• Lower bounds for resolution and cutting plane proofs and monotone computations

This page was built for publication: How QBF expansion makes strategy extraction hard