Weekly outline

  • General

  • Appello Gennaio 2022

    • Quiz icon
      PreTest-TripleHoare-1-2022 Quiz
      Not available unless: You belong to Iscritti Appello Gennaio 2022
  • MODALITA' D'ESAME A DISTANZA

    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. 



  • INFORMAZIONI GENERALI

    DOCENTEFilippo Bonchi (filippo.bonchi@unipi.it)
     Orario Mercoledi 14-16, Aula E e Giovedì 11-13, Aula E
    Orario ricevimento
    Mercoledi 16-18
    CounselingLunedì 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)

    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

    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 pagePlease contact the lecturer if you need to take the exam in English.


    Links


  • 18/09/2019: Introduzione al corso e al Calcolo Proposizionale

    • Introduzione al corso
    • Introduzione al Calcolo Proposizionale; Connettivi logici; Proposizioni (formule proposizionali); Formalizzazione di enunciati; Formalizzazione di implicazioni in linguaggio naturale; Tautologie e Contraddizioni.
    Dispense: [LP1], pag 5--8

  • 19/09/2019: Dimostrazione di Tautologie

    • 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.

  • 25/09/2019: Dimostrazione di Tautologie e Sintassi del Calcolo Proposizionale

    • Tautologie: dimostrazioni e controesempi
    • Sulla sintassi del Calcolo Proposizionale
    • Ambiguità, precedenza tra connettivi e parentesi
    • Altre Leggi del Calcolo Proposizionale
    Dispense: [LP1], fino a pag 12

  • 26/09/2019: Esercitazione su 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

  • 02/10/2018: Dimostrazioni di Implicazioni Tautologiche

    • Dimostrazione di Implicazioni Tautologiche
    1. Principio di sostituzione per l’implicazione
    2. Occorrenze positive e negative
    3. Altre tecniche di dimostrazione
    4. Forme Normali e Principio di Risoluzione

    • Insiemi funzionalmente completi di connettivi
    Dispense: [LP1], fino a pag 18

  • 03/10/2019: Dimostrazioni e Tautologie, Ipotesi non tautologiche

    • Tautologie come schemi di dimostrazione
    • Dimostrazioni con ipotesi non tautologiche

    Dispense: [LP1], fino a pag 23


  • 9/10/2019: Esercitazione su Calcolo Proposizionale

    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

  • 10/10/2019: Logica del Primo Ordine: Motivazioni e Sintassi.

    • 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.

  • 16/10/2019: Logica del Primo Ordine: Formalizazione e Semantica Informale

    • Interpretazione di un linguaggio del primo ordine
    • Formalizzazione di enunciati: linee guida ed esempi

  • 17/10/2019: Logica del Primo Ordine: Semantica Formale.

    • Semantica della Logica del Primo Ordine
      • Assegnamenti
      • Semantica dei termini per induzione strutturale 
      • Esempi
      • Semantica di formule per induzione strutturale

  • 23/10/2019: Esercitazione su Formalizzazione e Semantica 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

  • 24/10/2019: Logica del Primo Ordine: Proof System

    • 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


  • 30/10/2019: Logica del Primo Ordine: Proof System (2)

    • Leggi per quantificatori
    • Leggi valide solo su dominio non vuoto
    • Leggi per quantificatori su dominio
    • Formule vacuamente vere/false

  • 31/10/2019: Simulazione Prima Prova di Verifica

    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

  • 07/11/2019 - Prima prova di verifica

    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.

  • 13/11/2019: Logica del Primo Ordine: Proof System (3)

    • Regole di inferenza: Generalizzazione e Skolemizzazione
    • Esempi di dimostrazione
    • Esempi di formule valide e non valide

    Dispense: finita la dispensa [LP1]


  • 14/11/2019: Notazione e leggi per insiemi, intervalli e domini

    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.


  • 20/11/2019: Quantificatori funzionali

    • 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.


  • 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

  • 28/11/2018: Logica di Hoare: Introduzione

    • 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. 

  • 27/11/2019: Triple di Hoare: Regole di inferenza per assegnamento, sequenza e comando condizionale.

    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.

  • 04/12/2019: Esercitazione su Triple di Hoare

    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

  • 05/12/2019: Triple di Hoare: Regola per il Comando Iterativo

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

    Dispense: [LdH], fino a pag 27.

  • 11/12/2019: Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo

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

    Dispense: [LdH], fino a pag 30.


  • 12/12/2019: Esercitazione su Triple di Hoare

  • 20/12/2019 - Seconda prova di verifica

  • 10/01/2020 - Primo Appello

  • 30/01/2020 - Secondo Appello