Indice degli argomenti

  • Introduzione

  • INFORMAZIONI GENERALI

    DOCENTE Andrea Corradini <andrea@di.unipi.it>
    Orario Martedì 14-16, Aula E e Giovedì 14-16, Aula E
    Orario ricevimento Cliccare qui.

    Avvisi

    • [10 settembre 2019] Gli orali del quinto appello si terranno Mercoledi' 11 settembre a partire dalle 9:00 in aula A1.
    • [24 giugno 2019] Ho pubblicato testo (con soluzioni) del terzo appello, e i risultati del terzo appello. Gli orali si terranno Giovedì 27 giugno alle 14:30 in Aula C1.
    • [20 maggio 2019] Sono state fissate le date del terzo e quarto appello di LPP come segue (l'iscrizione sul portale Esami dovrebbe essere attivata tra pochissimo):
      • terzo appello: Sabato 22 giugno ore 10-12
      • quarto appello: Martedì 9 luglio ore 11-13
    • [17 maggio 2019] Attenzione: a causa di un disguido non sono ancora state fissate le date degli appelli della sessione estiva di LPP. Verranno pubblicati lunedì 20 o al più tardi martedì 21 maggio. Mi scuso con tutti per l'inconveniente.
    • Alla pagina http://pages.di.unipi.it/corradini/Didattica/LPP-18/04-LPP-aule.htm  trovate l'indicazione dell'aula in cui recarvi per il secondo appello dell'11 febbraio 2019 alle ore 14:00. Presentarsi nell'aula indicata alle ore 13:45. 
    • ORALI: Gli studenti che hanno superato i compitini e devono sostenere l'orale non devono iscriversi agli scritti successivi. Basta che si presentino per l'orale nella data che pubblichero' e che comunichero' per email a tutti gli interessati.
    • I prossimi orali si terranno Martedi' 15 gennaio mattina in aula A1 e Mercoledi' 16 gennaio, mattina e pomeriggio, in aula N1.
    • Alla pagina http://pages.di.unipi.it/corradini/Didattica/LPP-18/01-Allocazione.htm  trovate l'indicazione dell'aula in cui recarvi per il compitino di oggi, 2 novembre, alle ore 14:00. Presentarsi nell'aula indicata alle ore 13:45.
      Le aule D3, D4 e D5 sono nell'edificio della segreteria studenti.
    • Ho fissato un ricevimento straordinario Mercoledi' 31 ottobre alle ore 9:30 presso la Sala Riunioni Ovest del Dipartimento di Informatica.
    • il 2 novembre, nella mattinata, verranno pubblicate su questa pagina le istruzioni per il primo compitino del pomeriggio alle 14:00
      Gli studenti sono pregati di recarsi nelle aule che verranno indicate almeno 15 minuti prima.

    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 per l'intera sessione invernale (appelli di gennaio e febbraio).
    Attenzione:
    • possono sostenere l'esame orale solo gli studenti che hanno assolto gli OFA: all'orale è obbligatorio presentare il libretto con il timbro che certifichi tale assolvimento
    • se uno studente viene respinto all'esame orale il voto conseguito allo scritto viene annullato, e dovrà rifare la prova scritta.

    Risultati prove scritte

    Testi di compitini ed esami (alcuni con soluzioni)

    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

    Registrazioni delle lezioni di LPP, Anno accademico 2015/16

    Sono disponibil le registrazioni delle lezioni dell'anno 2015/16. Alcuni contenuti possono essere cambiati nel corso degli anni. Le registrazioni sono accessibili alla URL <http://owncloud-usid.unipi.it/index.php/s/G8vYwNWZqrTSIxa>. Per la passwd rivolgersi al docente. Di alcune lezioni potrebbe mancare l'audio: richiederlo per email al docente.

    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

    • 18/09/2018 - Introduzione al corso e al Calcolo Proposizionale

      Titolo Introduzione
      Argomenti
      • Introduzione al corso
      • Introduzione al Calcolo Proposizionale; Connettivi logici; Proposizioni (formule proposizionali); Formalizzazione di enunciati; Formalizzazione di implicazioni in linguaggio naturale; Tautologie e Contraddizioni.
       Materiale didattico
       Dispense: [LP1] pag 5-8
       Lucidi   LPP-2018-01.pdf
      • 20/09/2018 - Dimostrazione di Tautologie

        Data 20/09/2018
        Titolo Dimostrazione di Tautologie
        Argomenti
        • Tabelle di verità
        • Dimostrazioni per sostituzione
        • Leggi del Calcolo Proposizionale
         Materiale didattico
        • [LP1]  pag 3-10
        • [LMB-INF] Sezione 1.4, "Dimostrazioni per sostituzione", pag 4-7, e sezione 3.2.1, "Interpretare le formule proposizionali", pag. 32-35.
         Lucidi  LPP-2018-02.pdf

        • 25/09/2018 - Dimostrazione di Tautologie e Sintassi del Calcolo Proposizionale

          Data 25/09/2018
          Titolo Dimostrazione di Tautologie e Sintassi del Calcolo Proposizionale
          Argomenti
          • Tautologie: dimostrazioni e controesempi
          • Inferenze in linguaggio naturale e tautologie
          • Sulla sintassi del Calcolo Proposizionale: Ambiguità, precedenza tra connettivi e parentesi
          • Altre Leggi del Calcolo Proposizionale Dimostrazioni per sostituzione
           Materiale didattico
          • [LP1]  fino a pag. 12
           Lucidi  LPP-2018-03.pdf

          • 27/09/2018 - Esercitazione su Calcolo Proposizionale

            Gli studenti sono invitati a continuare a svolgere a casa gli esercizi che non hanno completato in aula.

            All'inizio della prossima settimana (Ottobre 2) verranno pubblicate le soluzioni degli esercizi proposti.

            Per l'esercitazione si può usare la seguente tabella delle leggi, che sarà utilizzabile anche durante la prima prova in itinere.

          • 02/10/2018 - Dimostrazione di Implicazioni Tautologiche

            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

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

              Data 04/10/2018
              Titolo Dimostrazioni e Tautologie, Ipotesi non tautologiche
              Argomenti
              • Tautologie come schemi di dimostrazione
              • Dimostrazioni con ipotesi non tautologiche
               Materiale didattico
              • [LP1]  fino a pag. 23
               Lucidi  LPP-2018-05.pdf

              • 09/10/2018 - Esercitazione su Calcolo Proposizionale

                Gli studenti sono invitati a continuare a svolgere a casa gli esercizi che non hanno completato in aula.

                Le soluzioni degli esercizi proposti verranno pubblicate nei prossimi giorni.

                Per l'esercitazione si può usare la tabella delle leggi tabelle-leggi-v1.pdf, che sarà utilizzabile anche durante la prima prova in itinere.

              • 11/10/2018 - Logica del Primo Ordine: Motivazioni, Sintassi

                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

                • 16/10/2018 - Logica del Primo Ordine: Formalizzazione

                  Data 16/10/2018
                  Titolo Logica del Primo Ordine: Formalizzazione e Semantica
                  Argomenti
                  • Interpretazione di un linguaggio del primo ordine
                  • Formalizzazione di enunciati: linee guida ed esempi
                  • Esempi di semantica di formule di Logica del Primo Ordine
                   Materiale didattico
                  • [LP1], pag 34-37
                   Lucidi  LPP-2018-07.pdf

                  • 18/10/2018 - Logica del Primo Ordine: Semantica

                    Data 18/10/2018
                    Titolo Logica del Primo Ordine: Semantica
                    Argomenti
                    • Semantica di formule per induzione strutturale
                    • Esempi
                    • Esercizi su semantica di formule del primo ordine Interpretazione di un linguaggio del primo ordine
                     Materiale didattico
                    • [LP1], pag 38-40
                     Lucidi  LPP-2018-08.pdf

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

                      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-v1.pdf, che sarà utilizzabile anche durante la prima prova in itinere.

                    • 25/10/2018 - Logica del Primo Ordine: Proof System

                      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

                      • 02/11/2018 - Prima prova di verifica



                        • 06/11/2018 - Logica del Primo Ordine: Proof System (2)

                          Data 06/11/2018
                          Titolo Logica del Primo Ordine: Proof System (2)
                          Argomenti
                          • Leggi per quantificatori
                          • Leggi valide solo su dominio non vuoto
                          • Leggi per quantificatori su dominio
                          • Formule vacuamente vere/false
                          • Esempi di dimostrazioni
                           Materiale didattico
                          • [LP1], pag 47-48
                           Lucidi  LPP-2018-10.pdf

                          • 08/11/2018 - Logica del Primo Ordine: Proof System (3)

                            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

                            • 13/11/2018 - Esercitazione su validità e non validità di formule

                              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.

                            • 15/11/2018 - Notazione e leggi per insiemi, intervalli e domini

                              Data 15/11/2018
                              Titolo Notazione e leggi per insiemi, intervalli e domini
                              Argomenti
                              • 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
                               Materiale didattico
                              • [LP2], pag 1-9
                               Lucidi  LPP-2018-12.pdf

                              • 20/11/2018 - Quantificatori Funzionali

                                Data 20/11/2018
                                Titolo Quantificatori funzionali
                                Argomenti
                                • Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo
                                • Leggi per quantificatori funzionali
                                • Leggi dell'intervallo
                                • Formalizzazione di enunciati
                                 Materiale didattico
                                • [LP2], fino a pag 30
                                 Lucidi  LPP-2018-13.pdf

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

                                  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.

                                • 27/11/2018 - Logica di Hoare: Introduzione

                                  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

                                  • 29/11/2018 - Triple di Hoare: Regole per assegnamento, sequenza e comando condizionale

                                    Data 29/11/2018
                                    Titolo Triple di Hoare: Regole di inferenza per assegnamento, sequenza e comando condizionale
                                    Argomenti
                                    • 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
                                     Materiale didattico
                                    • [LdH], fino a pag 23.
                                     Lucidi  LPP-2018-15.pdf

                                    • 04/12/2018 - Esercitazione su Triple di Hoare

                                      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.

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

                                      Data 6/12/2018
                                      Titolo Triple di Hoare: Regola per il Comando Iterativo
                                      Argomenti
                                      • Triple di Hoare: Regola per il Comando Iterativo
                                      • Esempi
                                       Materiale didattico
                                      • [LdH], fino a pag 27[
                                       Lucidi  LPP-2018-16.pdf

                                      • 11/12/2018 - Triple di Hoare: Sequenze e Aggiornamento Selettivo

                                        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

                                        • 13/12/2018 - Esercitazione su Triple di Hoare

                                          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.


                                        • 20/12/2018 - Seconda Prova di Verifica