Hardness and optimality in QBF proof systems modulo NP
type: Item
instance of: scholarly article
title: Hardness and optimality in QBF proof systems modulo NP
DOI: 10.1007/978-3-030-80223-3_8
author: Leroy Chew
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: 7495568
zbMATH Keywords: QBF
zbMATH Keywords: proof complexity
zbMATH Keywords: simulation
zbMATH Keywords: resolution
zbMATH Keywords: extended Frege
zbMATH Keywords: NP oracles
zbMATH Keywords: optimal proof systems
zbMATH Keywords: strategy extraction
describes a project that uses: RAReQS
describes a project that uses: DepQBF
MaRDI profile type: Publication
full work available at URL: 978-3-030-80223-3 8
OpenAlex ID: W3185666742
cites work: Computational Complexity
cites work: Unified QBF certification and its applications
cites work: Approximation and Small-Depth Frege Proofs
cites work: Q4993272
cites work: Frege Systems for Quantified Boolean Logic
cites work: New Resolution-Based QBF Calculi and Their Proof Complexity
cites work: Q2954985
cites work: Q5136303
cites work: Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
cites work: How QBF expansion makes strategy extraction hard
cites work: The relative efficiency of propositional proof systems
cites work: Parity, circuits, and the polynomial-time hierarchy
cites work: The intractability of resolution
cites work: One-way permutations in NC 0
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: Dual weak pigeonhole principle, Boolean complexity, and derandomization
cites work: A First Step Towards a Unified Proof Checker for QBF
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: Q4856172
cites work: Q4381398
cites work: Q4298260
cites work: Q5593816
cites work: Contributions to the Theory of Practical Quantified Boolean Formula Solving
description: scientific article; zbMATH DE number 7495568