How QBF expansion makes strategy extraction hard
type: Item
instance of: scholarly article
title: How QBF expansion makes strategy extraction hard
DOI: 10.1007/978-3-030-51074-9_5
author: Leroy Chew
author: Judith Clymo
publication date: 2022-11-09T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7614507
zbMATH Keywords: QBF
zbMATH Keywords: proof complexity
zbMATH Keywords: QRAT
zbMATH Keywords: strategy extraction
zbMATH Keywords: quantifier expansion
zbMATH Keywords: feasible interpolation
MaRDI profile type: Publication
full work available at URL: 978-3-030-51074-9 5
OpenAlex ID: W2997716221
cites work: Lower bounds: from circuits to QBF proof systems
cites work: Short proofs in QBF expansion
cites work: Q2954985
cites work: Q5270089
cites work: Understanding cutting planes for QBFs
cites work: Q5136303
cites work: The equivalences of refutational QRAT
cites work: The relative efficiency of propositional proof systems
cites work: On the complexity of cutting-plane proofs
cites work: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
cites work: A Unified Proof System for QBF Preprocessing
cites work: Solving QBF with Counterexample Guided Refinement
cites work: Expansion-based QBF solving versus Q-resolution
cites work: A little blocked literal goes a long way
cites work: QRAT polynomially simulates \(\forall\)-Exp+Res
cites work: Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits
cites work: Resolution for quantified Boolean formulas
cites work: Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic
cites work: Some consequences of cryptographical conjectures for \(S_2^1\) and EF
cites work: \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
cites work: Lower bounds for resolution and cutting plane proofs and monotone computations
description: scientific article; zbMATH DE number 7614507