Logica per la Programmazione - Corso A [LPP-B-14]

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

[9 luglio 2015]
Risultati del quarto appello: Ris-06-2014.pdf
Correzione: Venerdì 10 luglio ore 12:00 in Sala Riunioni Ovest del Dipartimento di Informatica.
[18 giugno 2015]
Risultati del terzo appello: Ris-05-2014.pdf
Correzione e orali: Lunedì 22 giugno ore 10:00 in Aula B.
[17 febbraio 2015]
Lista orali del 18/2, dalle 12:00 in Aula L1, nell'ordine: NERVI, ODORISIO, POGGI, COCCA, SIRONI, CIPOLLITTI, PROTANO, BASSI, GUARINO, CASCINO, GRASSINO
Lista orali del 19/2 mattina, dalle 9:00 in Aula B, nell'ordine:PISTOLESI, CASENOVE, PIRAJNO, PIETROSANTE, CAPOZZA, COLOMBINI, BISCONTI
Lista orali del 19/2 pomeriggio, dalle 15:30 in Aula B, nell'ordine: TIZZANO, CHEIKH MED, D'AQUINO, DI LELLA, CATANIA, ARRIGOTTI
Lista orali del 20/2 mattina, dalle 9:00 in Aula B, nell'ordine: GUGLIELMO, MARRELLA, LISCI, MONTI, CARLI, SCARSELLI, MENCHINI
Lista studenti ammessi all'orale, nell'ordine in cui verranno considerate le preferenze per la data e in cui si svolgeranno gli orali: AMMESSI_ORALI-SecondoAppello-Voti.pdf
[16 febbraio 2015]Risultati del secondo appello: Ris-04-2014.pdf
Correzione e inizio orali: Martedì 17 febbraio ore 14:30, in Aula L1. Gli orali proseguiranno mercoledì 18 dalle 12:00 in Aula L1 e la mattina di giovedì 19 dalle 9:00 in Aula B. Coloro che non possono venire il 17/2 devono mandarmi un email indicando la preferenza. Ogni sera pubblichero' la lista delle persone iscritte all'orale del giorno successivo.
[15 febbraio 2015] Pubblicati testi e soluzioni del secondo appello dell'11 febbraio.
[27 gennaio 2015] Lista orali di mercoledì 28/1, ore 9:00: Serra, Guglielmo, Ferrando, Orlando, Cascino, Bova, La Placa, Lanza
[26 gennaio 2015] Lista orali di martedì 27/1: Gravina, Balducci, Szczygiel, Cecchetto, Chessa, Lami, Cancro, Purgatorio, Morelli.
[25 gennaio 2015] Elenco ammessi orali e ordine precedenza orali: AMMESSI_ORALI_2.pdf.
Gli orali iniziano Lunedì 26/1 dopo la visione delle correzioni, e continuano: Lunedì per tutta la giornata; Martedì 27/1 dalle 14:00; e Mercoledì 28/1 dalle 9:00, sempre in Aula B. Si può fare l'orale anche dopo lo scritto del secondo appello dell'11 febbraio.
Gli studenti che non possono venire il 26/1 alle 9:30 sono pregati di mandare un email al docente indicando quando desiderano farlo (se il 27-28/1 o a febbraio). La lista degli iscritti all'orale del 27 e 28/1 sarà pubblicata la sera precedente.
[23 gennaio 2015] Pubblicati testi e soluzioni degli scritti del 16 gennaio scorso.
Risultati del primo appello e dei recuperi: Ris-03-2014.pdf
Visione scritti ed inizio orali: Lunedì 26 gennaio, ore 9:30, aula B.
Si invitano fortemente tutti gli studenti, e soprattutto coloro che non hanno passato lo scritto, a prendere visione delle correzioni fatte, per evitare di ripetere gli stessi errori.
[19 gennaio 2015] Elenco studenti iscritti all'orale, nell'ordine:
1. Martedì 20 gennaio, aula A1, ore 9:00:
  Cameriero Marco, Sabella Samuele, Corbucci Luca, Ricucci Giovanni, Finocchio Federico
2. Mercoledì 21 gennaio, aula A1, ore 9:00:
  Sisbarra Antonio, Pandelea Vlad Alexandru, Aurora Emanuele, Alessi Carlo, Torris Emanuele, Casalini Lorenzo, Capozza Matteo, Ceccarini Gabriele, Mauro Giovanni.
Segnalare eventuali errori per email al docente.
[12 gennaio 2015] Elenco studenti che hanno passato almeno un compitino, con eventuale voto di ammissione all'orale: Ris-02B-2014.
Gli orali per gli studenti ammessi con i compitini si terrano tra Lunedì 19 e Mercoledì 21, mattina e pomeriggio, in Aula A1. Presentarsi Lunedì 19 gennaio alle ore 9:30 in aula A1 per concordare la data: gli orali inizieranno subito dopo. Verrà data precedenza in base al voto di ammissione. Inviare un email al docente se non si può intervenire, indicando giorno e orario preferito.
[8 gennaio 2015] Pubblicati i risultati del secondo compitino. Iscrivendosi allo scritto del 16 gennaio 2015, indicare nelle note se si intende sostenere solo una parte del compito.
[18 dicembre 2014] Pubblicato il testo della seconda prova intermedia e le relative soluzioni. La pubblicazione della correzione è prevista per il 7 gennaio 2015. Buone feste a tutti.
[18 dicembre 2014] Per la seconda prova intermedia di oggi alle 14, gli studenti del Corso A si devono presentare in Aula A, e quelli del Corso B in Aula B alle 13:55 al più tardi.
[15 dicembre 2014] Possono sostenere la seconda prova intermedia del 18 dicembre 2014 anche gli studenti che sono risultati insufficienti alla prima prova intermedia del 4 novembre 2014.
[10 dicembre 2014] Ho pubblicato i risultati del primo compitino. Mi scuso ancora per il ritardo.
[14 novembre 2014] Causa Consiglio di Dipartimento, il ricevimento di Lunedì 17 novembre si svolgerà dalle 15:30 alle 16:00 e da dopo la fine del Consiglio fino alle 19:30.
[6 novembre 2014] Abbiamo pubblicato il testo e le soluzioni del Primo Compitino.
[4 novembre 2014] Per il primo compitino, gli studenti devono presentarsi oggi alle ore 13:50 nelle seguenti aule:
- Da AHMED DANIELE a DONATI LUCA in Aula A
- Da DOVERI MARCO a NOTO DANILO in Aula E
- Da NOVELLI FRANCESCO a ROGNINI ALESSANDRO in Aula B
- Da ROMEO GIUSEPPE a ZINNO GERARDO in Aula C
[10 settembre 2014] Il corso inizierà Martedì 30 settembre 2014, alle ore 14:00 in Aula B.

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).
Possono sostenere la seconda prova intermedia del 18 dicembre 2014 anche gli studenti che sono risultati insufficienti alla prima prova intermedia del 4 novembre 2014
Solo per il primo appello del 16 gennaio 2015, indipendentemente dall'aver superato una, entrambe o nessuna prova di verifica, ogni studente si può iscrivere o per lo scritto totale, o per una sola parte (nell'ultimo caso indicandolo come nota al momento dell'iscrizione). La consegna dell'elaborato annulla automaticamente l'eventuale elaborato corrispondente precedentemente superato.
Negli appelli successivi non sarà possibile recuperare solo parte dello scritto.

Testi delle prove (con alcune soluzioni)

[4 novembre 2014] Testo primo compitino; Testo con soluzioni
[18 dicembre 2014] Testo secondo compitino; Testo con soluzioni.
[16 gennaio 2015] Testo primo appello; Testo con soluzioni
[16 gennaio 2015] Testo recupero primo compitino; Testo con soluzioni
[16 gennaio 2015] Testo recupero secondo compitino; Testo con soluzioni
[11 febbraio 2015] Testo secondo appello; Testo con soluzioni

Risultati

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

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	30/09/2014	Introduzione al corso Introduzione al Calcolo Proposizionale	Lucidi: Logica_2014_01.pdf Logica_2014_02.pdf fino a pag. 12	Introduzione al corso Introduzione al Calcolo Proposizionale Connettivi logici; Proposizioni (formule proposizionali); Formalizzazione di enunciati; Formalizzazione di implicazioni in linguaggio naturale.
2	02/10/2014	Dimostrazione di Tautologie	Dispensa: [LP1] fino a pag 11; [LMB-INF] Sezione 1.4, "Dimostrazioni per sostituzione", pag 4-7, e sezione 3.2.1, "Interpretare le formule proposizionali", pag. 32-35. Lucidi: Logica_2014_02.pdf, tutti. Logica_2014_03.pdf, tutti. Logica_2014_03bis.pdf, fino a pag. 5.	Tautologie e Contraddizioni; Dimostrazione di tautologie; Interpretazioni; Tabelle di verità; Principio di Sostituzione; Concetto di Legge del Calcolo Proposizionale; Leggi per Equivalenza, Congiunzione, Disgiunzione, Negazione, Implicazione; Insiemi funzionalmente completi di connettivi logici.
3	7/10/2014	Dimostrazione di Equivalenze Tautologiche, Sulla sintassi del Calcolo Proposizionale	Lucidi: Logica_2014_03bis.pdf, tutti.	Insiemi Funzionalmente Completi di Connettivi Logici; Esempi di dimostrazioni; Leggi di Assorbimento e Complemento; Ambiguità della sintassi del Calcolo Proposizionale; Precedenza tra i connettivi logici.
4	9/10/2014	Esercitazione su Calcolo Proposizionale	Esercizi proposti	Tabelle con leggi del calcolo proposizionale (e semantica della Logica dei Predicati): tabelle-leggi-v1.pdf
5	14/10/2014	Dimostrazione di Implicazioni Tautologiche, Forme normali	Dispense: [LP1], fino a pag 17 Lucidi: Logica_2014_04.pdf	Dimostrazioni di implicazioni; Occorrenze positive e negative; Principio di Sostituzione per l'Implicazione; Forma normale congiuntiva e disgiuntiva; Il Principio di Risoluzione.
6	16/10/2014	Dimostrazione di Implicazioni Tautologiche, Forme normali	Dispense: [LP1], fino a pag 23 [LMB-INF] Sezione 3.3, "Formalizzare proposizioni e inferenze", pag 35-37. Lucidi: Logica_2014_05.pdf	Rappresentazione di inferenze e tecniche di dimostrazione come tautologie; Dimostrazioni come tautologie; Dimostrazioni con ipotesi non tautologiche.
7	21/10/2014	Esercitazione su Calcolo Proposizionale	Esercizi proposti	Tabelle con leggi del calcolo proposizionale (e semantica della Logica dei Predicati): tabelle-leggi-v1.pdf
8	23/10/2014	Logica del Primo Ordine: Motivazioni, Sintassi e Interpretazioni. Formalizzazione di enunciati.	Dispense: [LP1], Sezioni 8 e 8.1 [pag 27-31], 9 e 9.1 [pag 33-35] [LMB-INF] Capitolo 4, "Logica dei Predicati", pag 50-55, fino a Sezione 4.3.1 esclusa. Lucidi: Logica_2014_06.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.
9	28/10/2014	Logica del Primo Ordine: Semantica	Dispense: [LP1], pag 36-38 Lucidi: Logica_2014_07.pdf	Semantica della Logica del Primo Ordine: Semantica di termini chiusi e aperti; Assegnamenti; Semantica di formule per induzione strutturale; Esempi.
10	30/10/2014	Esercitazione su Formalizzazione e Semantica del primo ordine	Esercizi proposti	Tabelle con leggi del calcolo proposizionale (e semantica della Logica dei Predicati): tabelle-leggi-v1.pdf
11	4/11/2014	Prima prova di verifica	Testo: 01-2014-PrimoCompitino.pdf Soluzioni: 01-2014-PrimoCompitinoSol.pdf
12	11/11/2014	Logica del primo ordine: Proof System	Dispense: [LP1], pag 39-48 Lucidi: Logica_2014_08.pdf, fino a pag. 22	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	13/11/2014	Logica del primo ordine: Proof System (2)	Dispense: [LP1], pag 49-51 Lucidi: Logica_2014_08.pdf, tutti.	Predicato di uguaglianza; Leggi per l'uguaglianza. Regole di inferenza: Generalizzazione e Skolemizzazione; Quantificazione su dominio vuoto: discussione; Leggi valide solo per dominio non vuoto; Esempi di dimostrazione. Esercizi Proposti
14	18/11/2014	Notazione e leggi per insiemi, intervalli e domini	Dispense: [LP2], pag 1-9. Lucidi: Logica_2014_09.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; 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	20/11/2014	Quantificatori funzionali	Dispense: [LP2], fino a pag. 30. Lucidi: Logica_2014_10.pdf.	Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo; Formalizzazione di enunciati; Leggi per quantificatori funzionali; leggi dell'intervallo.
16	25/11/2014	Esercitazione su Dimostrazioni di Validità e Formalizzazione di Enunciati.	Esercizi proposti	Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf
17	27/11/2014	Logica di Hoare: Introduzione	Dispense: [LdH], fino a pag 20. Lucidi: Logica_2014_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	02/12/2014	Triple di Hoare: Regole di inferenza per assegnamento, sequenza e comando condizionale.	Dispense: [LdH], fino a pag 23. Lucidi: Logica_2014_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	04/12/2014	Esercitazione su Triple di Hoare	Esercizi proposti	Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf
20	09/12/2014	Triple di Hoare: Regola per il Comando Iterativo	Dispense: [LdH], fino a pag 27. Lucidi: Logica_2014_13.pdf.	Triple di Hoare: Regola per il Comando Iterativo; Esempi.
21	11/12/2014	Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo	Dispense: [LdH], fino a pag 30. Lucidi: Logica_2014_14.pdf.	Sequenze: sintassi e semantica; Assioma e regola per aggiornamento selettivo; Esercizi su verifica di triple di Hoare.
22	16/12/2014	Esercitazione su Triple di Hoare	Esercizi proposti
23	18/12/2014	Seconda prova di verifica	Ore 14:00 Corso A ==> Aula A Corso B ==> Aula B	Iscrizione obbligatoria alla pagina https://esami.unipi.it/esami/ Possono sostenere la seconda prova intermedia del 18 dicembre 2014 anche gli studenti che sono risultati insufficienti alla prima prova intermedia del 4 novembre 2014 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ì 11-13, Aula A
Orario ricevimento	Cliccare qui