We aim to understand inherent reasons for lower bounds for QBF proof systems and revisit and compare two previous approaches in this direction.

The first of these relates size lower bounds for strong QBF Frege systems to circuit lower bounds via strategy extraction (Beyersdorff & Pich, LICS'16). Here we ... more >>>

A fundamental notion in Algorithmic Statistics is that of a stochastic object, i.e., an object having a simple plausible explanation. Informally, a probability distribution is a plausible explanation for $x$ if it looks likely that $x$ was drawn at random with respect to that distribution. In this paper, we ... more >>>

We prove new lower bounds on the sizes of proofs in the Cutting Plane proof system, using a concept that we call "unsatisfiability certificate". This approach is, essentially, equivalent to the well-known feasible interpolation method, but is applicable to CNF formulas that do not seem suitable for interpolation. Specifically, we ... more >>>