Propositional Proof Complexity
St.
Petersburg, 29.3 - 7.4. 2009
Within the scope of the "Joint Advanced Student School
- JASS'2009" in St. Petersburg (March 29 - April 7), we offer the course "Propositional Proof Complexity".
Directors:
Prof. Dr. E. Hirsch (Steklov
Institute, St. Petersburg)
Prof. Dr. E. W.
Mayr (TU München)
Assistants:
D. Chibisov
D. Itsykson
Application:
The course addresses highly motivated and interested students. Active preparation
and contribution of the participants will be required. The course language
is English. Expenses for travel, board and lodging of german participants
are covered by the school.
Application deadline for GERMAN applicants: February 10, 2009 (extended).
Application form: PDF
.
German applicants should send their applications
to D. Chibisov.
Russian
applicants should send their applications to Prof. Dr. E. Hirsch
Course Description:
Proof complexity
studies the length of proofs in propositional logic and is
closely related to open questions in the computational complexity
theory as well as to practical applications of automated theorem
proving. The course is devoted, besides the
fundamentals of proof theory,
to complexity theoretic considerations of different proof calculi (like
resolution, cutting planes, and algebraic proofs). Additionally,
the connections between proof complexity and communication complexity
will be considered as well as applications of proof complexity in
areas like pseudorandom number generators or crpytography will be
discussed.
Organization:
Every participant is expected to give a talk and
to prepare a paper on the topic of his/her talk. Some help is provided on
the organizational stuff page
Stefan Kunkel
Introduction: P, NP, coNP, NP-completeness,
propositional proof systems, simulations and separations. Examples:
Frege, resolution, Nullstellensatz, polynomial calculus.
Literature:
[Bu,AB/Pap,Pu1,Pu2]
|
|
|
Michael Herrmann
Equivalence of Frege systems; treelike Frege systems;
Gentzen calculus.Extended Frege, equivalence to extended resolution. Upper bound for PHP in Extended Frege and Frege.
Literature: [Bu]
|
|
Maximilian Schlund, Mykola Protsenko
Width-based lower bounds for resolution and polynomial
calculus: PHP, Tseytin formulas.
Literature: [BSW,BIKP,CEI]
|
|
|
Alisa Knizel
Razborov's theorem, interpolation method,
and lower bounds for Resolution and Cutting Planes.
Literature:[Pap, Pu3, AB]
|
|
|
Sergey Nurk
Lower bounds for Res-k.
Literature: [A, ABE, AB2]
|
|
Alexander Glazman
Switching lemma.
Literature: ...
|
|
Ivan Monakhov
Lower bounds for bounded depth Frege
systems.
Literature:[BS, BSH]
|
|
|
Tobias Lieber
Automatisation (Grobner bases and width-based) and non-automatisability.
Literature: [BSW,AR,CEI,AB2]
|
|
Dmitry Antipov
Optimal proof systems and disjoint NP
pairs.
Literature: ...
|
|
Markus Latte
Pseudorandom generators hard for propositional proof
systems.
Literature: [ABR,Raz]
|
|
Grigory Yaroslavtsev
Lower bounds using communication
complexity.
Literature: [BP, ... ]
|
|
Literature:
[A] Alekhnovich, M.: Lower
bounds for k-DNF resolution on random 3-CNFs. In: STOC'05: Proceedings
of the thirty-seventh annual ACM symposium on
Theory of computing, New York, NY, USA, ACM Press (2005) 251-256
[AB] S. Arora and B. Barak [draft of their new book]
Atserias, A., Bonet, M.L., Esteban, J.L.: Lower bounds for the weak
pigeonhole principle and random formulas beyond resolution. Information
and Computation 176(2) (2002) 136-152
[AB2] A. Atserias and M. L. Bonet. On the Automatizability of
Resolution and Related Propositional Proof Systems, Information and
Computation, 189(2), pages 182-201, 2004.
[ABE] Atserias, A., Bonet, M.L., Esteban, J.L.: Lower bounds for the
weak pigeonhole principle and random formulas beyond resolution.
Information and Computation 176(2) (2002) 136-152
[ABR] M. Alekhnovich, E. Ben-Sasson, A. Razborov. Pseudorandom Generators In Propositional Proof Complexity. FOCS-2000.
[AR] M. Alekhnovich, A.A. Razborov. Resolution is not automatizable
unless W[P] is not tractable. Proceedings of the 42nd IEEE Symposium on
Foundations of Computer Science.
[BIKP] P. Beame, R. Impagliazzo, J. Krajicek, T. Pitassi, Lower bounds
on Hilbert's Nullstellensatz and propositional proofs. Foundations of
Computer Science, 1994.
[BS] E. Ben-Sasson. Hard Examples for Bounded Depth Frege Proceedings
of the 34th Annual {ACM} Symposium on Theory of Computing, STOC02,
563--572, 2002.
[BSH] E. Ben-Sasson, P. Harsha. Lower Bounds for Bounded Depth Frege Proofs via Buss-Pudlak Games ECCC Report TR03-004, 2003.
[BSW] E. Ben-Sasson and A. Wigderson. Short proofs are narrow - Resolution made simple. Journal of ACM, 48(2):149-169, 2001.
[Bu] S. Buss. An Introduction to Proof Theory.In Handbook of Proof Theory, Elsevier, 1--78, 1998.
*or*
Propositional Proof Complexity: An Introduction. NATO Summer School, Marktoberdorf, Germany, 1997.
ftp://euclid.ucsd.edu/pub/sbuss/research/marktoberdorf97.ps
[CEI] M. Clegg, J. Edmonds, R. Impagliazzo. Using the Groebner basis
algorithm to find proofs of unsatisfiability. STOC 96, 174-183.
[Pap] C. Papadimitriou, Computational Complexity, Addison-Wesley, 1994.
[Pu1] P. Pudlak [draft of his new book]
[Pu2] P. Pudlak. On the complexity of the propositional calculus. Sets
and Proofs: Invited papers from Logic Colloquium'97, Cambridge
University Press, 197--218, 1999
[Pu3] P. Pudlak. Lower bounds for resolution and cutting plane proofs
and monotone computations. Journal of Symbolic Logic, 62(3):981-998,
1997.
[Raz] A. Razborov. Pseudorandom Generators hard for k-DNF Resolution
and Polynomial Calculus. Manuscript. Availalble at the Author's web
page, 2003
[SBI] N. Segerlind, S. Buss, R. Impagliazzo: A Switching Lemma for
Small Restrictions and Lower Bounds for k-DNF Resolution. SIAM
Journal on Computing 33(5) (2004) 1171-1200