Section outline
-
DOCENTE Filippo Bonchi (filippo.bonchi@unipi.it) Orario Mercoledi 14-16, Aula E e Giovedì 11-13, Aula E Orario ricevimento Giovedi 14-16 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 nello stesso appello oppure in quello successivo.
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).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
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.Links
- Logica per la Programmazione, A.A. 2017/18 [LPP-17]
- Logica per la Programmazione, A.A. 2016/17 [LPP-16]
-
- Introduzione al corso
- Introduzione al Calcolo Proposizionale; Connettivi logici; Proposizioni (formule proposizionali); Formalizzazione di enunciati; Formalizzazione di implicazioni in linguaggio naturale; Tautologie e Contraddizioni.
-
- Dimostrazione di Tautologie
- Tabelle di verità
- Dimostrazioni per sostituzione
- Leggi del Calcolo Proposizionale
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.
-
- Tautologie: dimostrazioni e controesempi
- Sulla sintassi del Calcolo Proposizionale
- Ambiguità, precedenza tra connettivi e parentesi
- Altre Leggi del Calcolo Proposizionale
-
- Dimostrazione di Implicazioni Tautologiche
- 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
-
- Tautologie come schemi di dimostrazione
- Dimostrazioni con ipotesi non tautologiche
Dispense: [LP1], fino a pag 23
-
- Limiti del Calcolo Proposizionale
- Sintassi della Logica del Primo Ordine: Alfabeto, Grammatica, Termini, Formule
- Occorrenze legate e libere di variabili; Formule aperte e chiuse
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.
- Limiti del Calcolo Proposizionale
-
- 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
- Semantica della Logica del Primo Ordine
-
- Modelli
- Formule valide e soddisfacibili
- Conseguenza logica
- Sistemi di dimostrazione
- Correttezza e completezza
- Validità del risultato di una dimostrazione
- Teorema di Deduzione
Dispense: [LP1], pag 39-46
- Modelli
-
- Attenzione: Iscrizione obbligatoria alla pagina https://esami.unipi.it/esami2/
- Per la prova di verifica non si possono portare né dispense né appunti. Si potrà usare solo il foglio tabelle-leggi-v1.pdf che riassume le leggi necessarie.
- Attenzione: Gli studenti devono presentarsi alle 13.45 nell'aula indicata in http://pages.di.unipi.it/corradini/Didattica/LPP-18/01-Allocazione.htm
- Attenzione: Iscrizione obbligatoria alla pagina https://esami.unipi.it/esami2/
-
- Leggi per quantificatori
- Leggi valide solo su dominio non vuoto
- Leggi per quantificatori su dominio
- Formule vacuamente vere/false
- Leggi per quantificatori
-
- Regole di inferenza: Generalizzazione e Skolemizzazione
- Esempi di dimostrazione
- Esempi di formule valide e non valide
Dispense: finita la dispensa [LP1]
-
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
Dispense: [LP2], pag 1-9.
- Notazione intensionale per insiemi, Predicato di Appartenenza, Insieme vuoto
-
- Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo
- Leggi per quantificatori funzionali
- Leggi dell'intervallo
- Formalizzazione di enunciati
Dispense: [LP2], fino a pag. 30.
- Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo
-
- 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
Dispense: [LdH], fino a pag 20.
- Linguaggio imperativo minimo: sintassi con grammatica BNF
-
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.
Dispense: [LdH], fino a pag 23.
- Regole di inferenza pre e post.
-
- Triple di Hoare: Regola per il Comando Iterativo;
- Invarianti;
- Esempi.
Dispense: [LdH], fino a pag 27.
- Triple di Hoare: Regola per il Comando Iterativo;
-
- Sequenze: sintassi e semantica
- Assioma e regola per aggiornamento selettivo
- Esercizi su verifica di triple di Hoare
Dispense: [LdH], fino a pag 30.
- Sequenze: sintassi e semantica
