Towards Uniform Certification in QBF

DOI10.46298/lmcs-20(1:14)2024arXiv2210.07085v4OpenAlexW3215442047MaRDI QIDQ6151563

Friedrich Slivovsky, Leroy Chew

Publication date: 11 March 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2210.07085v4

zbMATH Keywords

verificationFregeproof complexityQBFextended Fregestrategy extraction

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Unnamed Item
• Solving QBF with counterexample guided refinement
• Local soundness for QBF calculi
• A little blocked literal goes a long way
• Understanding cutting planes for QBFs
• Resolution for quantified Boolean formulas
• Building strategies into QBF proofs
• Hardness and optimality in QBF proof systems modulo NP
• Expansion-based QBF solving versus Q-resolution
• Solution validation and extraction for QBF preprocessing
• Efficient certified RAT verification
• Long-distance Q-resolution with dependency schemes
• Unified QBF certification and its applications
• Multi-linear strategy extraction for QBF expansion proofs via local soundness
• Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
• On Unification of QBF Resolution-Based Calculi
• QBF Resolution Systems and Their Proof Complexities
• DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
• Quantified propositional calculi and fragments of bounded arithmetic
• A First Step Towards a Unified Proof Checker for QBF
• On the correspondence between arithmetic theories and propositional proof systems – a survey
• The relative efficiency of propositional proof systems
• Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
• Proof Complexity
• Contributions to the Theory of Practical Quantified Boolean Formula Solving
• Automated Testing and Debugging of SAT and QBF Solvers
• Integrating Dependency Schemes in Search-Based QBF Solvers
• Dependency Learning for QBF
• Frege Systems for Quantified Boolean Logic
• New Resolution-Based QBF Calculi and Their Proof Complexity
• Computational Complexity