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

DOCENTE Andrea Corradini <andrea@di.unipi.it>

Orario Martedì 14-16, Aula A e Giovedì 14-16, Aula A

Orario ricevimento Cliccare qui.

Informazioni utili e Avvisi

[7 settembre 2018] Visione correzioni quinto appello del 4/9/2018 e orali: Lunedì 10 settembre, ore 9:30, in Aula N1. Gli orali proseguiranno per tutta la giornata.
Attenzione: L'ammissione all'orale (votazione maggiore di 15 nello scritto del quinto appello) vale anche per il prossimo appello di Gennaio 2019.
[10 luglio 2018] Ho pubblicato i risultati del quarto appello del 6/7 scorso. Visione correzioni quarto appello e inizio orali: Mercoledì 11 luglio, ore 9:30, in Aula C. Gli orali proseguiranno per tutta la giornata.
Attenzione: L'ammissione all'orale (votazione maggiore di 15 nello scritto del quarto appello) vale anche per l'appello di settembre.
[17 giugno 2018] Ho pubblicato i risultati del terzo appello del 15/6 scorso. Visione correzioni terzo appello e inizio orali: Lunediì 18 giugno, ore 14:00, in Sala Riunioni Est, Dipartimento di Informatica. Gli orali proseguiranno Giovedì 21 giugno alle ore 14:00.
[14 febbraio 2018] Gli orali di domani, 15/2, si terranno in Aula L1 a partire dalle 11.
[12 febbraio 2018] Ho pubblicato i risultati del secondo appello del 8/2 scorso. Visione correzioni secondo appello e prenotazione orali: Martedì 13 febbraio, ore 9:30, in Aula L1. Gli orali cominceranno subito dopo e proseguiranno nei giorni seguenti.
Attenzione: Mi scuso per lo scarso prevviso. Pubblichero' domani (13/2) in tarda mattinata le istruzioni per prenotarsi per l'orale per coloro che non sono potuti venire alla correzione.
[26 gennaio 2018] Ho pubblicato i risultati del primo appello del 18/1 scorso. Visione correzioni primo appello e prenotazione orali: Lunedì 29 gennaio, ore 13:30, in Aula C.. Gli orali cominceranno subito dopo e proseguiranno nei giorni seguenti:
- Mercoledì 31/1
- Venerdì 2/2
- Martedì 6/2
Attenzione: Inviare un email al docente se non si può essere presenti, con oggetto "[LPP 2017] Richiesta data orale" indicando le date preferite.
Si ricorda che il superamento dell'esame scritto (con compitini o prova finale) ha validità fino alla fine della corrispondente sessione. Pertanto gli studenti attualmente ammessi all'orale possono sostenerlo anche con gli orali del secondo appello.
[10 gennaio 2018] Gli orali di questa settimana proseguono domani 11/1 e dopodomani 12/1 la mattina dalle ore 9:00 e il pomeriggio dalle ore 14:30, sempre in Aula C. Se qualcuno vuole ancora iscriversi ci sono degli slot liberi venerdì 12.
[3 gennaio 2018] Ho pubblicato i risultati del secondo compitino del 21/12 scorso e i voti di ammissione all'orale. Visione correzioni secondo compitino e prenotazione orali: Martedì 9 gennaio, ore 13:00, in aula C. Gli orali cominceranno subito dopo e proseguiranno nei giorni seguenti.
Attenzione: le prenotazioni per gli orali NON si raccolgono tramite il portale ESAMI, ma solo il 9/1 alle 13:00 in aula C. Inviare un email al docente se non si può essere presenti.
Si ricorda che il superamento dell'esame scritto (con compitini o prova finale) ha validità fino alla fine della corrispondente sessione. Pertanto gli studenti attualmente ammessi all'orale possono sostenerlo anche con gli orali del primo o del secondo appello.
[17 novembre 2017] Ho pubblicato i risultati del primo compitino del 2/11 scorso. Per vedere le correzioni potete venire a ricevimento.
[14 novembre 2017] Le registrazioni delle lezioni dell'anno 2015/16 sono accessibili alla URL <http://owncloud-usid.unipi.it/index.php/s/G8vYwNWZqrTSIxa>. Per la passwd rivolgersi al docente. Di alcune lezioni potrebbe mancare l'audio: richiederlo per email al docente.
[26 ottobre 2017] Il ricevimento del primo novembre 2017 (festivo) è anticipato a Martedì 31 ottobre alle ore 11, presso lo studio del docente.
[19 settembre 2017] Il corso inizierà Martedì 19 settembre 2017.

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).
Attenzione: Gli studenti che a Novembre sono ancora gravati da O.F.A. non possono sostenere la prima prova di verifica intermedia (si veda https://www.di.unipi.it/it/didattica/inf-l/test-d-ingresso-e-corsi-di-recupero).

Testi delle prove (con alcune soluzioni)

[2 novembre 2017] Testo primo compitino; Testo con soluzioni.
[21 dicembre 2017] Testo secondo compitino; Testo con soluzioni.
[18 gennaio 2018] Testo primo appello; Testo con soluzioni
[8 febbraio 2018] Testo secondo appello
[15 giugno 2018] Testo terzo appello

Materiale didattico (Dispense, PDF)

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

Lettere dell'alfabeto greco

Teaching material in English

For foreign students unable to understand Italian, the teaching material consists of Chapter 1, 2 and 4 of the following book: LOGIC IN COMPUTER SCIENCE Modelling and Reasoning about Systems, di Michael Huth e Mark Ryan. Web page. Please contact the lecturer if you need to take the exam in English.

Tabella delle lezioni

N.	DATA	TITOLO	RIFERIMENTI	ARGOMENTI
1	19/09/2017	Introduzione al corso Introduzione al Calcolo Proposizionale	Dispense: [LP1], pag 6--8 Lucidi: LPP_2017_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	22/09/2017	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_2017_02.pdf	Dimostrazione di Tautologie Tabelle di verità Dimostrazioni per sostituzione Leggi del Calcolo Proposizionale
3	26/09/2017	Dimostrazione di Tautologie e Sintassi del Calcolo Proposizionale	Dispense: [LP1], fino a pag 12 Lucidi: LPP_2017_03.pdf	Tautologie: dimostrazioni e controesempi Sulla sintassi del Calcolo Proposizionale Ambiguità, precedenza tra connettivi e parentesi Altre Leggi del Calcolo Proposizionale
4	28/9/2017 Aule A + E	Esercitazione su Calcolo Proposizionale	Esercizi proposti	Tabella di leggi: tabelle-leggi-v1.pdf
5	3/10/2017	Dimostrazione di Implicazioni Tautologiche	Dispense: [LP1], fino a pag 18 Lucidi: LPP_2017_04.pdf	Principio di sostituzione per l’implicazione Occorrenze positive e negative Altre tecniche di dimostrazione Forme Normali e Principio di Risoluzione Insiemi funzionalmente completi di connettivi logici
6	5/10/2017	Dimostrazioni e Tautologie, Ipotesi non tautologiche	Dispense: [LP1], fino a pag 23 Lucidi: LPP_2017_05.pdf	Tautologie come schemi di dimostrazione Dimostrazioni con ipotesi non tautologiche
7	10/10/2017	Esercitazione su Calcolo Proposizionale	Esercizi proposti	Tabella di leggi (utilizzabile durante il primo compitino): tabelle-leggi-v1.pdf
8	12/10/2017	Logica del Primo Ordine: Motivazioni, Sintassi e Interpretazioni.	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_2017_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
9	17/10/2017	Logica del Primo Ordine: Formalizzazione e Semantica	Dispense: [LP1], pag 33-35 Lucidi: LPP_2017_07.pdf fino a pag. 134.	Interpretazione di un linguaggio del primo ordine Formalizzazione di enunciati: linee guida ed esempi Semantica della Logica del Primo Ordine Assegnamenti Semantica dei termini per induzione strutturale Esempi Semantica di formule per induzione strutturale
10	19/10/2017	Logica del Primo Ordine: Semantica	Dispense: [LP1], pag 36-38 Lucidi: LPP_2017_07.pdf	Semantica di formule per induzione strutturale Esempi Esercizi su semantica di formule del primo ordine
11	24/10/2017	Esercitazione su Formalizzazione e Semantica del primo ordine	Esercizi proposti	Tabella di leggi (utilizzabile durante il primo compitino): tabelle-leggi-v1.pdf
12	26/10/2017	Logica del Primo Ordine: Proof System	Dispense: [LP1], pag 39-46 Lucidi: LPP_2017_08.pdf	Modelli Formule valide e soddisfacibili Conseguenza logica Sistemi di dimostrazione Correttezza e completezza Validità del risultato di una dimostrazione Teorema di Deduzione
--	2/11/2017	Prima prova di verifica		Testo: 01-2017-PrimoCompitino.pdf Soluzioni: 01-2017-PrimoCompitinoSol.pdf
13	7/11/2017	Logica del Primo Ordine: Proof System (2)	Dispense: [LP1], pag 47-51 Lucidi: LPP_2017_09.pdf, fino a pag. 14.	Leggi per quantificatori Leggi valide solo su dominio non vuoto Leggi per quantificatori su dominio Formule vacuamente vere/false Predicato di uguaglianza; Leggi per l'uguaglianza Esempi di dimostrazioni
14	9/11/2017	Logica del Primo Ordine: Proof System (3)	Dispense: [LP1], pag 47-51 Lucidi: LPP_2017_09.pdf, tutti.	Regole di inferenza: Generalizzazione e Skolemizzazione Esempi di dimostrazione Esempi di formule valide e non valide
15	14/11/2017	Esercitazione su Dimostrazioni di Validità e di Non Validità di Formule.	Esercizi proposti	Tabella di leggi (utilizzabile durante il secondo compitino): tabelle-leggi-v3.pdf
16	16/11/2017	Notazione e leggi per insiemi, intervalli e domini	Dispense: [LP2], pag 1-9. Lucidi: LPP_2017_10.pdf.	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 Leggi dell'intervallo per quantificatori Definizione di array Formalizzazione di enunciati su array
17	21/11/2017	Quantificatori funzionali	Dispense: [LP2], fino a pag. 30. Lucidi: LPP_2017_11.pdf.	Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo Leggi per quantificatori funzionali Leggi dell'intervallo Formalizzazione di enunciati
18	23/11/2017	Esercitazione su Formalizzazione di Enunciati con Sequenze.	Esercizi proposti	Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf
19	28/11/2017	Logica di Hoare: Introduzione	Dispense: [LdH], fino a pag 20. Lucidi: LPP_2017_12.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
20	30/11/2017	Triple di Hoare: Regole di inferenza per assegnamento, sequenza e comando condizionale.	Dispense: [LdH], fino a pag 23. Lucidi: LPP_2017_13.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.
21	05/12/2017	Esercitazione su Triple di Hoare	Esercizi proposti	Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf
22	07/12/2017	Triple di Hoare: Regola per il Comando Iterativo	Dispense: [LdH], fino a pag 27. Lucidi: LPP_2017_14.pdf.	Triple di Hoare: Regola per il Comando Iterativo Esempi
23	12/12/2017	Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo	Dispense: [LdH], fino a pag 30. Lucidi: LPP_2017_15.pdf.	Sequenze: sintassi e semantica Assioma e regola per aggiornamento selettivo Esercizi su verifica di triple di Hoare
24	14/12/2017	Esercitazione su Triple di Hoare	Esercizi proposti	Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf
--	21/12/2017 ore 9-11	Seconda prova di verifica	Testo: 02-2017-SecondoCompitino.pdf Soluzioni: 02-2017-SecondoCompitinoSol.pdf	Iscrizione obbligatoria alla pagina https://esami.unipi.it/esami2/ La seconda prova intermedia del 21 dicembre 2017 è riservata agli studenti che hanno avuto almeno 16 alla prima prova intermedia del 2 novembre 2017. 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.

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