DOCENTE | Andrea Corradini <andrea@di.unipi.it> |
Orario | Martedì 14-16, Aula A e Giovedì 11-13, Aula A |
Orario ricevimento | Cliccare qui. |
Gli orali si terranno Giovedi' 18 e Venerdi' 19 Febbraio. Coloro che non possono essere presenti, possono delegare un collega per la prenotazione. Su richiesta, e' possibile fissare l'orale in data successiva, dopo l'inizio del secondo semestre.
Coloro che non possono essere presenti, potranno iscriversi all'orale segnando il proprio nome sui fogli che verranno affissi alla porta dello studio del docente subito dopo.
Gli orali si terranno nei seguenti giorni:
N. |
DATA |
TITOLO |
RIFERIMENTI |
ARGOMENTI |
Introduzione al corso Introduzione al Calcolo Proposizionale |
Dispense: [LP1], pag 6--8
Lucidi: LPP_2015_01.pdf |
| ||
Dimostrazione di Tautologie |
Dispense: [LP1], fino a pag 10 [LMB-INF] Sezione 1.4, "Dimostrazioni per sostituzione", pag 4-7, e sezione 3.2.1, "Interpretare le formule proposizionali", pag. 32-35. Lucidi: LPP_2015_02.pdf |
| ||
Dimostrazione di Tautologie e Sintassi del Calcolo Proposizionale |
Dispense: [LP1], fino a pag 12 Lucidi: LPP_2015_03.pdf |
| ||
Esercitazione su Calcolo Proposizionale |
|
Tabella di leggi (utilizzabile durante il primo
compitino): tabelle-leggi-v1.pdf | ||
Dimostrazione di Implicazioni Tautologiche |
Dispense: [LP1], fino a pag 18 Lucidi: LPP_2015_04.pdf |
| ||
Dimostrazioni e Tautologie, Ipotesi non tautologiche |
Dispense: [LP1], fino a pag 23 Lucidi: LPP_2015_05.pdf |
| ||
Esercitazione su Calcolo Proposizionale |
|
Tabella di leggi (utilizzabile durante il primo
compitino): tabelle-leggi-v1.pdf | ||
Logica del Primo Ordine: Motivazioni, Sintassi e Interpretazioni. Formalizzazione di enunciati. |
Dispense: [LP1], Sezioni 8 e 8.1 [pag 27-31] Lucidi: LPP_2015_06.pdf |
| ||
9 |
27/10/2015 |
Logica del Primo Ordine: Semantica |
Dispense: [LP1], pag 36-38 Lucidi: LPP_2015_07.pdf |
Semantica della Logica del Primo Ordine: Assegnamenti; Semantica dei termini; Semantica di formule per induzione strutturale; Esempi.
|
10 |
Venerdì |
Esercitazione su Formalizzazione e Semantica del primo ordine |
Attenzione: causa sospensione dell'attività didattica per assemblea, l'esercitazione si terrà Venerdì 30 ottobre alle ore 9:00 in Aula A.
Tabelle con leggi del calcolo proposizionale (e semantica della Logica dei Predicati): tabelle-leggi-v1.pdf | |
11 |
5/11/2015 |
Prima prova di verifica |
Testo:
01-2015-PrimoCompitino.pdf |
Risultati: 01-2015-Risultati.pdf |
12 |
10/11/2015 |
Logica del Primo Ordine: Proof System |
Dispense: [LP1], pag 39-40 Lucidi: LPP_2015_08.pdf, fino a pag. 160. |
Modelli; Formule valide e soddisfacibili; Conseguenza logica; Sistemi di dimostrazione; Correttezza e completezza; Validità del risultato di una dimostrazione; Teorema di Deduzione; Leggi per quantificatori.
|
13 |
12/11/2015 |
Logica del Primo Ordine: Proof System (2) |
Dispense: [LP1], pag 49-51 Lucidi: LPP_2015_08.pdf, tutti. |
Leggi valide solo su dominio non vuoto; Quantificazione su dominio vuoto: discussione; Predicato di uguaglianza; Leggi per l'uguaglianza. Regole di inferenza: Generalizzazione e Skolemizzazione; Esempi di dimostrazione.
|
14 |
17/11/2015 |
Notazione e leggi per insiemi, intervalli e domini |
Dispense: [LP2], pag 1-9. Lucidi: LPP_2015_09.pdf, tutti. |
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.
|
15 |
19/11/2015 |
Quantificatori funzionali |
Dispense: [LP2], fino a pag. 30. Lucidi: LPP_2015_10.pdf. |
Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo; Leggi per quantificatori funzionali; leggi dell'intervallo; Formalizzazione di enunciati. |
Esercitazione su Dimostrazioni di Validità e Formalizzazione di Enunciati. |
|
Tabella di leggi (utilizzabile durante il secondo
compitino): tabelle-leggi-v3.pdf | ||
17 |
26/11/2015 |
Logica di Hoare: Introduzione |
Dispense: [LdH], fino a pag 20. Lucidi: LPP_2015_11.pdf. |
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. |
18 |
01/12/2015 |
Triple di Hoare: Regole di inferenza per assegnamento, sequenza e comando condizionale. |
Dispense: [LdH], fino a pag 23. Lucidi: LPP_2015_12.pdf. |
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. Regola per comando condizionale; Esempi di verifica di Triple di Hoare. |
19 |
03/12/2015 |
Esercitazione su Triple di Hoare |
Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf | |
20 |
09/12/2015 |
Triple di Hoare: |
Dispense: [LdH], fino a pag 27. Lucidi: LPP_2015_13.pdf. |
Triple di Hoare: Regola per il Comando Iterativo; Esempi. |
21 |
10/12/2014 |
Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo |
Dispense: [LdH], fino a pag 30. Lucidi: LPP_2015_14.pdf. |
Sequenze: sintassi e semantica; Assioma e regola per aggiornamento selettivo; Esercizi su verifica di triple di Hoare. |
22 |
15/12/2015 |
Esercitazione su Triple di Hoare |
|
|
23 |
17/12/2014 |
Seconda prova di verifica |
Testo:
02-2015-SecondoCompitino.pdf |
Iscrizione obbligatoria alla pagina https://esami.unipi.it/esami2/
Per la prova di verifica non si possono portare né dispense né appunti. Si potrà usare solo il foglio tabelle-leggi-v3.pdf che riassume le leggi necessarie. |
|
|
| ||
|
|
|