DOCENTE | Andrea Corradini <andrea@di.unipi.it> |
Orario | Martedì 14-16, Aula A e Giovedì 11-13, Aula A |
Orario ricevimento | Cliccare qui |
N. |
DATA |
TITOLO |
RIFERIMENTI |
ARGOMENTI |
1 |
08/10/2013 |
Introduzione al corso |
Lucidi: Logica_2013_1.pdf Logica_2013_2.pdf fino a pag. 11 |
|
2 |
10/10/2013 |
Dimostrazione di Tautologie |
Dispensa: [LP1] fino a pag 11.
|
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
|
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 |
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 |
|
|
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]
|
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. |
|
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 |
|
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
|
|
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
|
Per la prova di verifica è obbligatorio iscriversi, accedendo alla pagina http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/ Attenzione:
|
10 |
12/11/2013 |
Logica del primo ordine: Proof System |
Dispense: [LP1], pag 39-48 |
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
|
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. |
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. |
13 |
26/11/2013 |
Quantificatori funzionali |
Lucidi: Logica_2013_10.pdf.
|
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.
|
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: |
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 |
|
17 |
10/12/2013 |
Triple di Hoare:
|
Lucidi:
|
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/. |
18 |
12/12/2013 |
Triple di Hoare: Sequenze (Array) e Aggiornamento Selettivo |
Lucidi:
|
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 |
|
|
20 |
19/12/2013 |
Seconda prova di verifica e Appello Straordinario |
Testo: 02-2013-SecondoCompitino.pdf
|
Per la prova di verifica è obbligatorio iscriversi, accedendo alla pagina http://compass2.di.unipi.it/didattica/inf31/share/orario/Appelli/ Attenzione:
|