| + + | ++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: |
+
+
+ + + + |
+
Elementi di teoria degli insiemi |
Letture consigliate:
+
|