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


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

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

Testi delle prove (con alcune 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

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
19/09/2017
Introduzione al corso
Introduzione al Calcolo Proposizionale
Dispense: [LP1], pag 6--8

Lucidi: LPP_2017_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/2017
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_2017_02.pdf

  • Dimostrazione di Tautologie
    • Tabelle di verità
    • Dimostrazioni per sostituzione
    • Leggi del Calcolo Proposizionale
3
26/09/2017
Dimostrazione di Tautologie e Sintassi del Calcolo Proposizionale Dispense: [LP1], fino a pag 12

Lucidi: LPP_2017_03.pdf

  • Tautologie: dimostrazioni e controesempi
  • Sulla sintassi del Calcolo Proposizionale
  • Ambiguità, precedenza tra connettivi e parentesi
  • Altre Leggi del Calcolo Proposizionale
4
28/9/2017
Aule
A + E

Esercitazione su Calcolo Proposizionale

Esercizi proposti

Tabella di leggi: tabelle-leggi-v1.pdf

5
3/10/2017
Dimostrazione di Implicazioni Tautologiche Dispense: [LP1], fino a pag 18

Lucidi: LPP_2017_04.pdf

  • 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
6
5/10/2017

Dimostrazioni e Tautologie, Ipotesi non tautologiche

Dispense: [LP1], fino a pag 23

Lucidi: LPP_2017_05.pdf

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

7
10/10/2017

Esercitazione su Calcolo Proposizionale

Esercizi proposti

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

8
12/10/2017

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_2017_06.pdf.

  • 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

17/10/2017

Logica del Primo Ordine: Formalizzazione e Semantica

Dispense: [LP1], pag 33-35

Lucidi: LPP_2017_07.pdf fino a pag. 134.

  • 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
    • Semantica di formule per induzione strutturale

10

19/10/2017

Logica del Primo Ordine: Semantica

Dispense: [LP1], pag 36-38

Lucidi: LPP_2017_07.pdf

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

11
24/10/2017

Esercitazione su Formalizzazione e Semantica del primo ordine

Esercizi proposti

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

12

26/10/2017

Logica del Primo Ordine: Proof System

Dispense: [LP1], pag 39-46

Lucidi: LPP_2017_08.pdf

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

--

2/11/2017

Prima prova di verifica

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

13

7/11/2017

Logica del Primo Ordine: Proof System (2)

Dispense: [LP1], pag 47-51

Lucidi: LPP_2017_09.pdf, fino a pag. 14.

  • Leggi per quantificatori
  • Leggi valide solo su dominio non vuoto
  • Leggi per quantificatori su dominio
  • Formule vacuamente vere/false
  • Predicato di uguaglianza; Leggi per l'uguaglianza
  • Esempi di dimostrazioni

14

9/11/2017

Logica del Primo Ordine: Proof System (3)

Dispense: [LP1], pag 47-51

Lucidi: LPP_2017_09.pdf, tutti.

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

15
14/11/2017

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

16/11/2017

Notazione e leggi per insiemi, intervalli e domini

Dispense: [LP2], pag 1-9.

Lucidi: LPP_2017_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

21/11/2017

Quantificatori funzionali

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

Lucidi: LPP_2017_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

23/11/2017

Esercitazione su Formalizzazione di Enunciati con Sequenze.

Esercizi proposti

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

19

28/11/2017

Logica di Hoare: Introduzione

Dispense: [LdH], fino a pag 20.

Lucidi: LPP_2017_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

20

30/11/2017

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

Dispense: [LdH], fino a pag 23.

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

21

05/12/2017

Esercitazione su Triple di Hoare

Esercizi proposti

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

22

07/12/2017

Triple di Hoare:
Regola per il Comando Iterativo

Dispense: [LdH], fino a pag 27.

Lucidi: LPP_2017_14.pdf.

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

23

12/12/2017

Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo

Dispense: [LdH], fino a pag 30.

Lucidi: LPP_2017_15.pdf.

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

24

14/12/2017

Esercitazione su Triple di Hoare

Esercizi proposti

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

--

21/12/2017
ore 9-11

Seconda prova di verifica

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

Iscrizione obbligatoria alla pagina https://esami.unipi.it/esami2/
La seconda prova intermedia del 21 dicembre 2017 è riservata agli studenti che hanno avuto almeno 16 alla prima prova intermedia del 2 novembre 2017.

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.

Links