Propositional proof systems : efficiency and automatizability
Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Mathematics, 2003.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2005
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/29344 |
| _version_ | 1826198662001197056 |
|---|---|
| author | Alekhnovitch, Mikhail, 1978- |
| author2 | Madhu Sudan. |
| author_facet | Madhu Sudan. Alekhnovitch, Mikhail, 1978- |
| author_sort | Alekhnovitch, Mikhail, 1978- |
| collection | MIT |
| description | Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Mathematics, 2003. |
| first_indexed | 2024-09-23T11:08:14Z |
| format | Thesis |
| id | mit-1721.1/29344 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T11:08:14Z |
| publishDate | 2005 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/293442019-04-12T09:37:38Z Propositional proof systems : efficiency and automatizability Alekhnovitch, Mikhail, 1978- Madhu Sudan. Massachusetts Institute of Technology. Dept. of Mathematics. Massachusetts Institute of Technology. Dept. of Mathematics. Mathematics. Thesis (Ph. D.)--Massachusetts Institute of Technology, Dept. of Mathematics, 2003. Includes bibliographical references (p. 135-143). The thesis considers two fundamental questions in propositional proof complexity: lower bounds on the size of the shortest proof and automatizability of propositional proof systems. With respect to the first part, we develop a new paradigm for proving lower bounds in propositional calculus. Our method is based on the purely computational concept of pseudorandom generator. Namely, we call a pseudorandom generator Gn: [0, 1 ] - [0, 1]m hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement G (xl,...,xn) f b for any string b [0, 1]m. We consider a variety of "combinatorial" pseudorandom generators inspired by the Nisan-Wigderson generator on the one hand, and by the construction of Tseitin tautologies on the other. We prove that under certain circumstances these generators are hard for such proof systems as Resolution, Polynomial Calculus and Polynomial Calculus with Resolution (PCR). As to the second part, we prove that the problem of approximating the size of the shortest proof within factor 2log1-o(1) is NP-hard. This result is very robust in that it holds for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution, Horn resolution, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problem of approximating the length of proofs. Finally, we show that neither Resolution nor tree-like Resolution is automatizable unless the class W[P] from the hierarchy of parameterized problems is fixed-parameter tractable by randomized algorithms with one-sided error. by Mikhail Alekhnovitch. Ph.D. 2005-10-14T19:58:28Z 2005-10-14T19:58:28Z 2003 2003 Thesis http://hdl.handle.net/1721.1/29344 52760120 eng M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission. http://dspace.mit.edu/handle/1721.1/7582 143 p. 5200175 bytes 5199983 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology |
| spellingShingle | Mathematics. Alekhnovitch, Mikhail, 1978- Propositional proof systems : efficiency and automatizability |
| title | Propositional proof systems : efficiency and automatizability |
| title_full | Propositional proof systems : efficiency and automatizability |
| title_fullStr | Propositional proof systems : efficiency and automatizability |
| title_full_unstemmed | Propositional proof systems : efficiency and automatizability |
| title_short | Propositional proof systems : efficiency and automatizability |
| title_sort | propositional proof systems efficiency and automatizability |
| topic | Mathematics. |
| url | http://hdl.handle.net/1721.1/29344 |
| work_keys_str_mv | AT alekhnovitchmikhail1978 propositionalproofsystemsefficiencyandautomatizability |