Topic outline

  • General

  • INFORMAZIONI GENERALI

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

    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


  • 19/09/2018: 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

  • 20/09/2018: 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.

  • 26/09/2018: 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

  • 27/09/2018: Esercitazione su Calcolo Proposizionale

  • 03/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

  • 04/10/2018: Dimostrazioni e Tautologie, Ipotesi non tautologiche

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

    Dispense: [LP1], fino a pag 23


  • 10/10/2018: Esercitazione su Calcolo Proposizionale

  • 11/10/2018: 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.

  • 17/10/2018: Logica del Primo Ordine: Formalizazione e Semantica Informale

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

  • 18/10/2018: 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

  • 24/10/2018: Esercitazione su Formalizzazione e Semantica del primo ordine

  • 25/10/2018: 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


  • 02/11/2018 - Prima prova di verifica

  • 7/11/2018: 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

  • 8/11/2018: 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/2018: Esercitazione su Dimostrazioni di Validità e di Non Validità di Formule

  • 15/11/2018: 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.


  • 21/11/2018: 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.


  • 22/11/2018: Esercitazione su Formalizzazione di Enunciati con Sequenze

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

  • 29/11/2018: 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.

  • 05/12/2018: Esercitazione su Triple di Hoare

  • 06/12/2018: Triple di Hoare: Regola per il Comando Iterativo

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

    Dispense: [LdH], fino a pag 27.

  • 12/12/2018: 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.


  • 13/12/2918: Esercitazione su Triple di Hoare

  • 20/12/2018 - Seconda prova di verifica

  • 23/01/2019 - Primo Appello

  • 11/02/2019 - Secondo Appello

  • 22/06/2019 - Terzo Apello

  • 09/07/2019 - Quarto Appello

    Highlighted
  • O6/09/2019 - Quinto Appello