Building strategies into QBF proofs
type: Item
instance of: scholarly article
title: Building strategies into QBF proofs
author: Olaf Beyersdorff
author: Joshua Blinkhorn
author: Meena Mahajan
published in: Journal of Automated Reasoning
publication date: 2021-06-09T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7356969
zbMATH Keywords: QBF
zbMATH Keywords: DQBF
zbMATH Keywords: resolution
zbMATH Keywords: proof complexity
Wikidata QID: Q113901241
describes a project that uses: sKizzo
describes a project that uses: dCAQE
describes a project that uses: CAQE
describes a project that uses: Quaffle
describes a project that uses: Easychair
describes a project that uses: HQSpre
MaRDI profile type: Publication
full work available at URL: s10817-020-09560-1
OpenAlex ID: W3028147070
cites work: Lower bounds for multiplayer noncooperative games of incomplete information
cites work: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
cites work: Unified QBF certification and its applications
cites work: Automated Deduction – CADE-20
cites work: Q3620436
cites work: Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
cites work: Q4625702
cites work: Q5090460
cites work: Lower bounds: from circuits to QBF proof systems
cites work: New Resolution-Based QBF Calculi and Their Proof Complexity
cites work: Lifting QBF Resolution Calculi to DQBF
cites work: Dependency Quantified Horn Formulas: Models and Complexity
cites work: Towards NP-P via proof complexity and search
cites work: Q3457218
cites work: Q5306365
cites work: The relative efficiency of propositional proof systems
cites work: Conformant planning as a case study of incremental QBF solving
cites work: Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
cites work: Encodings of Bounded Synthesis
cites work: Fast DQBF Refutation
cites work: Q3624018
cites work: Expansion-based QBF solving versus Q-resolution
cites work: Resolution for quantified Boolean formulas
cites work: A Non-prenex, Non-clausal QBF Solver with Game-State Learning
cites work: Q4856172
cites work: Theory and Applications of Satisfiability Testing
cites work: Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test
cites work: Handbook of Model Checking
cites work: Long Distance Q-Resolution with Dependency Schemes
cites work: Dependency learning for QBF
cites work: Polynomial-time validation of QCDCL certificates
cites work: Proof complexity of fragments of long-distance Q-resolution
cites work: A resolution-style proof system for DQBF
cites work: Q5503674
cites work: Local soundness for QBF calculi
cites work: Clausal abstraction for DQBF
cites work: Preprocessing for DQBF
DOI: 10.1007/S10817-020-09560-1
Recommended article: Q5090460
Recommended article: Strategic construction of Fitch-style proofs
Recommended article: On QBF Proofs and Preprocessing
Recommended article: How QBF expansion makes strategy extraction hard
Recommended article: Q4941840
Recommended article: Building Theorem Provers
Recommended article: QBF Resolution Systems and Their Proof Complexities
Recommended article: Lower Bound Techniques for QBF Proof Systems
Recommended article: Multi-linear strategy extraction for QBF expansion proofs via local soundness
Recommended article: On Stronger Calculi for QBFs
description: scientific article; zbMATH DE number 7356969