DOCENTE | Andrea Corradini <andrea@di.unipi.it> |
Orario | Martedì 14-16, Aula A e Giovedì 11-13, Aula A |
Orario ricevimento | Mercoledì 15-18, Studio 357, Dipartimento di Informatica |
N. |
DATA |
TITOLO |
RIFERIMENTI |
ARGOMENTI |
Introduzione al corso Introduzione al Calcolo Proposizionale |
Dispense: [LP1], pag 6--8
Lucidi: LPP_2016_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_2016_02.pdf |
| ||
Dimostrazione di Tautologie e Sintassi del Calcolo Proposizionale |
Dispense: [LP1], fino a pag 12 Lucidi: LPP_2016_03.pdf |
| ||
Dimostrazione di Implicazioni Tautologiche |
Dispense: [LP1], fino a pag 18 Lucidi: LPP_2016_04.pdf |
| ||
Esercitazione su Calcolo Proposizionale |
|
Tabella di leggi (utilizzabile durante il primo
compitino): tabelle-leggi-v1.pdf | ||
Dimostrazioni e Tautologie, Ipotesi non tautologiche |
Dispense: [LP1], fino a pag 23 Lucidi: LPP_2016_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. |
Dispense: [LP1], Sezioni 8 e 8.1 [pag 27-31] Lucidi: LPP_2016_06.pdf, fino a pag. 112. |
| ||
9 |
18/10/2016 |
Logica del Primo Ordine: Formalizzazione e Semantica |
Dispense: [LP1], pag 36-38 Lucidi: LPP_2016_07.pdf fino a pag. 132. |
|
10 |
20/10/2016 |
Logica del Primo Ordine: Semantica |
Dispense: [LP1], pag 36-38 Lucidi: LPP_2016_07.pdf, tutte |
|
11 |
25/10/2016 |
Esercitazione su Formalizzazione e Semantica del primo ordine |
Tabelle con leggi del calcolo proposizionale (e semantica della Logica dei Predicati): tabelle-leggi-v1.pdf | |
12 |
27/10/2016 |
Logica del Primo Ordine: Proof System |
Dispense: [LP1], pag 39-46 Lucidi: LPP_2016_08.pdf |
|
-- |
3/11/2016 |
Prima prova di verifica |
Testo:
01-2016-PrimoCompitino.pdf Soluzioni: 01-2016-PrimoCompitinoSol.pdf
| |
13 |
8/11/2016 |
Logica del Primo Ordine: Proof System (2) |
Dispense: [LP1], pag 47-51 Lucidi: LPP_2016_09.pdf |
|
14 |
10/11/2016 |
Leggi per quantificazione su dominio |
Dispense: [LP1], pag 47-51 Lucidi: LPP_2016_09.pdf |
|
Esercitazione su Dimostrazioni di Validità e di Non Validità di Formule. |
|
Tabella di leggi (utilizzabile durante il secondo
compitino): tabelle-leggi-v3.pdf | ||
16 |
17/11/2016 |
Notazione e leggi per insiemi, intervalli e domini |
Dispense: [LP2], pag 1-9. Lucidi: LPP_2016_10.pdf. |
Estensioni del linguaggio del primo ordine
|
17 |
22/11/2016 |
Quantificatori funzionali |
Dispense: [LP2], fino a pag. 30. Lucidi: LPP_2016_11.pdf. |
|
18 |
24/11/2016 |
Logica di Hoare: Introduzione |
Dispense: [LdH], fino a pag 20. Lucidi: LPP_2016_12.pdf. |
|
19 |
29/12/2016 |
Triple di Hoare: Regole di inferenza per assegnamento, sequenza e comando condizionale. |
Dispense: [LdH], fino a pag 23. Lucidi: LPP_2016_13.pdf. |
Triple di Hoare
|
20 |
01/12/2016 |
Esercitazione su Formalizzazione di Enunciati con Sequenze e Triple di Hoare |
Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf | |
21 |
06/12/2016 |
Triple di Hoare: |
Dispense: [LdH], fino a pag 27. Lucidi: LPP_2016_14.pdf. |
|
22 |
13/12/2016 |
Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo |
Dispense: [LdH], fino a pag 30. Lucidi: LPP_2016_15.pdf. |
|
23 |
15/12/2016 |
Esercitazione su Triple di Hoare |
Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf | |
-- |
22/12/2016 |
Seconda prova di verifica |
Testo:
02-2016-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. |