Frege Systems for Quantified Boolean Logic

DOI10.1145/3381881zbMath1494.03091OpenAlexW3014737894WikidataQ118123548 ScholiaQ118123548MaRDI QIDQ5133965

Leroy Chew, Ilario Bonacina, Ján Pich, Olaf Beyersdorff

Publication date: 11 November 2020

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://ora.ox.ac.uk/objects/uuid:0a74f630-1bf6-4dfd-8a64-055cd9fde488

zbMATH Keywords

sequent calculussimulationslower boundsintuitionistic logicFrege systemsstrategy extractionQBF proof complexity

Mathematics Subject Classification ID

Complexity of proofs (03F20)

Related Items (8)

Proof complexity of modal resolution ⋮ A simple proof of QBF hardness ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Towards Uniform Certification in QBF ⋮ Lower bounds for QCDCL via formula gauge ⋮ Lower bounds for QCDCL via formula gauge ⋮ Hardness and optimality in QBF proof systems modulo NP ⋮ Proof complexity of symbolic QBF reasoning

This page was built for publication: Frege Systems for Quantified Boolean Logic