An Isaac Newton Institute Workshop

New Directions in Proof Complexity

Uniform Proof Complexity

Author: A Beckmann (University of Wales, Swansea)

Abstract

One main aim in Propositional Proof Complexity is to prove strong lower bounds for a general propositional proof system. Inspired by this program, we will introduce uniform reducts of propositional proof systems. Uniform reducts are sets of first order formulas of arithmetic which are defined using translations from first order formulas to propositional formulas. We will describe basic properties of uniform reducts, discuss their relationship to Cook's Programme, and explain some more advanced features of them. Recently, Steve Cook made an obervation relating the study of uniform reducts to the existence of optimal proof systems - if time permits we will touch on this as well.