Logica per la Programmazione - Corso A [LPP-A-12]


DOCENTE Andrea Corradini <andrea@di.unipi.it>
Orario Martedì 14-16, Aula A e Giovedì 11-13, Aula A
Orario ricevimento Cliccare qui

Avvisi


Modalità di esame

L'esame di LPP è costituito da uno scritto e da un orale. Per poter sostenere l’orale è necessario aver superato entrambe le prove in itinere (compitini) con un voto >= 16 e con una media >= 18, oppure aver superato la prova scritta di un appello d'esame con un voto >=16.

Testi delle prove (con alcune soluzioni)

Risultati


Materiale didattico (Dispense, PDF)


Tabella delle lezioni

N.

DATA

TITOLO

RIFERIMENTI

ARGOMENTI

1

25/09/2012

Introduzione al corso

Lucidi: Logica_2010_1.pdf

NB: lezione tenuta dalla Prof. F. Levi

2

27/09/2012

Introduzione al Calcolo Proposizionale

Lucidi: Logica_2010_2.pdf

NB: lezione tenuta dalla Prof. F. Levi

3

2/10/2012

Dimostrazione di Tautologie

Dispense: [LP1], fino a pag 12
Lucidi: Logica_2010_3.pdf
Esercizi proposti e/o svolti a lezione: Esercizi 2, Esercizi 3

Formalizzazione di Enunciati Dichiarativi; 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

4/10/2012

Dimostrazione di Implicazioni Tautologiche,
Forme normali

Dispense: [LP1], fino a pag 18
Lucidi: Logica_2010_4.pdf, tutti
Esercizi: Esercizi proposti a lezione

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

9/10/2012

Esercitazione

Esercizi proposti: Esercitazione_2012_1.pdf

Svolgimento e correzione corale di alcuni esercizi su formalizzazione di enunciati, occorrenze positive e negative, dimostrazione di tautologie.

6

11/10/2012

Dimostrazioni con Ipotesi non Tautologiche

Dispense: [LP1], fino a pag 24, Sezione 7 esclusa
Lucidi: Logica_2010_5.pdf
Esercizi: Esercizi proposti a lezione


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.

7

16/10/2012

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

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

18/10/2012

Semantica della logica del prim'ordine

Dispense: [LP1], pag 36-39
Lucidi: Logica_2010_7.pdf

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.

9

23/10/2012

Il Calcolo del Primo Ordine

Dispense: [LP1]: pag 39-49
Lucidi: Logica_2010_8.pdf [fino a pag. 21]

Sistemi di dimostrazione; Correttezza e completezza; Validità del risultato di una dimostrazione; Teorema di Deduzione; Leggi per quantificatori; Predicato di uguaglianza; Leggi per l'uguaglianza.

10

25/10/2012

Regole di Inferenza per Quantificatori
Esercitazione

Dispense: [LP1] pag. 49-51 + Sezione 8.2 [pag. 32-33]
Lucidi: Logica_2010_8.pdf [tutto]
Alcuni esercizi proposti: Esercitazione_2010_2.pdf

Regole di inferenza: Generalizzazione e Skolemizzazione. Svolgimento di alcuni esercizi su formalizzazione di enunciati con la logica del primo ordine.

11

30/10/2012

Esercitazione


Esercitazione: Esercitazione_2012_4.pdf.

Esercizi su dimostrazioni e formalizzazione con logica del prim'ordine.

12

7/11/2012

Primo compitino

Testo: 01-2012-PrimoCompitino.pdf.

Testo con soluzioni: 01-2012-PrimoCompitino-SOL.pdf.
Risultati

13

8/11/2012

Notazione e leggi per insiemi, intervalli e domini

Lucidi: Logica_2010_9.pdf, Dispense: [LP2], pag 1-9.
Esercizi: Esercizi proposti

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.

14

13/11/2012

Quantificatori funzionali

Lucidi:
Logica_2010_10.pdf, fino a pag. 12.
Dispense: [LP2], fino a pag. 15.

Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo; Formalizzazione di enunciati; Leggi Generali e Leggi Specifiche per Quantificatori Funzionali.

15

15/11/2012

Formalizzazione di enunciati e leggi per quantificatori funzionali

Lucidi:
Logica_2010_10.pdf, tutto.
Dispense: [LP2], pag 16-31.

Quantificatori funzionali: formalizzazione di enunciati, leggi generali e leggi specifiche, leggi dell'intervallo; Esempi di dimostrazione. Formalizzazione di proprietà di relazioni binarie: univalenza, totalià, iniettività, surgettività (si veda pag. 3 di Esercitazione_2010_2_SOL.pdf).

16

20/11/2012

Logica di Hoare: Introduzione

Lucidi:
Logica_2012_11.pdf.
Dispense: [LdH], fino a pag 18.

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.

17

22/11/2012

Triple di Hoare: Regole di inferenza per assegnamento e sequenza.

Lucidi:
Logica_2012_12.pdf.
Esercizi proposti:
Esercizi_2012_12.pdf.
Dispense: [LdH], fino a pag 22.

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. Esempi di verifica di triple.

18

27/11/2012

Triple di Hoare:
Esercizi e Regola del Condizionale

Lucidi:
Logica_2012_12.pdf, ultima pagina.
Logica_2012_13.pdf.
Dispense: [LdH], fino a pag. 23 (escluso sezione 4.7).

Triple di Hoare: Regola per comando condizionale; Esempi di verifica di Triple di Hoare.

19

29/11/2012

Triple di Hoare:
Regola per il Comando Iterativo

Lucidi:
Logica_2012_14.pdf, tutto.
Dispense: [LdH]: fino a pag 27

Triple di Hoare: Regola per il Comando Iterativo; Esempi.

20

4/12/2012

Esercitazione


Esercizi proposti: Esercitazione_2012_5.pdf

Esercizi su Triple di Hoare.

21

6/12/2012

Triple di Hoare:
Sequenze (Array) e Aggiornamento Selettivo

Lucidi:
Logica_2012_15.pdf.
Dispense: [LdH]: fino a pag 30

Regola per aggiornamento selettivo; Esercizi su verifica di triple di Hoare.

22

11/12/2012

Esempi ed esercizi su Triple di Hoare

Lucidi:
Logica_2012_16.pdf.
Dispense: [LdH]: fino a pag 38

Esempi di verifica di Triple di Hoare; Programmi annotati; Semplice esempio di determinazione dell'invariante; Esempi di specifica di programmi.

23

13/12/2012

Esempi ed esercizi su Triple di Hoare

Lucidi:
Logica_2012_16.pdf.

Esempi di specifica di programmi usando Triple di Hoare; Formalizzazione di enunciati su sequenze.

24

18/12/2012

Esercitazione


25

21/12/2012

Secondo compitino

Ore 14 - Aule A, B

Iscrizione obbligatoria alla URL http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/appelli.asp?letter=&ycourse=&course=inf31&year=2013&start=20&end=20
Gli studenti che non hanno superato il Primo Compitino possono fare il Secondo come esercitazione (iscrivendosi regolarmente). Il docente correggerà comunque lo scritto, ma consegnerà correzioni e valutazione solo a mano, su richiesta.
Gli studenti possono consultare durante il compitino dispense e appunti personali. Telefonini e altri apparati elettronici dovranno essere spenti.