Corso A | Corso B | |
DOCENTI | Andrea Corradini <andrea@di.unipi.it> | Paolo Mancarella <paolo@di.unipi.it> |
Orario | Martedì 9-11, Aula A e Giovedì 9-11, Aula A | Martedì 9-11, Aula B e Giovedì 9-11, Aula B |
Orario ricevimento | Cliccare qui | Cliccare qui |
N. |
DATA |
TITOLO |
RIFERIMENTI |
ARGOMENTI |
1 |
19/10/2010 |
Protesta dell'Università
|
Materiale informativo su Università e sulla protesta a Pisa: https://sites.google.com/site/protestaunipi/home |
Introduzione al corso: La logica da Aristotele alla logica matematica; Logica e informatica; Contenuto del corso. |
2 |
21/10/2010 |
Calcolo Proposizionale |
Lucidi: Logica_2010_2.pdf
|
Introduzione al Calcolo Proposizionale: Connettivi logici; Sintassi del Calcolo Proposizionale; Semantica dei connettivi logici con Tabelle di Verità; Formalizzazione di enunciati dichiarativi; Tautologie e Contraddizioni. |
3 |
26/10/2010 |
Dimostrazioni di Tautologie |
Dispense: [LP1], fino a pag 11, escluso Modus Ponens |
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 |
28/10/2010 |
Dimostrazioni 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 |
2/11/2010 |
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 |
4/11/2010 |
Esercitazione |
Esercizi proposti: Eserciztazione_2010_1.pdf |
Svolgimento di alcuni esercizi su formalizzazione di enunciati, occorrenze positive e negative, dimostrazione di tautologie. |
7 |
8/11/2010 |
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 |
11/11/2010 |
Esercitazione |
Dispense: [LP1], Sezione 8.2 [pag 32-33] Esercizi proposti: Esercitazione_2010_2.pdf |
Svolgimento di alcuni esercizi su formalizzazione di enunciati con la logica del primo ordine. |
9 |
16/11/2010 |
Corsi A e B: |
Corsi A e B: Lucidi: Logica_2010_7.pdf
|
Corsi A e B: 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.
|
10 |
18/11/2010 |
Il Calcolo del Primo Ordine |
Lucidi: Logica_2010_8.pdf [fino a lucido 19]
|
Sistemi di dimostrazione; Correttezza e completezza; Validità del risultato di una dimostrazione; Teorema di Deduzione; Leggi per quantificatori.
|
11 |
23/11/2010 |
Il Calcolo del Primo Ordine |
Lucidi: Logica_2010_8.pdf, tutto.
|
Predicato di uguaglianza; Leggi per l'uguaglianza; Regole di inferenza per quantificatori: Generalizzazione e Skolemizzazione. Esercizi vari. |
|
25/11/2010 |
|
Lezione annullata causa occupazione |
|
12 |
2/12/2010 |
Notazione e leggi per insiemi, intervalli e domini |
Lucidi: Logica_2010_9.pdf, fino a pag 15.
|
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. |
13 |
7/12/2010 |
Primo compitino |
Testo con soluzioni: 01-2010-PrimoCompitino-Soluzioni.pdf. |
|
14 |
9/12/2010 |
Leggi di intervallo, Quantificatori funzionali |
Lucidi: Logica_2010_9.pdf, tutto. |
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 |
14/12/2010 |
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 |
16/12/2010 |
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 |
21/12/2010 |
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. Solo corso B: Regola per comando condizionale. |
18 |
11/01/2011 |
Triple di Hoare: regole di inferenza ed esempi |
Lucidi: |
Regole di inferenza per le Triple di Hoare, compreso Regola per il Condizionale e Regola per il Comando Iterativo; Esempi di verifica di Triple di Hoare. |
19 |
13/01/2011 |
Triple di Hoare: Comando condizionale, Sequenze |
Lucidi: |
Esempi di verifica di Triple di Hoare, in particolare di Comandi Iterativi; [Corso A] Sequenze: sintassi, semantica e regola per aggiornamento selettivo. Programmi annotati. |
20 |
18/01/2011 |
Triple di Hoare: Comando condizionale, Sequenze |
Lucidi: |
Ricapitolazione su Sequenze: sintassi, semantica e regola per aggiornamento selettivo. Programmi annotati. Esempi di programmi annotati e di dimostrazione di poprietà di invarianza. |
21 |
20/01/2011 |
Esercizi su Triple di Hoare e su formalizzazione |
Lucidi: |
Esercizi ed esempi su Triple di Hoare: numero di elementi positivi di una sequenza, incremento di una sequenza, fattoriale, MCD. Esercizi di formalizzazione con sequenze. |
22 |
25/01/2011 |
Esercizi di ricapitolazione |
Lucidi: |
Esercizi ed esempi su Triple di Hoare, formalizzazione di enunciati, dimostrazioni del primo ordine. |
23 |
27/01/2011 |
Esercitazione per secondo compitino |
Testo esercizi: |
|