
TSpace at The University of Toronto Libraries >
School of Graduate Studies  Theses >
Doctoral >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1807/17477

Title:  Power of Nonuniformity in Proof Complexity 
Authors:  Perron, Steven 
Advisor:  Cook, Stephen A. 
Department:  Computer Science 
Keywords:  proof complexity computational complexity 
Issue Date:  17Jul2009 
Abstract:  As the title indicates, this thesis is concerned with the strength of nonuniformity in proof complexity. The
nonuniform part is there because we look at quantified propositional proof systems. With these proof systems we are interested in the minimum size of proofs that prove a family of tautologies. Like circuits, these proofs are not necessarily easy to construct. We measure the strength of a
proof system by characterizing which families of tautologies have polynomialsize proofs in the proof system.
The proof systems we examine were first introduced by Kraj\'{\i}cek and Pudl{\'a}k \cite{KP90}, but have only received
limited attention since then. These systems are called $G_i$ and $G_i^*$. $G_i$ is the propositional version of Gentzen's $LK$ with cut formulas restricted to formulas with
$i1$ quantifier alternations, and $G_i^*$ is the treelike version of $G_i$.
We look at the strength of these proof systems in three ways. The first is to compare them with bounded arithmetic. We find the weakest theory that can prove that a given proof system is sound. The second method is to compare proof systems with respect to computational complexity. We determine the complexity of finding a witness for the outermost existential quantifiers of a formula given a proof of that formula. The final method is to compare the proof systems to each other. This is done using the notion of $p$simulations. An important tool in all of this work is an adaptation of the Herbrand theorem for the propositional setting. Most prooftheoretic proofs of the Herbrand
theorem require cutelimination which causes the size of the proof to increase exponentially. We adapt the statement of
the theorem and the proof to avoid this increase.
We finish by defining new proof systems that meet given requirements. The goal is to determine where proof systems get their strength. In all cases, it comes down to the
eigenvariables. The strength of a proof system that allows quantifiers in the cut formulas is determined by the difficulty of witnessing the eigenvariables. 
URI:  http://hdl.handle.net/1807/17477 
Appears in Collections:  Doctoral Department of Computer Science  Doctoral theses

This item is licensed under a Creative Commons License
Items in TSpace are protected by copyright, with all rights reserved, unless otherwise indicated.
