[Proof Complexity] New preprint

[Olaf Beyersdorff]

Dear Colleagues,

A new preprint 'Understanding Gentzen and Frege Systems for QBF’ by Jan Pich and myself is available at http://eccc.hpi-web.de/report/2016/011/ The abstract is attached below.

Comments and suggestions are very welcome.

Best wishes
Olaf


Abstract:
Recently Beyersdorff, Bonacina, and Chew (ITCS'16) introduced a natural class of Frege systems for quantified Boolean formulas (QBF) and showed strong lower bounds for restricted versions of these systems. Here we provide a comprehensive analysis of their new extended Frege system, denoted EF+red, which is a natural extension of classical extended Frege EF.

Our main results are the following:

Firstly, we prove that the standard Gentzen-style system G_1^* p-simulates EF+red and that G_1^* is strictly stronger under standard complexity-theoretic hardness assumptions.

Secondly, we show a correspondence of EF+red to bounded arithmetic: EF+red can be seen as the non-uniform propositional version of intuitionistic S^1_2. Specifically, intuitionistic S^1_2 proofs of arbitrary statements in prenex form translate to polynomial-size EF+red proofs, and EF+red is in a sense the weakest system with this property.

Finally, we show that unconditional lower bounds for EF+red would imply either a major breakthrough in circuit complexity or in classical proof complexity, and in fact the converse implications hold as well. Therefore, the system EF+red naturally unites the central problems from circuit and proof complexity.

Technically, our results rest on a formalised strategy extraction theorem for EF+red akin to witnessing in intuitionistic S^1_2 and a normal form for EF+red proofs.





--
Dr Olaf Beyersdorff,  Associate Professor
School of Computing
University of Leeds, Leeds, LS2 9JT, UK.
Phone: +44 113 343 8319
Email: O.Beyersdorff at leeds.ac.uk<mailto:O.Beyersdorff at leeds.ac.uk>
http://www.engineering.leeds.ac.uk/people/computing/staff/o.beyersdorff