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


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

Avvisi


Modalità di esame

Scritto (eventualmente sostituito da due prove in itinere) e orale.
I periodi degli appelli sono riportati nel Calendario Accademico.

Testi delle prove con soluzioni

Risultati


Materiale didattico (Dispense, PDF)


Tabella delle lezioni

N.

DATA

TITOLO

RIFERIMENTI

ARGOMENTI

1

20/09/2011

Introduzione al corso
Introduzione al Calcolo Proposizionale

Lucidi: Logica_2010_1.pdf.
Logica_2010_2.pdf, fino a pag. 13.
Esercizi: Esercizi proposti a lezione

Introduzione al corso: La logica da Aristotele alla logica matematica; Logica e informatica; Contenuto del corso.
Introduzione al Calcolo Proposizionale: Connettivi logici; Sintassi del Calcolo Proposizionale; Semantica dei connettivi logici con Tabelle di Verità; Formalizzazione di enunciati dichiarativi; Tautologie e Contraddizioni.

2

22/09/2011

Calcolo Proposizionale
Dimostrazioni di Tautologie

Dispense: [LP1], fino a pag 10
Lucidi: Logica_2010_2.pdf, tutti
Logica_2010_3.pdf, fino a pag 23.
Esercizi: Esercizi proposti a lezione

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

3

27/09/2011

Dimostrazioni di Implicazioni Tautologiche

Dispense: [LP1], fino a pag 16
Lucidi: Logica_2010_3.pdf, tutti
Lucidi: Logica_2010_4.pdf, fino a pag. 19

Insiemi Funzionalmente Completi di Connettivi Logici
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;

4

4/10/2011

Forme normali
Esercitazione

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

Esercizi proposti: Esercitazione_2010_1.pdf

Forma normale congiuntiva e disgiuntiva; Il Principio di Risoluzione.
Svolgimento di alcuni esercizi su formalizzazione di enunciati, occorrenze positive e negative, dimostrazione di tautologie.

5

6/10/2011

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.

6

11/10/2011

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.

7

13/10/2011

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.

8

18/10/2011

Esercitazione

Dispense: [LP1], Sezione 8.2 [pag. 32-33]
Alcuni esercizi proposti: Esercitazione_2010_2.pdf

Svolgimento di alcuni esercizi su formalizzazione di enunciati con la logica del primo ordine.

9

20/10/2011

Il Calcolo del Primo Ordine

Dispense: [LP1]: pag 39-48
Lucidi: Logica_2010_8.pdf [fino a pag. 18]

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

10

25/10/2011

Il Calcolo del Primo Ordine

Dispense: [LP1], pag. 48-51
Lucidi: Logica_2010_8.pdf [tutto]
Esercizi: Esercizi proposti a lezione

Ancora leggi per quantificatori; Predicato di uguaglianza; Leggi per l'uguaglianza; Regole di inferenza: Generalizzazione e Skolemizzazione. Esercizi vari.

11

27/10/2011

Esercitazione

Esercizi della Lezione 8
Esercitazione_2010_2.pdf

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

12

4/11/2011

Primo compitino

Ore 14:00, Aule A, B, C.

Iscrizione obbligatoria alla URL http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/appelliret.asp?start=10&end=10&chk=3553
Gli studenti possono consultare durante il compitino dispense e appunti personali. Telefonini e altri apparati elettronici dovranno essere spenti.

13

8/11/2011

Notazione e leggi per insiemi, intervalli e domini

Lucidi: Logica_2010_9.pdf, Dispense: [LP2], pag 1-7.
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.

14

10/11/2011

Leggi di intervallo, Quantificatori funzionali, Formalizzazione di enunciati

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

Leggi dell'intervallo per quantificatori; Definizione di array; Formalizzazione di enunciati su array; Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo.

15

15/11/2011

Formalizzazione di enunciati e leggi per quantificatori funzionali

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

Quantificatori funzionali: formalizzazione di enunciati, leggi generali e leggi specifiche, leggi dell'intervallo; Esempi di dimostrazione.

16

17/11/2011

Logica di Hoare: Introduzione

Lucidi:
Logica_2010_11.pdf, fino a pag. 13.
Dispense: [LdH], fino a pag 17.

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.

17

22/11/2011

Triple di Hoare: definizioni e regole di inferenza

Lucidi:
Logica_2010_11.pdf, fino a pag. 21.
Dispense: [LdH], fino a pag 22.

Interpretazione di triple di Hoare: semantica, correttezza, specifica. 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.

18

24/11/2011

Triple di Hoare:
Esercizi e Regola del Condizionale

Lucidi:
Logica_2010_11.pdf, fino a pag. 22.
Logica_2010_12.pdf, pag. 2 e 4.
Dispense: [LdH], fino a pag. 23 (escluso sezione 4.7).

Triple di Hoare: Assioma e Regola per l'Assegnamento, Regola della Sequenza, Regola per comando condizionale; Esempi di verifica di Triple di Hoare.

19

29/11/2011

Triple di Hoare:
Regola per il Comando Iterativo, Esercizi

Lucidi:
Logica_2010_11.pdf, tutto.
Logica_2010_12.pdf pag 6 e 7.
Dispense: [LdH]: fino a pag 27

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

--

29/11/2011

Esercitazione straordinaria

Aula B, ore 14:15-16:00
Esercizi proposti: 2011-11-29-EsercitazioneRecupero.pdf

Visione correzioni primo compititno del 4/11/2011; esercitazione di ripasso su Calcolo Proposizionale e Logica del Prim'Ordine

20

1/12/2011

Triple di Hoare

Lucidi:
Logica_2010_12.pdf fino a pag 9.
Dispense: [LdH], fino a pag 27, pag. 31--33.

Triple di Hoare: Variabili di Specifica, Programmi annotati, Esempi di verifica di triple con Regola per il Comando Iterativo.

21

6/12/2011

Triple di Hoare

Lucidi:
Logica_2010_12.pdf fino a pag 15.
Dispense: [LdH], fino a pag 38.

Ricapitolazione su Sequenze: sintassi, semantica e regola per aggiornamento selettivo.

22

13/12/2011

Esercizi di ricapitolazione

Lucidi:
Logica_2010_13.pdf.

Esercizi ed esempi su Triple di Hoare, formalizzazione di enunciati.

23

15/12/2011

Esercitazione

Testo esercizi:
2011-12-15-EsercitazioneFinale.pdf.

 

--

19/12/2011

Secondo compitino

Ore 16, Aule A, B, C

Iscrizione obbligatoria alla URL http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/appelliret.asp?start=20&end=20&chk=3553&chk=3554
Gli studenti che non hanno superato il Primo Compitino possono fare il Secondo come esercitazione (iscrivendosi regolarmente): il loro scritto non verrà corretto.
Gli studenti possono consultare durante il compitino dispense e appunti personali. Telefonini e altri apparati elettronici dovranno essere spenti.