Logica per la Programmazione - Corso A [LPP-A-16]


DOCENTE Andrea Corradini <andrea@di.unipi.it>
Orario Martedì 14-16, Aula A e Giovedì 11-13, Aula A
Orario ricevimento Mercoledì 15-18, Studio 357, Dipartimento di Informatica

Informazioni utili e Avvisi


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 solo in un appello della stessa sessione di esami.
Il superamento delle prove di verifica intermedie al posto dello scritto vale solo per la sessione invernale (appelli di gennaio e febbraio).

Testi delle prove (con alcune soluzioni)

Risultati


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

Tabella delle lezioni

N.

DATA

TITOLO

RIFERIMENTI

ARGOMENTI

1
10/09/2016
Introduzione al corso
Introduzione al Calcolo Proposizionale
Dispense: [LP1], pag 6--8

Lucidi: LPP_2016_01.pdf

  • Introduzione al corso
  • Introduzione al Calcolo Proposizionale; Connettivi logici; Proposizioni (formule proposizionali); Formalizzazione di enunciati; Formalizzazione di implicazioni in linguaggio naturale; Tautologie e Contraddizioni.
2
22/09/2016
Dimostrazione di Tautologie 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.

Lucidi: LPP_2016_02.pdf

  • Dimostrazione di Tautologie
    • Tabelle di verità
    • Dimostrazioni per sostituzione
    • Leggi del Calcolo Proposizionale
  • Insiemi funzionalmente completi di connettivi
3
27/09/2016
Dimostrazione di Tautologie e Sintassi del Calcolo Proposizionale Dispense: [LP1], fino a pag 12

Lucidi: LPP_2016_03.pdf

  • Tautologie: dimostrazioni e controesempi
  • Sulla sintassi del Calcolo Proposizionale
  • Ambiguità precedenza tra connettivi e parentesi
  • Altre Leggi del Calcolo Proposizionale
4
29/9/2016
Dimostrazione di Implicazioni Tautologiche Dispense: [LP1], fino a pag 18

Lucidi: LPP_2016_04.pdf

  • Principio di sostituzione per l’implicazione
  • Occorrenze positive e negative
  • Altre tecniche di dimostrazione
  • Forme Normali e Principio di Risoluzione
5
4/10/2015

Esercitazione su Calcolo Proposizionale

Esercizi proposti

Tabella di leggi (utilizzabile durante il primo compitino): tabelle-leggi-v1.pdf

6
6/10/2016

Dimostrazioni e Tautologie, Ipotesi non tautologiche

Dispense: [LP1], fino a pag 23

Lucidi: LPP_2016_05.pdf

  • Inferenze corrette come tautologie
  • Tautologie come schemi di dimostrazione
  • Dimostrazioni con ipotesi non tautologiche

7
11/10/2016

Esercitazione su Calcolo Proposizionale

Esercizi proposti

Tabella di leggi (utilizzabile durante il primo compitino): tabelle-leggi-v1.pdf
Attenzione: Gli studenti sono invitati a continuare autonomamente la risoluzione degli esercizi proposti e non svolti durante l'esercitazione. Nel caso di dubbi o per correggere le soluzioni rivolgersi al docente.

8
13/10/2016

Logica del Primo Ordine: Motivazioni, Sintassi e Interpretazioni.

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.

Lucidi: LPP_2016_06.pdf, fino a pag. 112.

  • Limiti del Calcolo Proposizionale
  • Sintassi della Logica del Primo Ordine: Alfabeto, Grammatica, Termini, Formule
  • Occorrenze legate e libere di variabili; Formule aperte e chiuse

9

18/10/2016

Logica del Primo Ordine: Formalizzazione e Semantica

Dispense: [LP1], pag 36-38

Lucidi: LPP_2016_07.pdf fino a pag. 132.

  • 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

10

20/10/2016

Logica del Primo Ordine: Semantica

Dispense: [LP1], pag 36-38

Lucidi: LPP_2016_07.pdf, tutte

  • Semantica di formule per induzione strutturale
  • Esempi
  • Esercizi su semantica di formule del primo ordine e Formalizzazione di enunciati

11

25/10/2016

Esercitazione su Formalizzazione e Semantica del primo ordine

Esercizi proposti

Tabelle con leggi del calcolo proposizionale (e semantica della Logica dei Predicati): tabelle-leggi-v1.pdf

12

27/10/2016

Logica del Primo Ordine: Proof System

Dispense: [LP1], pag 39-46

Lucidi: LPP_2016_08.pdf

  • Modelli
  • Formule valide e soddisfacibili
  • Conseguenza logica
  • Sistemi di dimostrazione
  • Correttezza e completezza
  • Validità del risultato di una dimostrazione
  • Teorema di Deduzione

--

3/11/2016

Prima prova di verifica

Testo: 01-2016-PrimoCompitino.pdf
Soluzioni: 01-2016-PrimoCompitinoSol.pdf

13

8/11/2016

Logica del Primo Ordine: Proof System (2)

Dispense: [LP1], pag 47-51

Lucidi: LPP_2016_09.pdf

  • Leggi per quantificatori
  • Leggi valide solo su dominio non vuoto
  • Quantificazione su dominio vuoto: discussione
  • Predicato di uguaglianza; Leggi per l'uguaglianza
  • Regole di inferenza: Generalizzazione e Skolemizzazione
  • Esempi di dimostrazione

14

10/11/2016

Leggi per quantificazione su dominio
Esercizi vari su logica del primo ordine

Dispense: [LP1], pag 47-51

Lucidi: LPP_2016_09.pdf

  • Leggi per quantificatori su dominio.

15
15/11/2016

Esercitazione su Dimostrazioni di Validità e di Non Validità di Formule.

Esercizi proposti

Tabella di leggi (utilizzabile durante il secondo compitino): tabelle-leggi-v3.pdf

16

17/11/2016

Notazione e leggi per insiemi, intervalli e domini

Dispense: [LP2], pag 1-9.

Lucidi: LPP_2016_10.pdf.

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

17

22/11/2016

Quantificatori funzionali

Dispense: [LP2], fino a pag. 30.

Lucidi: LPP_2016_11.pdf.

  • Quantificatori funzionali: sintassi e significato intuitivo di sommatoria, cardinalità, minimo e massimo
  • Leggi per quantificatori funzionali
  • Leggi dell'intervallo
  • Formalizzazione di enunciati

18

24/11/2016

Logica di Hoare: Introduzione

Dispense: [LdH], fino a pag 20.

Lucidi: LPP_2016_12.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

19

29/12/2016

Triple di Hoare: Regole di inferenza per assegnamento, sequenza e comando condizionale.

Dispense: [LdH], fino a pag 23.

Lucidi: LPP_2016_13.pdf.

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.

20

01/12/2016

Esercitazione su Formalizzazione di Enunciati con Sequenze e Triple di Hoare

Esercizi proposti

Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf

21

06/12/2016

Triple di Hoare:
Regola per il Comando Iterativo

Dispense: [LdH], fino a pag 27.

Lucidi: LPP_2016_14.pdf.

  • Triple di Hoare: Regola per il Comando Iterativo
  • Esempi

22

13/12/2016

Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo

Dispense: [LdH], fino a pag 30.

Lucidi: LPP_2016_15.pdf.

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

23

15/12/2016

Esercitazione su Triple di Hoare

Esercizi proposti

Tabella con leggi e regole di inferenza: tabelle-leggi-v3.pdf

--

22/12/2016
ore 9-11

Seconda prova di verifica

Testo: 02-2016-SecondoCompitino.pdf
Soluzioni:
02-2016-SecondoCompitinoSol.pdf

Iscrizione obbligatoria alla pagina https://esami.unipi.it/esami2/
La seconda prova intermedia del 22 dicembre 2016 è riservata agli studenti che hanno avuto almeno 16 alla prima prova intermedia del 3 novembre 2016. Gli studenti che hanno avuto "insufficiente" possono comunque sostenere la prova come esercitazione, iscrivendosi alla pagina indicata sopra, ma il loro elaborato non verrà corretto.

Per la prova di verifica non si possono portare né dispense né appunti. Si potrà usare solo il foglio tabelle-leggi-v3.pdf che riassume le leggi necessarie.