DOCENTE | Andrea Corradini <andrea@di.unipi.it> |
Orario | Martedì 14-16, Aula A e Giovedì 11-13, Aula A |
Orario ricevimento | Cliccare qui |
N. |
DATA |
TITOLO |
RIFERIMENTI |
ARGOMENTI |
1 |
25/09/2012 |
Introduzione al corso |
Lucidi: Logica_2010_1.pdf |
NB: lezione tenuta dalla Prof. F. Levi |
2 |
27/09/2012 |
Introduzione al Calcolo Proposizionale |
Lucidi: Logica_2010_2.pdf |
NB: lezione tenuta dalla Prof. F. Levi |
3 |
2/10/2012 |
Dimostrazione di Tautologie |
Dispense: [LP1], fino a pag 12
|
Formalizzazione di Enunciati Dichiarativi; Dimostrazioni di equivalenze; Principio di Sostituzione; Concetto di Legge del Calcolo Proposizionale; Leggi per Equivalenza, Congiunzione, Disgiunzione, Negazione, Implicazione;
Esempi di dimostrazioni; Leggi di Assorbimento e Complemento;
Insiemi Funzionalmente Completi di Connettivi Logici |
4 |
4/10/2012 |
Dimostrazione di Implicazioni Tautologiche, |
Dispense: [LP1], fino a pag 18
|
Ambiguità della sintassi del Calcolo Proposizionale; Precedenza tra i connettivi logici; Dimostrazioni di implicazioni; Occorrenze positive e negative; Principio di Sostituzione per l'Implicazione; Altre tecniche di dimostrazione; Forma normale congiuntiva e disgiuntiva; Il Principio di Risoluzione. |
5 |
9/10/2012 |
Esercitazione |
Esercizi proposti: Esercitazione_2012_1.pdf |
Svolgimento e correzione corale di alcuni esercizi su formalizzazione di enunciati, occorrenze positive e negative, dimostrazione di tautologie. |
6 |
11/10/2012 |
Dimostrazioni con Ipotesi non Tautologiche |
Dispense: [LP1], fino a pag 24, Sezione 7 esclusa
|
|
7 |
16/10/2012 |
Logica del Primo Ordine: Motivazioni, Sintassi e Interpretazioni |
Dispense: [LP1], Sezioni 8 e 8.1 [pag 27-31], 9 e 9.1 [pag 33-35]
|
Limiti del Calcolo Proposizionale; Sintassi della Logica del Primo Ordine: Alfabeto, Grammatica, Termini, Formule; Occorrenze legate e libere di varaibili; Formule aperte e chiuse; Interpretazione di un linguaggio del primo ordine; Esempi di interpretazioni; Formalizzazione di enunciati: linee guida ed esempi. |
8 |
18/10/2012 |
Semantica della logica del prim'ordine |
Dispense: [LP1], pag 36-39
|
Semantica del Calcolo del Primo Ordine: Semantica di termini chiusi e aperti; Assegnamenti; Semantica di formule per induzione strutturale; Esempi; Modelli; Formule valide, soddisfacibili, insoddisfacibili; Conseguenza logica. |
9 |
23/10/2012 |
Il Calcolo del Primo Ordine |
Dispense: [LP1]: pag 39-49 |
Sistemi di dimostrazione; Correttezza e completezza; Validità del risultato di una dimostrazione; Teorema di Deduzione; Leggi per quantificatori; Predicato di uguaglianza; Leggi per l'uguaglianza. |
10 |
25/10/2012 |
Regole di Inferenza per Quantificatori |
Dispense: [LP1] pag. 49-51 + Sezione 8.2 [pag. 32-33]
|
Regole di inferenza: Generalizzazione e Skolemizzazione. Svolgimento di alcuni esercizi su formalizzazione di enunciati con la logica del primo ordine. |
11 |
30/10/2012 |
Esercitazione |
|
Esercizi su dimostrazioni e formalizzazione con logica del prim'ordine. |
12 |
7/11/2012 |
Primo compitino |
Testo: 01-2012-PrimoCompitino.pdf. |
Testo con soluzioni: 01-2012-PrimoCompitino-SOL.pdf.
|
13 |
8/11/2012 |
Notazione e leggi per insiemi, intervalli e domini |
Lucidi: Logica_2010_9.pdf,
Dispense: [LP2], pag 1-9.
|
Estensioni del linguaggio del primo ordine: Notazione intensionale per insiemi, Predicato di Appartenenza, Insieme vuoto; Relazioni di ordinamento su naturali: definizioni e leggi; Definizioni e notazione per intervalli; Quantificazione ristretta a un insieme: domini, quantificazione su domini vuoti, estensione di leggi per quantificatori a domini; Leggi dell'intervallo per quantificatori; Definizione di array; Formalizzazione di enunciati su array. |
14 |
13/11/2012 |
Quantificatori funzionali |
Lucidi: |
Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo; Formalizzazione di enunciati; Leggi Generali e Leggi Specifiche per Quantificatori Funzionali. |
15 |
15/11/2012 |
Formalizzazione di enunciati e leggi per quantificatori funzionali |
Lucidi: |
Quantificatori funzionali: formalizzazione di enunciati, leggi generali e leggi specifiche, leggi dell'intervallo; Esempi di dimostrazione. Formalizzazione di proprietà di relazioni binarie: univalenza, totalià, iniettività, surgettività (si veda pag. 3 di Esercitazione_2010_2_SOL.pdf). |
16 |
20/11/2012 |
Logica di Hoare: Introduzione |
Lucidi: |
Linguaggio imperativo minimo: sintassi con grammatica BNF; stato di un programma; semantica delle espressioni; significato informale dei comandi. Asserzioni; soddisfazione di un'asserzione in uno stato. Definizione di Triple di Hoare: definizione di tripla soddisfatta. Interpretazione di triple di Hoare: semantica, correttezza, specifica. Regole di inferenza: pre e post. |
17 |
22/11/2012 |
Triple di Hoare: Regole di inferenza per assegnamento e sequenza. |
Lucidi: |
Triple di Hoare: Regole di inferenza, pre e post. Assiomi per skip, assegnamento semplice e assegnamento multiplo. Espressioni definite e non. Regole per assegnamento e per sequenza di comandi. Variabili di specifica. Esempi di verifica di triple. |
18 |
27/11/2012 |
Triple di Hoare:
|
Lucidi: |
Triple di Hoare: Regola per comando condizionale; Esempi di verifica di Triple di Hoare. |
19 |
29/11/2012 |
Triple di Hoare:
|
Lucidi:
|
Triple di Hoare: Regola per il Comando Iterativo; Esempi. |
20 |
4/12/2012 |
Esercitazione |
|
Esercizi su Triple di Hoare. |
21 |
6/12/2012 |
Triple di Hoare: |
Lucidi:
Logica_2012_15.pdf. Dispense: [LdH]: fino a pag 30 |
Regola per aggiornamento selettivo; Esercizi su verifica di triple di Hoare. |
22 |
11/12/2012 |
Esempi ed esercizi su Triple di Hoare |
Lucidi:
|
Esempi di verifica di Triple di Hoare; Programmi annotati; Semplice esempio di determinazione dell'invariante; Esempi di specifica di programmi. |
23 |
13/12/2012 |
Esempi ed esercizi su Triple di Hoare |
Lucidi:
|
Esempi di specifica di programmi usando Triple di Hoare; Formalizzazione di enunciati su sequenze. |
24 |
18/12/2012 |
Esercitazione |
|
|
25 |
21/12/2012 |
Secondo compitino |
Ore 14 - Aule A, B |
Iscrizione obbligatoria alla URL http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/appelli.asp?letter=&ycourse=&course=inf31&year=2013&start=20&end=20 |