Weekly outline

  • 6 Luglio 2020: Quarto Appello

    Tutti gli studenti iscritti all'appello devono essere alle ore 9h30 sul canale Google Meet https://meet.google.com/onu-wwrg-edq

    Gli orali si terranno all'indirizzo https://meet.google.com/nfq-gyzk-jrt

    Lavagna vituale: https://miro.com/welcomeonboard/udHuGCiO2Cj7gyKo6GLUWDPf9ACzbsd2vlbJx76Z7FBoPCr1mVyKXKHiwb7AVEtZ

    •  PreTest-CalcoloProposizionale-07-2020 Quiz
      Restricted Not available unless: You belong to Iscritti Appello Luglio
    •  PreTest-LogicaPrimoOrdine-07-2020 Quiz
      Restricted Not available unless: You belong to Iscritti Appello Luglio
    •  PreTest-TripleHoare-07-2020 Quiz
      Restricted Not available unless: You belong to Iscritti Appello Luglio
  • 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 tre quiz: uno per il Calcolo Proposizionale, uno per la Logica del Primo Ordine ed uno per le triple di Hoare. I quiz sono da considerarsi come delle vere e proprie simulazioni del pretest: infatti questi hanno la stessa durata e le stesse tipologie di domande del pretest. Invece, i punteggi della simulazione non rispecchiano quelli del pretest finale. I tre 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

    • 10/01/2020 - Primo Appello

    • 30/01/2020 - Secondo Appello