Teoria della
Dimostrazione
Anno
Accademico 2005/2006
-- Prof. Nicola Galesi
Introduzione Introduzione al corso. Concetti
introduttivi su insiemi, relazioni,
grafi, funzioni.
Elementi di combinatoria e probabilità. Notazioni asintotiche.
Richiami di algebra lineare. Connettivi logici. Formule booleane,
CNF,DNF.
Richiami
di complessità computazionale.
Macchine di Turing, spazio tempo, riducibilità.
Classi di complessità, NP-completezza. TAUT, SAT. Teorema di
Cook (cenni).
Il
problema P vs NP. Funzioni booleane. Circuiti booleani, Alberi di
decisione,
Branching programs.
Logica
proposizionale.
Semantica.
Calcolo dei seguenti (LK), con e senza cut.
Teorema di eliminazione del cut.
Sistemi assiomatici. Correttezza. Completezza.
Sistemi refutazionali: Risoluzione.
Logica del
prim’ordine Predicati.
Quantificatori. Calcolo dei sequenti (PK) del prim’ordine.
Correttezza. Completezza.
Skolemizzizazione. Risoluzione del prim’ordine.
Sistemi di dimostrazione
Definizione di sistema di dimostrazione proposizionale (SDP). SDP
“limitati
polinomialmente” (SDP-LP).
Simulazione
tra SDP. Simulazione polinomiale, Equivalenza polinomiale.
Dimostrazioni ad
albero (treelike) e a grafo (daglike). Esempi concreti di SDP: Sistemi
di Frege
(sistemi assiomatici).
Complessità delle dimostrazioni. Numero
di linee, numero di simboli. Il
problema P vs NP ed
esistenza di SDP-LP: Teorema di Cook-Reckhow. Limiti
inferiori per la complessità delle dimostrazioni
come approccio al problema P
vs NP. Sistemi automatizzabili.
Formalizzazione
Limiti inferiori e superiori. Come dimostrare limiti superiori e
inferiori.
Codifica in formule booleane
di principi combinatori: principio della
Piccionaia (PHP), formule di Tseitin, principio del matching in
un grafo,
principio della clique in un grafo. Separazione di SDP. Teorema di
separazione
esponenziale di treelike cut free LK da treelike LK.
Sistemi
di Frege
Equivalenza polinomiale di Sistemi di Frege. Sistemi di Frege
potenziati:
Esteso (EF),
con Sostituzione (SF), con ridenominazione di variabili (RF), con
sostituzione
di valori di verità (TFF).
Limiti
superiori: Dimostrazioni del PHP in EF. Simulazioni: EF simula SF,
SF simula
EF, TTF simula SF, RF simula TTF. Problemi aperti: Sistemi di Frege con
permutazione
di variabili (PF), Limiti inferiori per Sistemi di Frege.
Risoluzione
Importanza della Risoluzione in Informatica. Risoluzione non
è LP
(versione Beame-Pitassi).
Sottosistemi della Risoluzione: Risoluzione
treelike, regolare. Separazione
esponenziale tra
Risoluzione treelike e daglike.
Metodo
dell’ampiezza per limiti inferiori in
Risoluzione. Ampiezza di una
clausola, Ampiezza di una refutazione in
Risoluzione. Applicazione: limiti
inferiori per formule CNF aleatorie
nella Risoluzione.
Teorema
di interpolazione di Craig per la logica
proposizionale. Il metodo
dell’interpolazione trattabile per lo studio
dei limiti inferiori in Risoluzione.Applicazione: il
principio della Clique non
ammette dimostrazioni polinomiali in Risoluzione.
Cenni sul metodo
probabilistico per dimostrazioni di esistenza.
Il
metodo probabilistico per dimostrare limiti
inferiori per la complessità di dimostrazioni.
Applicazione: la risoluzione
regolare non è LP.
Cenni
sul concetto di spazio di una refutazione e
sua relazione con l’ampiezza.
Automatizzabilità di sistemi di dimostrazione
Dimostrazione automatica e automatizzabilità. Risoluzione
treelike e
quasi-polinomialmente automatizzabile. Risoluzione daglike e debolmente
esponenzialmente automatizzabile.
Risoluzione non è automatizzabile a
meno che W[P] sia in RP
(enunciato). Interpolazione trattabile e
automatizzabilità.
Cenni
su schemi crittografici. Schema RSA. EF
non ammette interpolazione trattabile
(e non è automatizzabile) a meno di
non poter rompere lo schema RSA (Cenni). Problemi aperti.
Tra
i sistemi di Frege e Risoluzione.
Sistemi
algebraici,
Cutting Planes, Sistemi di Lovasz-Schriver.
Separazione tra treelike e daglike
CP (cenni). Oltre i sistemi di Frege: Sistemi G e G*. Problemi aperti.
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,
> 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,
>
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.
Il corso di una settimana tenuto nell'estate del 2000 da
P. Beame, presso
l'Insitute for Advanced Study di Princeton.
> P. Beame, T. Pitassi. Propositional
Proof Complexity: Past, Present and Future. Bullettin
of the EATCS 65:66-89, 98.
Un survey scritto nel
1998 da due dei maggiori esperti
mondiali in proof complexity
con una ampia panoramica sui maggiori risultati ottenuti fino al
98 e con con una
ricca lista di importanti problemi aperti da risolvere
(Nota. Non è aggiornato e alcuni problemi
sono già
stati risolti)
> S. Buss. Lectures on Proof theory .
Mc Gill University
Si tratta di un
survey con la ricompilazione delle lezioni tenute da S.
Buss durante una
scuola estiva della durata di una settimana presso la sede delle
isole Barbados della
Mc Gill University di Montreal. Sono scritte dagli "studenti"
del
corso: tra i piu esperti
ricercatori mondiali in complessità !!.
> P.
Clote, E. Kranakis. Boolean functions
and Computation Models. Springer, 2002.
Un libro recente che tratta in
maniera molto
approfondita il campo della Proof
Complexity. E' abbastanza aggiornato.
> J. Krajíček. Bounded Arithmetic, Propositional Logic
and
Complexity Theory.
solo dopo aver seguito il corso a chi avesse
desiderio di approfondirne e continuare lo studio.
> Prof. T. Pitassi:
> Prof. S. Cook. University of Toronto:
Proof
Complexity and Bounded Arithmetic (2002)
Workshop e Scuole (passate e future)
>
Una scuola
estiva annuale a Pec (Praga) organizzata J. Krajicek dell’Accademia
delle Scienze della Repubblica Ceca.
Center della Rutgers
University, New Jersey (USA).(Include materiale
online delle lezioni tenute)
> Scuola
estiva in Complessità (00) presso
(Institute
for Advanced Study)
> LAA workshop. New
Directions in Proof Complexity. Cambridge 10-13 Aprile 2006