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


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

Informazioni utili e 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 di verifica intermedie con un voto >= 16 e con una media >= 18, oppure aver superato la prova scritta di un appello d'esame con un voto >=16. In generale, lo scritto superato in un appello consente di sostenere l'orale solo in un appello della stessa sessione di esami.
Il superamento delle prove di verifica intermedie al posto dello scritto vale solo per la sessione invernale (appelli di gennaio e febbraio).

Testi delle prove (con alcune soluzioni)

Risultati


Materiale didattico (Dispense, PDF)

  1. [LP1] Logica per la Programmazione
  2. [LP2] Logica per la Programmazione 2
  3. [LdH] Logica di Hoare
  4. [Per consultazione] [LMB-INF] Note LMB di Informatica

Materiale didattico in inglese

Come testo di consultazione in inglese, si suggeriscono i Capitoli 1, 2 e 4 del libro LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems, di Michael Huth e Mark Ryan. Pagina web. Scrivere un email al docente per visionare il libro.

Tabella delle lezioni

N.

DATA

TITOLO

RIFERIMENTI

ARGOMENTI

1
29/09/2015
Introduzione al corso
Introduzione al Calcolo Proposizionale
Dispense: [LP1], pag 6--8

Lucidi: LPP_2015_01.pdf

  • Introduzione al corso
  • Introduzione al Calcolo Proposizionale; Connettivi logici; Proposizioni (formule proposizionali); Formalizzazione di enunciati; Formalizzazione di implicazioni in linguaggio naturale; Tautologie e Contraddizioni.
2
1/10/2015
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_2015_02.pdf

  • Dimostrazione di Tautologie
    • Tabelle di verità
    • Dimostrazioni per sostituzione
    • Leggi del Calcolo Proposizionale
  • Insiemi funzionalmente completi di connettivi
3
6/10/2015
Dimostrazione di Tautologie e Sintassi del Calcolo Proposizionale Dispense: [LP1], fino a pag 12

Lucidi: LPP_2015_03.pdf

  • Tautologie: dimostrazioni e controesempi
  • Sulla sintassi del Calcolo Proposizionale
  • Ambiguità precedenza tra connettivi e parentesi
  • Altre Leggi del Calcolo Proposizionale
4
8/10/2015

Esercitazione su Calcolo Proposizionale

Esercizi proposti

Tabella di leggi (utilizzabile durante il primo compitino): tabelle-leggi-v1.pdf

5
13/10/2015
Dimostrazione di Implicazioni Tautologiche Dispense: [LP1], fino a pag 18

Lucidi: LPP_2015_04.pdf

  • Principio di sostituzione per l’implicazione
  • Occorrenze positive e negative
  • Altre tecniche di dimostrazione
  • Forme Normali e Principio di Risoluzione
6
15/10/2015

Dimostrazioni e Tautologie, Ipotesi non tautologiche

Dispense: [LP1], fino a pag 23

Lucidi: LPP_2015_05.pdf

  • Inferenze corrette come tautologie
  • Tautologie come schemi di dimostrazione
  • Dimostrazioni con ipotesi non tautologiche

7
20/10/2015

Esercitazione su Calcolo Proposizionale

Esercizi proposti

Tabella di leggi (utilizzabile durante il primo compitino): tabelle-leggi-v1.pdf
Attenzione: Gli studenti sono invitati a continuare autonomamente la risoluzione degli esercizi proposti e non svolti durante l'esercitazione. Nel caso di dubbi o per correggere le soluzioni rivolgersi al docente nell'orario di ricevimento (Lun 16-18). Le soluzioni verranno pubblicate verso la metà della prossima settimana.

8
22/10/2015

Logica del Primo Ordine: Motivazioni, Sintassi e Interpretazioni. Formalizzazione di enunciati.

Dispense: [LP1], Sezioni 8 e 8.1 [pag 27-31]
[LMB-INF] Capitolo 4, "Logica dei Predicati", pag 50-55, fino a Sezione 4.3.1 esclusa.

Lucidi: LPP_2015_06.pdf

  • Limiti del Calcolo Proposizionale
  • Sintassi della Logica del Primo Ordine: Alfabeto, Grammatica, Termini, Formule
  • Occorrenze legate e libere di variabili; Formule aperte e chiuse
  • Interpretazione di un linguaggio del primo ordine
  • Formalizzazione di enunciati: linee guida ed esempi.

9

27/10/2015

Logica del Primo Ordine: Semantica

Dispense: [LP1], pag 36-38

Lucidi: LPP_2015_07.pdf

Semantica della Logica del Primo Ordine: Assegnamenti; Semantica dei termini; Semantica di formule per induzione strutturale; Esempi.

10

Venerdì
30/10/2015
ore 9:00

Esercitazione su Formalizzazione e Semantica del primo ordine

Esercizi proposti

Attenzione: causa sospensione dell'attività didattica per assemblea, l'esercitazione si terrà Venerdì 30 ottobre alle ore 9:00 in Aula A.

Tabelle con leggi del calcolo proposizionale (e semantica della Logica dei Predicati): tabelle-leggi-v1.pdf

11

5/11/2015

Prima prova di verifica

Testo: 01-2015-PrimoCompitino.pdf
Soluzioni: 01-2015-PrimoCompitinoSol.pdf

Risultati: 01-2015-Risultati.pdf

12

10/11/2015

Logica del Primo Ordine: Proof System

Dispense: [LP1], pag 39-40

Lucidi: LPP_2015_08.pdf, fino a pag. 160.

Modelli; Formule valide e soddisfacibili; Conseguenza logica; Sistemi di dimostrazione; Correttezza e completezza; Validità del risultato di una dimostrazione; Teorema di Deduzione; Leggi per quantificatori.

13

12/11/2015

Logica del Primo Ordine: Proof System (2)

Dispense: [LP1], pag 49-51

Lucidi: LPP_2015_08.pdf, tutti.

Leggi valide solo su dominio non vuoto; Quantificazione su dominio vuoto: discussione; Predicato di uguaglianza; Leggi per l'uguaglianza. Regole di inferenza: Generalizzazione e Skolemizzazione; Esempi di dimostrazione.

14

17/11/2015

Notazione e leggi per insiemi, intervalli e domini

Dispense: [LP2], pag 1-9.

Lucidi: LPP_2015_09.pdf, tutti.

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.

15

19/11/2015

Quantificatori funzionali

Dispense: [LP2], fino a pag. 30.

Lucidi: LPP_2015_10.pdf.

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

16
24/11/2015

Esercitazione su Dimostrazioni di Validità e Formalizzazione di Enunciati.

Esercizi proposti

Tabella di leggi (utilizzabile durante il secondo compitino): tabelle-leggi-v3.pdf

17

26/11/2015

Logica di Hoare: Introduzione

Dispense: [LdH], fino a pag 20.

Lucidi: LPP_2015_11.pdf.

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.

18

01/12/2015

Triple di Hoare: Regole di inferenza per assegnamento, sequenza e comando condizionale.

Dispense: [LdH], fino a pag 23.

Lucidi: LPP_2015_12.pdf.

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. Regola per comando condizionale; Esempi di verifica di Triple di Hoare.

19

03/12/2015

Esercitazione su Triple di Hoare

Esercizi proposti

Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf

20

09/12/2015
ore 14-16, Aula A

Triple di Hoare:
Regola per il Comando Iterativo

Dispense: [LdH], fino a pag 27.

Lucidi: LPP_2015_13.pdf.

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

21

10/12/2014

Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo

Dispense: [LdH], fino a pag 30.

Lucidi: LPP_2015_14.pdf.

Sequenze: sintassi e semantica; Assioma e regola per aggiornamento selettivo; Esercizi su verifica di triple di Hoare.

22

15/12/2015

Esercitazione su Triple di Hoare

Esercizi proposti

23

17/12/2014
ore 14-16

Seconda prova di verifica

Testo: 02-2015-SecondoCompitino.pdf
Soluzioni: 02-2015-SecondoCompitinoSol.pdf

Iscrizione obbligatoria alla pagina https://esami.unipi.it/esami2/
La seconda prova intermedia del 17 dicembre 2014 è riservata agli studenti che hanno avuto almeno 16 alla prima prova intermedia del 4 novembre 2014. Gli studenti che hanno avuto "insufficiente" possono comunque sostenere la prova come esercitazione, iscrivendosi alla pagina indicata sopra, ma il loro elaborato non verrà corretto.

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.