Logica per la Programmazione - Corso B [LPP-B-13]


DOCENTE Andrea Corradini <andrea@di.unipi.it>
Orario Martedì 14-16, Aula A e Giovedì 11-13, 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.
Gli studenti che abbiano superato solo una delle prove di verifica intermedie possono recuperare l'altra nel solo appello di gennaio, sostenendola al posto dello scritto. Le prove di verifica intermedie valgono solo per la sessione invernale (appelli di gennaio e febbraio).
In generale, lo scritto superato in un appello consente di sostenere l'orale solo in un appello della stessa sessione di esami.

Testi delle prove (con alcune soluzioni)


Materiale didattico (Dispense, PDF)


Tabella delle lezioni

N.

DATA

TITOLO

RIFERIMENTI

ARGOMENTI

1

08/10/2013

Introduzione al corso
Introduzione al Calcolo Proposizionale

Lucidi: Logica_2013_1.pdf
Logica_2013_2.pdf fino a pag. 11

  • Introduzione al corso
  • Introduzione al Calcolo Proposizionale
    • Connettivi logici; Proposizioni (formule proposizionali); Formalizzazione di enunciati
  • Ore 15:40, Aula A: Presentazione del Prof. Vincenzo Gervasi sui Test d'Ingresso dell'A.A. 2012-13.

2

10/10/2013

Dimostrazione di Tautologie

Dispensa: [LP1] fino a pag 11.
Lucidi: Logica_2013_2.pdf, tutti Logica_2013_3.pdf, fino a pag. 17

Formalizzazione di implicazioni in linguaggio naturale; Tautologie e Contraddizioni; Dimostrazione di tautologie; Interpretazioni; Tabelle di verità; Principio di Sostituzione; Concetto di Legge del Calcolo Proposizionale; Leggi per Equivalenza, Congiunzione, Disgiunzione, Negazione, Implicazione.

3

15/10/2013

Dimostrazione di Equivalenze e di Implicazioni Tautologiche

Dispense: [LP1], fino a pag 15
Lucidi: Logica_2013_3bis.pdf, tutti
Logica_2013_4.pdf, fino a pag. 11
Esercizi: Esercizi proposti

Esempi di dimostrazioni; Leggi di Assorbimento e Complemento; Insiemi Funzionalmente Completi di Connettivi Logici; Ambiguità della sintassi del Calcolo Proposizionale; Precedenza tra i connettivi logici; Dimostrazioni di implicazioni; Occorrenze positive e negative;

4

17/10/2013

Dimostrazione di Implicazioni Tautologiche, Forme normali, Dimostrazioni come Tautologie

Dispense: [LP1], fino a pag 23
Logica_2013_4.pdf tutti
Logica_2013_5.pdf, fino a pag 15.

Principio di Sostituzione per l'Implicazione; Forma normale congiuntiva e disgiuntiva; Il Principio di Risoluzione; Rappresentazione di inferenze e tecniche di dimostrazione come tautologie; Dimostrazioni come tautologie; Dimostrazioni con ipotesi non tautologiche.

5

22/10/2013

Esercitazione su Calcolo Proposizionale


Logica_2013_5.pdf, tutti.
Esercizi proposti
Esercizi proposti con alcune soluzioni

6

24/10/2013

Logica del Primo Ordine: Motivazioni, Sintassi e Interpretazioni

Dispense: [LP1], Sezioni 8 e 8.1 [pag 27-31], 9 e 9.1 [pag 33-35]
Lucidi: Logica_2013_6.pdf

Limiti del Calcolo Proposizionale; Sintassi della Logica del Primo Ordine: Alfabeto, Grammatica, Termini, Formule; Occorrenze legate e libere di varaibili; Formule aperte e chiuse; Interpretazione di un linguaggio del primo ordine; Esempi di interpretazioni; Formalizzazione di enunciati: linee guida ed esempi (solo iniziato).

7

29/10/2013

Formalizzazione di enunciati.
Semantica della logica del prim'ordine


Dispense: [LP1], pag 36-38
Lucidi: Logica_2013_6.pdf, tutti
Lucidi: Logica_2013_7.pdf
Esercizi proposti

Formalizzazione di enunciati: linee guida ed esempi. Semantica della Logica del Primo Ordine: Semantica di termini chiusi e aperti; Assegnamenti; Semantica di formule per induzione strutturale; Esempi;

8

31/10/2013

Esercitazione


Testo: Esercitazione_2013_3.pdf
Tabelle leggi: tabelle-leggi-v1.pdf
Soluzioni proposte dai docenti: Esercitazione_2013_3-SOL.pdf

Attenzione: Giovedi' 31/10: PRL A/B ore 11:00, LPP A/B ore 16:00, nelle solite aule.

05/11/2013

Ricevimento collettivo

Ore 16:00-18:00, Aula A

Ricevimento con discussione esercizi dell'ultima esercitazione
Soluzioni proposte: Esercitazione_2013_3-SOL.pdf

06/11/2013

Ricevimento collettivo

Ore 14:00-16:00, Aula A

9

07/11/2013

Prima prova di verifica e Appello Straordinario

Testo: 01-2013-PrimoCompitino.pdf


Soluzioni: 01-2013-PrimoCompitino-SOL.pdf

Per la prova di verifica è obbligatorio iscriversi, accedendo alla pagina http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/

Attenzione:

  • Per la prova di verifica non si possono portare né dispense né appunti. Si potrà usare solo il foglio tabelle-leggi-v1.pdf, distribuito nell'Esercitazione del 31/10, che riassume le leggi necessarie.

10

12/11/2013

Logica del primo ordine: Proof System

Dispense: [LP1], pag 39-48
Lucidi: Logica_2013_8.pdf fino a pag 22.

Modelli; Formule valide e soddisfacibili; Conseguenza logica; Sistemi di dimostrazione; Correttezza e completezza; Validità del risultato di una dimostrazione; Teorema di Deduzione; Leggi per quantificatori.

11

14/11/2013

Logica del primo ordine: Proof System (2)

Dispense: [LP1], pag 49-51
Lucidi: Logica_2013_8.pdf, tutti.

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

12

19/11/2013

Notazione e leggi per insiemi, intervalli e domini

Dispense: [LP2], pag 1-9.
Lucidi: Logica_2013_9.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; Quantificazione ristretta a un insieme: domini, quantificazione su domini vuoti, estensione di leggi per quantificatori a domini; Leggi dell'intervallo per quantificatori; Definizione di array; Formalizzazione di enunciati su array.

21/11/2013

Lezione annullata a causa sospensione attività didattica per Assemblea


La didattica dei corsi di studio afferenti al dipartimento è sospesa il giorno 21/11/2013 dalle ore 11 alle ore 13 per partecipare all’assemblea di tutte le componenti degli atenei pisani prevista GIOVEDI' 21 NOVEMBRE 2013 alle ore 11.00, e che si terrà nell'Aula Magna del Dipartimento di Scienze Politiche in Via Serafini 3.
L’ Assemblea e’ indetta da indetta da ADI, ADU, ANDU, ARTeD, CIPUR, CISL-Universita', CNRU, CNU, COBAS-Pubblico Impiego, CoNPAss, CSA-CISAL Universita', FLC-CGIL, LINK, RETE29Aprile, SNALS-Docenti, SUN-Universitas News, UDU, UGL-INTESA FP, UIL RUA

13

26/11/2013

Quantificatori funzionali

Lucidi: Logica_2013_10.pdf.
Dispense: [LP2], fino a pag. 30.

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

14

28/11/2013

Logica di Hoare: Introduzione

Lucidi: Logica_2013_11.pdf.
Dispense: [LdH], fino a pag 20.

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. Regole di inferenza: pre e post. Assiomi per skip e assegnamento semplice. Espressioni definite e non.

15

3/12/2013

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

Lucidi:
Logica_2013_12.pdf.

Dispense: [LdH], fino a pag. 23 (escluso sezione 4.7).

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.

16

5/12/2013

Consegna compiti prima verifica corretti

Esercitazione su Logica del Primo Ordine, intervalli e quantificatori funzionali
Esercitazione_2013_4.pdf

17

10/12/2013

Triple di Hoare:
Regola per il Comando Iterativo

Lucidi:
Logica_2013_13.pdf.
Dispense: [LdH]: fino a pag 27

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

10/12/2013

Incontro con i Tutor

Ore 16:00, Aula A

Gli studenti che hanno avuto gravi insufficienze ai primi compitini sono caldamente invitati a intervenire. Le attività dei Tutor sono descritte alla pagina https://sites.google.com/site/infotutorunipi/.
Avviso: Per impegni personali il ricevimento del Prof. Corradini inizierà alle ore 17:00.

18

12/12/2013

Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo

Lucidi:
Logica_2013_14.pdf.
Dispense: [LdH] fino a pagina 30.

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

19

17/12/2013

Esercitazione su Triple di Hoare

 
Testo: Esercitazione_2013_5.pdf
Tabelle leggi: tabelle-leggi-v2.pdf

20

19/12/2013

Seconda prova di verifica e Appello Straordinario

Testo: 02-2013-SecondoCompitino.pdf


Soluzioni: 02-2013-SecondoCompitino-SOL.pdf

Per la prova di verifica è obbligatorio iscriversi, accedendo alla pagina http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/

Attenzione:

  • Per la prova di verifica non si possono portare né dispense né appunti. Si potrà usare solo il foglio tabelle-leggi-v2.pdf (distribuito nell'Esercitazione del 17/12) che riassume le leggi necessarie.
  • In occasione dell'appello di gennaio, gli studenti che abbiano superato una delle due prove di verifica possono recuperare l'altra invece di fare lo scritto su tutto il corso.