Logica per la Programmazione - Corsi A e B [LPP-10]

Protesta dell'Università
 
Introduzione al corso

Materiale informativo su Università e sulla protesta a Pisa: https://sites.google.com/site/protestaunipi/home
 
Lucidi: Logica_2010_1.pdf.

Introduzione al corso: La logica da Aristotele alla logica matematica; Logica e informatica; Contenuto del corso.

Calcolo Proposizionale

Lucidi: Logica_2010_2.pdf
Esercizi: Esercizi proposti a lezione

Introduzione al Calcolo Proposizionale: Connettivi logici; Sintassi del Calcolo Proposizionale; Semantica dei connettivi logici con Tabelle di Verità; Formalizzazione di enunciati dichiarativi; Tautologie e Contraddizioni.

Dimostrazioni di Tautologie

Dispense: [LP1], fino a pag 11, escluso Modus Ponens
Lucidi: Logica_2010_3.pdf
Esercizi: Esercizi proposti a lezione

Dimostrazioni di equivalenze; Principio di Sostituzione; Concetto di Legge del Calcolo Proposizionale; Leggi per Equivalenza, Congiunzione, Disgiunzione, Negazione, Implicazione; Esempi di dimostrazioni; Leggi di Assorbimento e Complemento; Insiemi Funzionalmente Completi di Connettivi Logici.

Dimostrazioni di Implicazioni Tautologiche

Dispense: [LP1], fino a pag 18
Lucidi: Logica_2010_4.pdf
Esercizi: Esercizi proposti a lezione

Ambiguità della sintassi del Calcolo Proposizionale; Precedenza tra i connettivi logici; Dimostrazioni di implicazioni; Occorrenze positive e negative; Principio di Sostituzione per l'Implicazione; Altre tecniche di dimostrazione; Forma normale congiuntiva e disgiuntiva; Il Principio di Risoluzione.

Dimostrazioni con Ipotesi non Tautologiche

Dispense: [LP1], fino a pag 24, Sezione 7 esclusa
Lucidi: Logica_2010_5.pdf
Esercizi: Esercizi proposti a lezione

Formalizzazione di dimostrazioni: tautologie corrispondenti a uno o più passi di dimostrazione; Uso di ipotesi come giustificazione; Esempi vari; Altre tecniche di dimostrazione: esempi di dimostrazione per assurdo e per casi.

Esercitazione

Esercizi proposti: Eserciztazione_2010_1.pdf

Svolgimento di alcuni esercizi su formalizzazione di enunciati, occorrenze positive e negative, dimostrazione di tautologie.

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

Esercitazione

Dispense: [LP1], Sezione 8.2 [pag 32-33] Esercizi proposti: Esercitazione_2010_2.pdf

Svolgimento di alcuni esercizi su formalizzazione di enunciati con la logica del primo ordine.

Corsi A e B:
LP1- Semantica
Solo Corso B:
Il Calcolo del Primo Ordine

Corsi A e B: Lucidi: Logica_2010_7.pdf
Dispense: [LP1], pag 36-39.
Solo Corso B: Lucidi: Logica_2010_8.pdf [fino a lucido 14]
Dispense: [LP1], pag 40-47 [fino a legge (eliminazione-forall).

Corsi A e B: Semantica del Calcolo del Primo Ordine: Semantica di termini chiusi e aperti; Assegnamenti; Semantica di formule per induzione strutturale; Esempi; Modelli; Formule valide, soddisfacibili, insoddisfacibili; Conseguenza logica.
Solo Corso A: Esercizi su formalizzazione: Relazioni binarie; Proprietà di Relazioni: funzionali, totali, iniettive, surgettive.
Solo Corso B: Sistemi di dimostrazione; Correttezza e completezza; Validità del risultato di una dimostrazione; Teorema di Deduzione; Leggi per quantificatori: Eliminazione della quantificazione universale.

Il Calcolo del Primo Ordine

Lucidi: Logica_2010_8.pdf [fino a lucido 19]
Dispense: [LP1], fino a pag 48.

Sistemi di dimostrazione; Correttezza e completezza; Validità del risultato di una dimostrazione; Teorema di Deduzione; Leggi per quantificatori.
Solo Corso B: Esercizi su formalizzazione di insiemi e di relazioni.

Il Calcolo del Primo Ordine

Lucidi: Logica_2010_8.pdf, tutto.
Dispense: [LP1], fino a pag 51.
Esercizi: Esercizi proposti

Predicato di uguaglianza; Leggi per l'uguaglianza; Regole di inferenza per quantificatori: Generalizzazione e Skolemizzazione. Esercizi vari.

Lezione annullata causa occupazione

Notazione e leggi per insiemi, intervalli e domini

Lucidi: Logica_2010_9.pdf, fino a pag 15.
Dispense: [LP2], pag 1-7.
Esercizi: Esercizi proposti

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.

Primo compitino

Testo con soluzioni: 01-2010-PrimoCompitino-Soluzioni.pdf.

Leggi di intervallo, Quantificatori funzionali

Lucidi: Logica_2010_9.pdf, tutto.
Logica_2010_10.pdf, fino a pag. 5.
Dispense: [LP2], pag 8-12.

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

Formalizzazione di enunciati e leggi per quantificatori funzionali

Lucidi:
Logica_2010_10.pdf, tutto.
Dispense: [LP2], pag 13-31.

Quantificatori funzionali: formalizzazione di enunciati, leggi generali e leggi specifiche, leggi dell'intervallo; Esempi di dimostrazione.

Logica di Hoare: Introduzione

Lucidi:
Logica_2010_11.pdf, fino a pag. 13.
Dispense: [LdH], fino a pag 17.

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.

Triple di Hoare: definizioni e regole di inferenza

Lucidi:
Logica_2010_11.pdf, fino a pag. 21.
Dispense: [LdH], fino a pag 22.

Interpretazione di triple di Hoare: semantica, correttezza, specifica. 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. Solo corso B: Regola per comando condizionale.

Triple di Hoare: regole di inferenza ed esempi

Lucidi:
Logica_2010_11.pdf, tutti,
Logica_2010_12.pdf Corso A: fino a pag 6; Corso B: fino a pag 9.
Dispense: [LdH], fino a pag 25.

Regole di inferenza per le Triple di Hoare, compreso Regola per il Condizionale e Regola per il Comando Iterativo; Esempi di verifica di Triple di Hoare.

Triple di Hoare: Comando condizionale, Sequenze

Lucidi:
Logica_2010_12.pdf Corso A: fino a pag 13; Corso B: fino a pag 9.
Dispense: [LdH], Corso A: fino a pag 33; Corso B: fino a pag 28.

Esempi di verifica di Triple di Hoare, in particolare di Comandi Iterativi; [Corso A] Sequenze: sintassi, semantica e regola per aggiornamento selettivo. Programmi annotati.

Triple di Hoare: Comando condizionale, Sequenze

Lucidi:
Logica_2010_12.pdf fino a pag 15.
Dispense: [LdH], fino a pag 38.

Ricapitolazione su Sequenze: sintassi, semantica e regola per aggiornamento selettivo. Programmi annotati. Esempi di programmi annotati e di dimostrazione di poprietà di invarianza.

Esercizi su Triple di Hoare e su formalizzazione

Lucidi:
Logica_2010_12.pdf tutti.
Dispense: [LdH], fino a pag 38.

Esercizi ed esempi su Triple di Hoare: numero di elementi positivi di una sequenza, incremento di una sequenza, fattoriale, MCD. Esercizi di formalizzazione con sequenze.

Esercizi di ricapitolazione

Lucidi:
Logica_2010_13.pdf.

Esercizi ed esempi su Triple di Hoare, formalizzazione di enunciati, dimostrazioni del primo ordine.

Esercitazione per secondo compitino

Testo esercizi:
Pre-SecondoCompitino.pdf. Soluzioni proposte:
Soluzioni_Pre_II_Compitino.pdf.