DOCENTE | Andrea Corradini <andrea@di.unipi.it> |
Orario | Martedì 9-11, Aula A e Giovedì 9-11, Aula A |
Orario ricevimento | Cliccare qui |
N. |
DATA |
TITOLO |
RIFERIMENTI |
ARGOMENTI |
1 |
20/09/2011 |
Introduzione al corso
|
Lucidi: Logica_2010_1.pdf. Logica_2010_2.pdf, fino a pag. 13. Esercizi: Esercizi proposti a lezione |
Introduzione al corso: La logica da Aristotele alla logica matematica; Logica e informatica; Contenuto del corso.
|
2 |
22/09/2011 |
Calcolo Proposizionale |
Dispense: [LP1], fino a pag 10 |
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 |
3 |
27/09/2011 |
Dimostrazioni di Implicazioni Tautologiche |
Dispense: [LP1], fino a pag 16
|
Insiemi Funzionalmente Completi di Connettivi Logici |
4 |
4/10/2011 |
Forme normali |
Dispense: [LP1], fino a pag 18
|
Forma normale congiuntiva e disgiuntiva; Il Principio di Risoluzione. |
5 |
6/10/2011 |
Dimostrazioni con Ipotesi non Tautologiche |
Dispense: [LP1], fino a pag 24, Sezione 7 esclusa
|
Formalizzazione di dimostrazioni: tautologie corrispondenti a uno o più passi di dimostrazione; Uso di ipotesi come giustificazione; Esempi vari; Altre tecniche di dimostrazione: esempi di dimostrazione per assurdo e per casi. |
6 |
11/10/2011 |
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. |
7 |
13/10/2011 |
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. |
8 |
18/10/2011 |
Esercitazione |
Dispense: [LP1], Sezione 8.2 [pag. 32-33]
|
Svolgimento di alcuni esercizi su formalizzazione di enunciati con la logica del primo ordine. |
9 |
20/10/2011 |
Il Calcolo del Primo Ordine |
Dispense: [LP1]: pag 39-48 |
Sistemi di dimostrazione; Correttezza e completezza; Validità del risultato di una dimostrazione; Teorema di Deduzione; Leggi per quantificatori. |
10 |
25/10/2011 |
Il Calcolo del Primo Ordine |
Dispense: [LP1], pag. 48-51 |
Ancora leggi per quantificatori; Predicato di uguaglianza; Leggi per l'uguaglianza; Regole di inferenza: Generalizzazione e Skolemizzazione. Esercizi vari. |
11 |
27/10/2011 |
Esercitazione |
Esercizi della Lezione 8 |
Esercizi su dimistrazioni e formalizzazione con logica del prim'ordine. |
12 |
4/11/2011 |
Primo compitino |
Ore 14:00, Aule A, B, C. |
Iscrizione obbligatoria alla URL http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/appelliret.asp?start=10&end=10&chk=3553 |
13 |
8/11/2011 |
Notazione e leggi per insiemi, intervalli e domini |
Lucidi: Logica_2010_9.pdf,
Dispense: [LP2], pag 1-7.
|
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. |
14 |
10/11/2011 |
Leggi di intervallo, Quantificatori funzionali, Formalizzazione di enunciati |
Lucidi: |
Leggi dell'intervallo per quantificatori; Definizione di array; Formalizzazione di enunciati su array; Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo. |
15 |
15/11/2011 |
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. |
16 |
17/11/2011 |
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. |
17 |
22/11/2011 |
Triple di Hoare: definizioni e regole di inferenza |
Lucidi: |
Interpretazione di triple di Hoare: semantica, correttezza, specifica. 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. |
18 |
24/11/2011 |
Triple di Hoare:
|
Lucidi: |
Triple di Hoare: Assioma e Regola per l'Assegnamento, Regola della Sequenza, Regola per comando condizionale; Esempi di verifica di Triple di Hoare. |
19 |
29/11/2011 |
Triple di Hoare:
|
Lucidi:
|
Triple di Hoare: Regola per il Comando Iterativo; Esempi. |
-- |
29/11/2011 |
Esercitazione straordinaria |
Aula B, ore 14:15-16:00
|
Visione correzioni primo compititno del 4/11/2011; esercitazione di ripasso su Calcolo Proposizionale e Logica del Prim'Ordine |
20 |
1/12/2011 |
Triple di Hoare |
Lucidi: |
Triple di Hoare: Variabili di Specifica, Programmi annotati, Esempi di verifica di triple con Regola per il Comando Iterativo. |
21 |
6/12/2011 |
Triple di Hoare |
Lucidi: |
Ricapitolazione su Sequenze: sintassi, semantica e regola per aggiornamento selettivo. |
22 |
13/12/2011 |
Esercizi di ricapitolazione |
Lucidi: |
Esercizi ed esempi su Triple di Hoare, formalizzazione di enunciati. |
23 |
15/12/2011 |
Esercitazione |
Testo esercizi: |
|
-- |
19/12/2011 |
Secondo compitino |
Ore 16, Aule A, B, C |
Iscrizione obbligatoria alla URL http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/appelliret.asp?start=20&end=20&chk=3553&chk=3554 |