test Browse by Author Names Browse by Titles of Works Browse by Subjects of Works Browse by Issue Dates of Works

Advanced Search
& Collections
Issue Date   
Sign on to:   
Receive email
My Account
authorized users
Edit Profile   
About T-Space   

T-Space 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 Non-uniformity in Proof Complexity
Authors: Perron, Steven
Advisor: Cook, Stephen A.
Department: Computer Science
Keywords: proof complexity
computational complexity
Issue Date: 17-Jul-2009
Abstract: As the title indicates, this thesis is concerned with the strength of non-uniformity in proof complexity. The non-uniform 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 polynomial-size 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 $i-1$ 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 proof-theoretic proofs of the Herbrand theorem require cut-elimination 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

Files in This Item:

File Description SizeFormat
Perron_Steven_J_200903_PhD_thesis.pdf536.42 kBAdobe PDF

This item is licensed under a Creative Commons License
Creative Commons

Items in T-Space are protected by copyright, with all rights reserved, unless otherwise indicated.