Logica per la Programmazione - Corso B [LPP-B-09]


Tabella delle lezioni

N.

DATA

TITOLO

RIFERIMENTI

ARGOMENTI

1

22/09/2009

Introduzione al corso, Calcolo Proposizionale

[LP1], pag 1-8;
Lucidi: Logica_0.pdf fino al lucido 17.

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)
Lucidi: Logica_0.pdf

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;

Lucidi: Logica_1.pdf

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);

Lucidi: Logica_2.pdf fino al lucido 9.

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;

Lucidi: Logica_2.pdf.

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);

Lucidi: Logica_3.pdf, fino al lucido 14.

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);

Lucidi: Logica_3.pdf

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);

Lucidi: Logica_4.pdf fino a lucido 14,
Esercitazione_1.pdf

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;

Lucidi: Logica_4.pdf

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
Risultati: Ris-01.pdf

12

6/11/2009

Applicazioni del calcolo del primo ordine: insiemi

[LP2], fino a pag 7;

Lucidi: Logica_5.pdf

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

Lucidi: Logica_5.pdf

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

Lucidi: Logica_6.pdf

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

Lucidi: Logica_6.pdf

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

Lucidi: Esercitazione_2.pdf

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

Lucidi: Logica_7.pdf

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
Lucidi: Logica_7.pdf

Soluzioni del primo compitino: 01-2009-PrimoCompitino-Soluzioni.pdf
Risultati del primo compitino: Ris-01.pdf

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

Lucidi: Logica_7.pdf

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

Lucidi: Logica_7.pdf

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

Lucidi: Logica_7.pdf

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
Risultati secondo compitino e ammessi all'orale: Ris-02.pdf