Terminplanung

• Abgabe der Ausarbeitung vor Weihnachten (nach vorheriger Tehmenabsprache, spätestens Anfang Dezember!)
• Vorträge am Sa. 18. Januar 2003.

Themen

Als Einführung eignet sich [Bus96, Kapitel 1], einen Überblick bietet [CK02, Kapitel 5].

1. Resolution (TSP)
   • Untere Schranken für reguläre baumartige Resolution, [Gal77].

     Vortragender: Andreas Pitschi, andreas.pitschi @ informatik.uni-ulm.de.
     Ausarbeitung: Teil 1.doc, Teil 2.doc.

   • Untere Schranke für allgemeine Resolution (PHP), [Hak85,BP96,BW01].

     Vortragende(r): Franz Kiraly, franz.kiraly @ informatik.uni-ulm.de
     Ausarbeitung.pdf

   • Trennung zwischen baumartiger und allgemeiner Resolution. [BIW00]

     Kein Vortrag.



2. Cutting Planes
   • Simulation von Resolution und Trennung, [CCT87].

     Vortragender: Florian Pitschi, florian.pitschi @ informatik.uni-ulm.de .
     Ausarbeitung:Titelblatt.doc, Ausarbeitung.doc

   • Untere Schranken, [Pud97,HC99].

     Vortragender: Matthias Raab, matthias.raab @ informatik.uni-ulm.de .
     Ausarbeitung.pdf

   • Trennung zu baumartigen Cutting Planes. [BEG97]

     Vortragender: Frank Förster, frank.foerster @ informatik.uni-ulm.de.
     Ausarbeitung.pdf



3. Frege Systeme
   • Gegenseitige Simulation verschiedener Systeme, [CR79].

     Vortragender: Christian Hummert, christian.hummert @ informatik.uni-ulm.de.

   • Untere Schranken für Systeme mit beschränkter Tiefe, [UF96].

     Kein Vortrag.

   • Automatisierbarkeit, [BPR00],

     Vortragender Bernd Ruoss, bernd.ruoss @ informatik.uni-ulm.de.

Literatur

BP96

Paul Beame, Toniann Pitassi: Simplified and Improved Resolution Lower Bounds. FOCS 1996: 274-282.

BIW00

Eli Ben-Sasson, Russell Impagliazzo, Avi Wigderson: Near-Optimal Separation of Treelike and General Resolution. Electronic Colloquium on Computational Complexity (ECCC) 7(5): (2000).

BW01

Eli Ben-Sasson, Avi Wigderson: Short proofs are narrow - resolution made simple. JACM 48(2): 149-169 (2001)

BEG97

María Luisa Bonet, Juan Luis Esteban, Nicola Galesi, Jan Johansen. Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems. 39th IEEE Symposium on Foundations of Computer Science, FOCS'98, pp 638-647.

BPR00

María Luisa Bonet, Toniann Pitassi, and Ran Raz. On Interpolation and Automatization for Frege Systems.
SIAM J. Comput. 29(6), 1939-1967, 2000.

Bus96

Samuel R. Buss. Lectures on Proof Theory. Technical Report SOCS-96.1 School of Computer Sience McGill University. http://www.math.ucsd.edu/ sbuss/ResearchWeb/Barbados95Notes/

CK02

Peter Clote and Evangelos Kranakis. Boolean Functions and Computation Models. Springer-Verlag, 2002.

CR79

S. A. Cook and R. A. Reckhow.
The relative efficiency of propositional proof systems.
The Journal of Symbolic Logic, 44(1):36-50, 1979.

CCT87

Cook, W., Coullard, C.R., and Turán, G. (1987)
On the complexity of cutting plane proofs.
Discrete Applied Mathematics, 18:25-38.

Gal77

Zvi Galil: On the Complexity of Regular Resolution and the Davis-Putnam Procedure. TCS 4(1): 23-46 (1977)

Hak85

Armin Haken: The Intractability of Resolution. TCS 39: 297-308 (1985)

HC99

Armin Haken, Stephen A. Cook: An Exponential Lower Bound for the Size of Monotone Real Circuits. JCSS 58(2): 326-335 (1999)

Pud97

Pudlak, P.
Lower bounds for resolution and cutting planes proofs and monotone computations,
J. of Symb. Logic 62(3), 1997, pp.981-998.

UF96

Alasdair Urquhart, Xudong Fu: Simplified Lower Bounds for Propositional Proofs. Notre Dame Journal of Formal Logic 37(4): 523-544 (1996)