Section outline
-
-
PreTest-TripleHoare-1-2022 Quiz
-
-
A causa dell'emergenza COVID, le modalità di esame del corso di Logica per la Programmazione vengono modificate in modo da permette agli studenti di sostenere l'esame a distanza.
La modalità d'esame a distanza prevede una prova orale a cui si accede superando un pretest.
- La prova orale consiste in un colloquio tra studente e docente volto a valutare la comprensione di tutti gli argomenti affrontati durante il corso. Questi includono anche quegli esercizi della prova scritta della vecchia modalità d'esame, come ad esempio la formalizzazione, la Skolemizzazione e la verifica di correttezza delle triple di Hoare.
- Il pretest ha la finalità di accertare le conoscenze di base degli studenti ed alcune elementari capacità deduttive. Il pretest consiste di tre parti che gli studenti dovranno risolvere in modo sequenziale: prima il Calcolo Proposizionale, poi Logica del Primo Ordine ed infine le Triple di Hoare. Ogni parte consiste di 4 domande da risolvere in 20 minuti.
Gli studenti possono trovare tutte le disposizioni logistiche di prova orale e pretest nella pagina "Organizzazione Logistica per la modalità d'esame a distanza".
- Simulazione del pretest. Al fine di aiutare gli studenti a superare il pretest, i docenti hanno preparato alcuni quiz: due per il Calcolo Proposizionale, due per la Logica del Primo Ordine e due per le triple di Hoare. I quiz sono da considerarsi come delle simulazioni del pretest: infatti questi hanno durata e domande simili a quell del pretest. Invece, i punteggi della simulazione non rispecchiano quelli del pretest finale. I quiz sono disponibili alla fine della pagina. Ogni quiz può essere ripetuto più volte.
- Svolgimento per Triple di Hoare. Le domande concernenti Calcolo Proposizionale e Logica del Primo Ordine sono analoghe a quelle previste dalla vecchia modalità d'esame. Per quanto riguarda le Triple di Hoare invece l'enfasi non è concentrata sul sistema di dimostrazione, come lo era nella vecchia modalità d'esame, ma piuttosto sulle nozioni di base, come ad esempio la semantica del linguaggio imperativo, il predicato def e la nozione di tripla soddisfatta. I docenti, preoccupati dal fatto che alcuni studenti possano trovarsi disorientati, hanno preparato delle note, disponibili alla fine della pagina, che mostrano la risoluzione delle varie tipologie di esercizi sulle triple.
-
DOCENTE Filippo Bonchi (filippo.bonchi@unipi.it) Orario Mercoledi 14-16, Aula E e Giovedì 11-13, Aula E Orario ricevimento Mercoledi 16-18 Counseling Lunedì e Giovedì 16-17:30 (Dipartimento di Informatica) 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. 2018/19 [LPP-18]
- 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
-
Data 02/10/2018 Titolo Dimostrazione di Implicazioni Tautologiche Argomenti - 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
Materiale didattico - [LP1] fino a pag. 18
Lucidi LPP-2018-04.pdf -
- 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
-
Data 11/10/2018 Titolo Logica del Primo Ordine: Motivazioni e Sintassi Argomenti - Limiti del Calcolo Proposizionale
- Sintassi della Logica del Primo Ordine: Alfabeto, Grammatica, Termini, Formule
- Occorrenze legate e libere di variabili; Formule aperte e chiuse
Materiale didattico - [LP1], Sezioni 8 e 8.1 [pag 29-33]
- [LMB-INF], Capitolo 4, "Logica dei Predicati", pag 50-53.
Lucidi LPP-2018-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
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
-
Data 25/10/2018 Titolo Logica del Primo Ordine: Proof System Argomenti - Modelli
- Formule valide e soddisfacibili
- Conseguenza logica
- Sistemi di dimostrazione
- Correttezza e completezza
- Validità del risultato di una dimostrazione
- Teorema di Deduzione
- Esercizi su semantica di formule del primo ordine Interpretazione di un linguaggio del primo ordine
Materiale didattico - [LP1], pag 40-47
Lucidi LPP-2018-09.pdf -
- 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
-
- Leggi per quantificatori
- Leggi valide solo su dominio non vuoto
- Leggi per quantificatori su dominio
- Formule vacuamente vere/false
- Leggi per quantificatori
-
Data 08/11/2018 Titolo Logica del Primo Ordine: Proof System (3) Argomenti - Linguaggio del Primo Ordine con Uguaglianza
- Regole di inferenza: Generalizzazione e Skolemizzazione
- Esempi di dimostrazioni con Skolemizzazione
- Esempio: formalizzare (non) continuità di una funzione sui reali
Materiale didattico - [LP1], pag 49-51
Lucidi LPP-2018-11.pdf -
Gli studenti sono invitati a continuare a svolgere a casa gli esercizi che non hanno completato in aula, e a confrontare le proprie soluzioni con quelle proposte dal docente.
Per l'esercitazione si può usare la tabella delle leggi tabelle-leggi-v3.pdf, che sarà utilizzabile anche durante la seconda prova in itinere.
-
- 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
-
20/11/2019: Esercitazione su Dimostrazioni di (Non) Validità di Formule e Formalizzazione di Enunciati con array
Data 27/11/2018 Titolo Logica di Hoare: Introduzione Argomenti - 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
Materiale didattico - [LdH], fino a pag 16.
Lucidi LPP-2018-14.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
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.
-
Data 11/12/2018 Titolo Triple di Hoare: Sequenze e Aggiornamento Selettivo Argomenti - Sequenze: sintassi e semantica
- Assioma e regola per aggiornamento selettivo
- Esercizi su verifica di triple di Hoare
Materiale didattico - [LdH], fino a pag 30
Lucidi LPP-2018-17.pdf -
- 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
