Abstract:
Propositional proof complexity–a sub-branch of computational complexity–is an extensively studied area, with a number of lower bound techniques for various propositional proof systems (for example Resolution, and Cutting Planes). The purpose of this thesis is to assess whether similar techniques are applicable for proof systems
for quantified Boolean formulas (QBFs). The major contributions of this work are
as follows:
1. We show that level-ordered Q-resolution and tree-like Q-resolution, two restrictions of Q-resolution system, are incomparable.
2. We establish the feasible interpolation technique, first introduced by Krajıˇcek
for Resolution [62], to all CDCL-based QBF Resolution calculi. This provides
the first general lower bound method for CDCL-based QBF calculi and also
extends the scope of the feasible interpolation technique.
3. We introduce a cutting planes system CP+∀red for QBFs and analyse the
proof-theoretical strength of this new calculus. We also establish the strategy
extraction technique and feasible interpolation technique for the new calculi.
4. We show that both the size-width relation, established by Ben-Sasson and
Wigderson in [9], and space-width relation, established by Atserias and Dal-
mau in [3], for the Resolution proof system drastically fail in Q-resolution, even
in its weaker tree-like version.
