Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
type: Item
instance of: scholarly article
title: Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
zbMATH Open document ID: 1332.68204
author: Friedrich Slivovsky
author: Stefan Szeider
published in: Theoretical Computer Science
publication date: 2015-12-15T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 6521254
zbMATH Keywords: quantified Boolean formulas
zbMATH Keywords: qbf
zbMATH Keywords: \(\mathcal{Q}\)-resolution
zbMATH Keywords: dependency schemes
MaRDI profile type: Publication
full work available at URL: j.tcs.2015.10.020
OpenAlex ID: W2191125414
cites work: Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
cites work: Unified QBF certification and its applications
cites work: Integrating Dependency Schemes in Search-Based QBF Solvers
cites work: Q4553262
cites work: Q3566747
cites work: Resolution for quantified Boolean formulas
cites work: An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
cites work: A machine program for theorem-proving
cites work: Q3624018
cites work: A Unified Proof System for QBF Preprocessing
cites work: On Unification of QBF Resolution-Based Calculi
cites work: On Propositional QBF Expansions and Q-Resolution
cites work: Lower bounds for multiplayer noncooperative games of incomplete information
cites work: Variable Dependencies of Quantified CSPs
cites work: Backdoor sets of quantified Boolean formulas
cites work: Computing Resolution-Path Dependencies in Linear Time ,
cites work: Variable Independence and Resolution Paths for Quantified Boolean Formulas
DOI: 10.1016/J.TCS.2015.10.020
description: scientific article; zbMATH DE number 6521254