Proof Theory

2009/2010 -- Nicola Galesi

Orari (!!!)

Il corso ha cambiato is suoi orari come segue

Giovedi 8:30—10:15 Aula Seminari (Dip Informatica, III piano, Via Salaria 113)

Venerdi 13:15 – 15:00 Aula Seminari

Email docente: lastname{ATA}di.uniroma1.it

Ricevimento: appuntamento per email

Abstract corso

Dopo un ‘introduzione ai concetti fondanti della Proof Complexity, si approfondirà lo studio della

risoluzione e della complessita delle refutazioni in questo calcolo per familiarizzare e apprendere

tecniche di dimostrazioni proprie del campo.

Infine si prendereanno in considerazione sistemi piu potenti e importanti problemi di frontiera della Proof Complexity

e della Complessita Computazionale.

Il corso si sarà organizzato come un laboratorio di ricerca dove studenti in gruppo e docente imparano insieme a ragionare v

E a risolvere probelmi via via più complessi.

Lezioni

Tu 29 Set – Intro + Esempi di dimostrazioni

Th 1 Ott – P, NP, Co-NP + def Sistema di dimostrazione [Lucidi] + Frege Systems

Nuovo Orario e Aule

Th 8 Ott -- Resolution I

Fr 10 Ott – Resolution II [Lucidi]

Th 15 Oct – Exponential Separation between TLR and DLR I

Fr 16 Oct -- Exponential Separation between TLR and DLR II

Th 22 Oct -- Exponential Separation between TLR and DLR III [Lucidi]

References:

E. Ben-Sasson,R.Impagliazzo, A. Wigderson

Near-Optimal Separation of General and Tree-Like Resolution.

Combinatorica, Vol 24, Issue 4, pp 585-604, 2004

Fr 23 Oct -- Beame-Pitassi simplified method for DLR lower bounds [Lucidi]

References:

[1] P.Beame, T. Pitassi. Simplified and Improved Resolution lower bounds.

IEEE FOCS 1999

Th 29+Fr 30 Homeworks [discussion and presentation 13-14 nov]

Testi, Bibliografia, Materiale Didattico.



Logica Matematica (per Informatici)


>  A.Asperti, A. Ciabattoni. Logica a Informatica. Mc Graw Hill


> J. Gallier. Logic for Computer Science. Harper & Row [online] 


> A. Nerode, R. Shore. Logic for Applications.  II Edizione. Springer.


> U. Schoning, Logic for Computer Scientists. Birkhauser

Logica Matematica

> J. Bell, M. Machover. A Course in Mathematical Logic, North Holland, 1977.
 

> C. Chang, H. Keisler. Model theory, North Holland, 1973.

Complessità


> C. Papadimitriou. Computational Complexity. Addison Wesley, 1994


> M. Sipser.  Introduction to Theory of Computation. PWS publishing 1996.
 

Complessità delle dimostrazioni


Si fornirà una lista completa delle referenze esatte da cui i risultati presentati sono tratti.  
I seguenti testi e surveys sono fondamentali per un approfondimento
della  Proof Complexity (alcuni sono disponibli online).

> P. Beame.  Proof Complexity. IAS Summer  School. (lecture Notes)
 

> P. Beame, T. Pitassi. Propositional Proof Complexity: Past, Present and Future.(Survey) 

> S. Buss. Lectures on Proof theory .  Mc Gill University
   (Lecture Notes)

> P. Clote,  E. Kranakis. Boolean functions and Computation Models. (book) Springer 2004

> J. Krajíček. Bounded Arithmetic, Propositional Logic and Complexity Theory. 
 Cambridge University Press, 1999. (book)

> J. Krajicek. Propositional Proof Complexity. Lecture Notes(2007)

> N. Segerlind.

> P. Pudlak Twelve open problems in Proof Complexity (paper)




Corsi simili in altre Università


> T. Pitassi: University of Toronto: Propositional Proof Complexity  (2002)


> S. Cook. University of Toronto: Proof Complexity and Bounded Arithmetic (2002)
 

> A. Razborov. University of Chicago. Proof Complexity (con una lista di problemi aperti da risolvere)

> N. Galesi. (2006) Teoria della dimostrazione (Un corso meno centrato sulla risoluzione)

.

Workshop e Scuole (passate e future)


>  Una scuola estiva annuale a Praga J. Krajicek.

> NoNa Summer School on Computational Complexity (2009 St Petersburg).

> Barriers on Computational Complexity. (2009 Princeton University).


>  Special Year on Logic and Algorithms (96 DIMACS Rutgers University)


>  Scuola estiva in Complessità (00) (Institute for Advanced Study, Princeton))

>  New Directions in Proof Complexity. Cambridge 10-13 Aprile 2006