N. |
DATA |
TITOLO |
RIFERIMENTI |
ARGOMENTI |
1 |
22/09/2009 |
Introduzione al corso, Calcolo Proposizionale |
[LP1], pag 1-8; |
Introduzione al corso; Dimostrazioni; Calcolo proposizionale; Connettivi logici e tabelle di verità; Precedenza tra connettivi logici; Tautologie e contraddizioni; Principio di sostituzione; Leggi per l'equivalenza. |
2 |
25/09/2009 |
Calcolo Proposizionale |
[LP1], fino a pag 12 (Escluso Sezione 4)
|
Leggi per congiunzione e disgiunzione, negazione e implicazione; Insiemi funzionalmente completi di connettivi logici; Alcune leggi derivate; Modus Ponens. |
3 |
29/09/2009 |
Dimostrazioni con Modus Ponens, Forme Normali |
[LP1], fino a pag. 18; |
Implicazioni tautologiche come giustificazioni; Occorrenze positive e negative di sottoformule in una formula; Principio di sostituzione per l'implicazione; Dimostrazione di implicazioni con Modus Ponens; Forma Normale Congiuntiva e Disgiuntiva; Equivalenza di formule tramite riduzione a forma normale. |
4 |
2/10/2009 |
Esercitazione |
Lucidi: Esercitazione_0.pdf |
|
5 |
6/10/2009 |
Formato generale di dimostrazioni |
[LP1], fino a pag. 22 (escluso 6.1); |
Esercizio: il connettivo NAND è funzionalmente completo; Tautologia corrispondente a un passo di dimostrazione; Tautologia corrispondente ad una dimostrazione; Uso di giustificazioni non tautologche. |
6 |
9/10/2009 |
Altre tecniche di dimostrazione |
[LP1], fino a pag. 23; |
Dimostrazione per assurdo; Dimostrazione per casi. Esercizi su: occorrenze positive/negative di sottoformule; tautologie e non; formalizzazione di implicazioni in linguaggio naturale |
7 |
16/10/2009 |
Relazione tra sintassi e semantica |
[LP1], fino a pag. 31 (escluso 8.2); |
Interpretazioni; Modelli; Conseguenze logiche; Correttezza e completezza di un calcolo; Calcolo dei predicati del primo ordine: sintassi |
8 |
20/10/2009 |
Semantica della logica del prim'ordine |
[LP1], fino a pag. 39 (esclusa Sezione 10); |
Interpretazione di un linguaggio del prim'ordine; Semantica dei termini; Semantica delle formule; Modelli; Conseguenza logica; Esempio: il linguaggio della teoria degli insiemi. |
9 |
23/10/2009 |
Esercizi, Calcolo del primo ordine |
[LP1], fino a pag. 46 (esclusa Sezione 10.9); |
Esercizi su formalizzazione di asserzioni in italiano; Concetto di "calcolo" (proof system); Regole di inferenza; Leggi per l'equivalenza; Teorema di deduzione; Leggi per l'implicazione; Formalizzazione del concetto di "relazione di equivalenza su un insieme" |
10 |
27/10/2009 |
Le leggi per i quantificatori |
[LP1], tutta; |
Leggi come formule valide; le leggi dei quantificatori universale ed esistenziale; leggi dell'operatore di uguaglianza; esempi di dimostrazioni nel calcolo del primo ordine |
11 |
30/10/2009 |
Prova di compitino |
|
Verranno proposti degli esercizi di tipologia simile a quelli del primo compitino del prossimo 4 novembre. Gli esercizi verteranno sugli argomenti presentati durante il corso, escluso le leggi e le dimostrazioni del calcolo del primo ordine (ma compreso l'uso di formule del primo ordine per formalizzare asserzioni). |
|
4/11/2009 |
Prima prova in intinere |
Testo con soluzioni: 01-2009-PrimoCompitino-Soluzioni.pdf
|
|
12 |
6/11/2009 |
Applicazioni del calcolo del primo ordine: insiemi |
[LP2], fino a pag 7; |
Notazione intensionale ed estensionale di insiemi; Leggi sugli insiemi; Intervalli; Predicati di disuguaglianza |
13 |
10/11/2009 |
Applicazioni del calcolo del primo ordine: intervalli |
[LP2], fino a pagina 9 |
Notazioni per domini e per intervalli; leggi per domini e per intervalli; formalizzazione di array di interi |
14 |
13/11/2009 |
Leggi per intervalli, Altri quantificatori |
[LP2], fino a pagina 14 |
Formalizzazione di proprietà di array di interi; Quantificatori funzionali: sommatoria, cardinalità, minimo e massimo; alcune leggi dei quantificatori funzionali. |
15 |
17/11/2009 |
Altre leggi per quantificatori funzionali, Esempi di dimostrazioni, Specifiche di stati di computazione. |
[LP2] fino a pagina 21 |
Altre leggi per i quantificatori funzionali: intervallo, singoletto, costante. Quantificazione su dominio vuoto. Esempi di dimostrazioni. |
16 |
20/11/2009 |
Esercitazione; esempi di specifiche. |
[LP2], tutta |
Esercizi di formalizzazione di asserzioni in italiano con logica del primo ordine e uso di sequenze |
17 |
24/11/2009 |
Semantica assiomatica: Introduzione. |
[LdH], fino a pag. 14 |
Semantica informale e formale di linguaggi di programmazione; Sintassi di un linguaggio imperativo minimo: espressioni e comandi; Concetto di stato; Semantica delle espressioni; Semantica informale dei comandi; Definizione di tripla di Hoare. |
18 |
27/11/2009 |
Correzione primo compitino; Triple di Hoare |
[LdH], fino a pag. 20 |
Proprietà di stati e asserzioni; Triple di Hoare; Letture diverse di triple di Hoare: Semantica, Correttezza, Specifica; Regole di Inferenza: rafforzamento di pre- e indebolimento di post-condizione; assiomi per skip e assegnamento. |
19 |
1/12/2009 |
Triple di Hoare; Sequenza e Condizionale |
[LdH], fino a pag. 22 |
Triple di Hoare: Assioma per assegnamento multiplo; Definizione delle esspressioni (funzione def(_)); Regola per sequenza di comandi; Esempi; Regola per Condizionale |
20 |
4/12/2009 |
Triple di Hoare; Condizionale e Iterazione |
[LdH], fino a pag. 27, escluso 5.8 |
Triple di Hoare: Regola per Condizionale; Regola del Comando Iterativo; Esempi |
21 |
11/12/2009 |
Esempi di verifica di Triple di Hoare |
[LdH], fino a pag. 27, escluso 5.8 |
Esempi di verifica di triple di Hoare: fattoriale, sequenza di comandi, comandi condizionali |
22 |
15/12/2009 |
Prova di compitino |
Testo: Pre-SecondoCompitino.pdf |
Verranno proposti degli esercizi di tipologia simile a quelli del secondo compitino del prossimo giovedì 17 dicembre. |
|
17/12/2009 |
Seconda prova in intinere |
Testo con soluzioni: 02-2009-SecondoCompitino-Soluzioni.pdf
|