Michael Alekhnovich, Eli Ben-Sasson, Alexander Razborov, Avi Wigderson

We study space complexity in the framework of

propositional proofs. We consider a natural model analogous to

Turing machines with a read-only input tape, and such

popular propositional proof systems as Resolution, Polynomial

Calculus and Frege systems. We propose two different space measures,

corresponding to the maximal number of bits, ...
more >>>

Lorenzo Carlucci, Nicola Galesi, Massimo Lauria

We initiate the study of the proof complexity of propositional encoding of (weak cases of) concrete independence results. In particular we study the proof complexity of Paris-Harrington's Large Ramsey Theorem. We prove a conditional lower bound in Resolution and a quasipolynomial upper bound in bounded-depth Frege.

more >>>Fu Li, Iddo Tzameret, Zhengyu Wang

Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional-calculus (i.e., Frege) proof is any proof starting from a set of axioms and deriving new Boolean formulas using a fixed set of sound derivation rules. Establishing any super-polynomial size lower bound on Frege proofs (in terms of the ... more >>>

Toniann Pitassi, Iddo Tzameret

We survey recent progress in the proof complexity of strong proof systems and its connection to algebraic circuit complexity, showing how the synergy between the two gives rise to new approaches to fundamental open questions, solutions to old problems, and new directions of research. In particular, we focus on tight ... more >>>

Leroy Chew

The proof complexity of Quantified Boolean Formulas (QBF) relates to both QBF solving and OBF certification. One method to p-simulate a QBF proof system is by formalising the soundness of its strategy extraction in propositional logic. In this work we illustrate how to use extended QBF Frege to simulate LD-Q(Drrs)-Res, ... more >>>