@INPROCEEDINGS{BeyersdorffChewSchmidtSuda16,
AUTHOR = {Beyersdorff, O. and Chew, L. and Schmidt, R. A. and Suda, M.},
YEAR = {2016},
TITLE = {Lifting QBF Resolution Calculi to DQBF},
EDITOR = {Creignou, N. and Le Berre, D.},
BOOKTITLE = {Theory and Applications of Satisfiability Testing (SAT 2016)},
SERIES = {Lecture Notes in Computer Science},
VOLUME = {9710},
PUBLISHER = {Springer},
DOI = {10.1007/978-3-319-40970-2_30},
PAGES = {490--499},
URL{http://www.cs.man.ac.uk/~schmidt/publications/BeyersdorffChewSchmidtSuda16.html},
ABSTRACT = {
We examine existing resolution systems for quantified Boolean 
formulas (QBF) and answer the question which of these calculi can 
be lifted to the more powerful Dependency QBFs (DQBF). An 
interesting picture emerges: While for QBF we have the strict 
chain of proof systems Q-Res < IR-calc < IRM-calc, the situation 
is quite different in DQBF. The obvious adaptations of Q-Res and 
likewise universal resolution are too weak: they are not complete. 
The obvious adaptation of IR-calc has the right strength: it is 
sound and complete. IRM-calc is too strong: it is not sound any 
more, and the same applies to long-distance resolution. 
Conceptually, we use the relation of DQBF to effectively 
propositional logic (EPR) and explain our new DQBF calculus based 
on IR-calc as a subsystem of first-order resolution.  
}
}