A New Characterisation of Propositional Proofs

Does every Boolean tautology have a short propositional-calculus proof? Here, a propositional calculus proof is a proof starting from a set of axioms and deriving new Boolean formulas using a set of fixed sound derivation rules. Establishing any strong size lower bound on propositional-calculus proofs (in terms of the size of the formulas proved) is a major open problem in proof complexity, and among a handful of fundamental hardness questions in complexity theory by and large. It has also bearing on efficient SAT-solving and other proof-search algorithms. In this talk I will show that in fact lower bounds on propositional-calculus proofs follow from certain size lower bounds on a very weak model of computation, namely, non-commutative arithmetic formulas. For this weak model of computation, many strong size lower bounds are already known since the early 90s. The argument is a new characterization of propositional proofs as non-commutative formulas.

(No specific prior knowledge will be assumed. Based on a joint work with Fu Li and Zhengyu Wang.)