Corso Integrato di Linguaggi e Strutture, parte di Linguaggi

Docente: Dott. Claudio Sacerdoti Coen

Informazioni generali:

Orario di ricevimento: ogni lunedi' alle 15:30, salvo avvisi contrari comunicati sul newsgroup.

Newsgroup:

È stato creato il newsgroup unibo.cs.informatica.linguaggi per mantenere il contatto fra gli studenti e con il docente durante il secondo semestre.

Regolamento del corso:

Il corso prevede delle attività da svolgersi in laboratorio utilizzando il dimostratore interattivo di teoremi Matita. Lo studente ha a disposizione due ore per svolgere in laboratorio gli esercizi assegnati loro. Al termine delle due ore avviene la consegna con relativa valutazione. Successivamente lo studente ha a disposizione una settimana per completare o correggere gli esercizi svolti per migliorare il punteggio ottenuto.

I punteggi conseguiti nelle prove di laboratorio concorrono al voto finale. Gli studenti che non prendono parte all'attività in laboratorio debbono sostenere un orale integrativo obbligatorio.

Oltre all'attività in laboratorio e all'eventuale orale integrativo, per superare la parte di Linguaggi è inoltre necessario superare un esame scritto. L'esame scritto si compone di due parti. La prima parte durante, la quale non e' possibile utilizzare appunti, comprende domande di teoria (enunciare definizioni, teoremi, dimostrare semplici teoremi, dimostrare teoremi importanti del corso quali correttezza, completezza e compattezza). La seconda parte chiede invece lo svolgimento di esercizi (p.e. costruire alberi di derivazione, mostrare modelli o contromodelli per formule, sintetizzare forme normali dalle tabelle di verità). Il superamente della prima parte è pre-requisito alla valutazione della seconda.

Esami:

Oltre ai sei appelli canonici (giu-lug, set-ott, gen-feb) sono previsti due appelli straordinari (parziali) a gen-feb. Superare uno dei due appelli parziali è equivalente al superamento di un appello canonico.

Coloro che non hanno seguito (con successo) le prove di laboratorio e che quindi debbono presentarsi all'orale, così come coloro che vogliono sostenere l'orale per cambiare il voto, debbono concordare con il docente una data per l'orale.

Le date degli appelli si trovano sulle pagine del corso di laurea. Per presentarsi a un appello è necessario iscriversi nell'apposito sito.

Valutazioni (esami e laboratorio):

Valutazioni relative all'attività di laboratorio, voti conseguiti nei vari appelli e voto proposto, in formato Gnumeric.

Programma dettagliato del corso:

Mer. 01/10/08, 08:30, aula Cremona

• Il metodo scientifico
• Mondo sensibile e verità
• "Verità" classica e intuizionista e sua dipendenza dal mondo oggetto del discorso
• Linguaggio naturale e sua inaffidabilità
• Linguaggio e metalinguaggio
• Paradossi legati all'uso obliquo dei nomi

Lun. 06/10/08, 13:30, aula Cremona

• Incompatibilità fra metalinguaggio (interprete universale) e terminazione per ogni programma
• Concetto di nome secondo Frege; denotazione vs connotazione
• Principio di invarianza per sostituzione
• Denotazione classica vs intuizionista
• Connettivi: sintassi, Backus-Naur Form, minimalità, ricorsione strutturale, induzione
• Sintassi BNF in BNF

Mer. 08/10/08, 08:30, aula Cremona

• Esempi di ricorsione strutturale: numero di simboli, altezza, numero di nodi, essere bilanciato, contenere una sola variabile
• Esempi di induzione: il numero di nodi è sempre <= di 2 elevato all'altezza meno 1; il numero di nodi è sempre >= dell'altezza; se l'albero è bilanciato e contiene solo connettivi binari, allora il numero di nodi è = a 2 elevato all'altezza meno 1
• Definizione ricorsiva di semantica classica della logica proposizionale
• Tabelle di verità per la semantica classica

Lun. 13/10/08, 13:30, aula Cremona

• Definizioni di soddisfacibilità, contradditorietà, tautologia, falsificabilità
• Definizione di conseguenza semantica
• Teorema di deduzione semantica

Mer. 15/10/08, 08:30, aula Cremona

• Semantica intuizionista della logica proposizionale
• Definizione di sostituzione
• Dimostrazione dell'invarianza per sostituzione
• Definizione di equivalenza semantica
• Introduzione del connettivo di coimplicazione

Lun. 20/10/08, 13:30, aula Cremona

• Principali equivalenze semantiche classiche e intuizioniste
• Relazioni, relazioni di equivalenza e congruenze
• Forme normali disgiuntive e normalizzazione di formule
• Introduzione all'utilizzo del dimostratore interattivo di teoremi Matita

Mer. 22/10/08, 08:30, aula Cremona

• Algoritmo per trasformare una formula in CNF o DNF
• Reti combinatoriche
• Corrispondenza fra reti combinatoriche e formule del calcolo proposizionale
• Completezza funzionale
• Algoritmo per sintetizzare una formula a partire dalla sua tabella di verità
• Esempi di insiemi di connettivi funzionalmente completi

Lun. 27/10/08, 13:30, aula Cremona

• Teorema di espansione di Shannon
• Introduzione del connettivo if-then-else
• If-then-else normal form, BDD, OBDD, ROBDD
• Costruzione di ROBDD a partire da formule date e da tabelle di verità

Mer. 29/10/08, 08:30, aula Cremona

• Sintesi di formule logiche tramite il metodo delle mappe di Karnaugh

Lun. 03/11/08, 13:30, aula Cremona

• Deduzione naturale per la logica intuizionista

Mer. 5/11/08, 08:30, aula Cremona

• Teorema di correttezza per la deduzione naturale intuizionista
• Teorema di correttezza per la deduzione naturale classica
• Specifica di un linguaggio di programmazione per le evidenze della semantica intuizionista di una prova
• Teorema di completezza per la deduzione naturale intuizionista
• Assiomi equivalenti della deduzione naturale classica

Lun. 10/11/08, 13:30, aula Cremona

• Teorema di completezza finita per la deduzione naturale classica
• Descrizione delle mutue implicazioni fra i teoremi di completezza, correttezza e compattezza
• Algoritmo di risoluzione

Mer. 12/11/08, 8:30, aula Cremona

• Teorema di compattezza
• Correttezza e completezza del metodo di risoluzione per il calcolo proposizionale

Lun. 17/11/08, 13:30, aula Cremona

• Sintassi della logica del primo ordine
• Variabili libere, alpha-conversione e sostituzione

Mer. 19/11/08, 8:30, aula Cremona

• Semantica classica per i linguaggi del primo ordine
• Semantica intuizionista per i linguaggi del primo ordine
• Deduzione naturale per i linguaggi del primo ordine

Lun. 24/11/08, 13:30, aula Cremona

• Soddisfacibilità, insoddisfacibilità, validità di formule di un linguaggio al primo ordine
• Esercitazioni sul linguaggio proposizionale

Mer. 26/11/08, 8:30, aula Cremona

• Equivalenze notevoli nel linguaggio del primo ordine

Lun. 01/12/08, 13:30, aula Cremona

• Altre equivalenze notevoli nel linguaggio del primo ordine
• Forma normale prenessa e trasformazione di una formula in una formula equivalente in forma normale prenessa
• Forma normale di Skolem e computo della forma normale di Skolem equi-soddisfacibile a una formula data

Mer. 03/12/08, 08:30, aula Cremona

• Decidibilità e semi-decidibilità
• Teoria di Herbrand per la logica del primo ordine
• Semi-decidibilità della logica del primo ordine

Mer. 10/12/08, 08:30, aula Cremona

• Sostituzioni, unificatori e unificatori più generali
• Algoritmo di unificazione
• Metodo di risoluzione per la logica dei predicati
• Ridondanza di informazione negli alberi di deduzione naturale
• Dalla deduzione naturale ai linguaggi di dimostrazione dichiarativi, procedurali e ai proof-termini (cenni)

Lun. 15/12/08, 13:30, aula Cremona

• Enunciati dei Teoremi di Incompletezza di Godel
• Cenni alle dimostrazioni dei Teoremi di Incompletezza di Godel
• Cenni alla teoria dei modelli: esistenza di modelli non standard per l'aritmetica; cenni agli enunciati dei teoremi di Lowenheim-Skolem;
• Cenni alla programmazione logica e collegamenti con il metodo di risoluzione

Esercitazioni in laboratorio:

Mer. 22/10/08

L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita al fine di:

• definire la sintassi delle formule del calcolo proposizionale
• definire la semantica classica delle formule del calcolo proposizionale
• dare la funzione di sostituzione
• dimostrare per induzione l'invarianza per sostituzione

Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.

È inoltre disponibile una breve introduzione a Matita che riassume il più piccolo insieme di comandi sufficiente per l'esercitazione.

Mer. 29/10/08, Mer. 05/11/08

L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita al fine di dimostrare il principio di dualità per il calcolo proposizionale. La dimostrazione consiste nel:

• definire l'operazione sintattica di negazione di tutti gli atomi
• definire l'operazione sintattica di dualizzazione di una formula
• definire l'operazione semantica di negazione di una valutazione
• dimostrare che la composizione della dualizzazione e della negazione di tutti gli atomi corrisponde semanticamente alla negazione della formula
• concludere, per mezzo di ulteriori lemmi tecnici, che l'equivalenza fra formule è preservata dalla dualizzazione

Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.

È inoltre disponibile una spiegazione dettagliata dell'esercitazione che enuncia le linee guida della prova.

Mer. 12/11/08

L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita al fine di dimostrare il teorema di espansione di Shannon per il calcolo proposizionale.

Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.

È inoltre disponibile una spiegazione dettagliata dell'esercitazione che enuncia le linee guida della prova.

Mer. 19/11/08

L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita come correttore di alberi di derivazione per la logica proposizionale.

Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.

È inoltre disponibile una spiegazione dettagliata dell'esercitazione che enuncia le linee guida della prova.

Mer. 26/11/08

L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita come correttore di alberi di derivazione per la logica proposizionale.

Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.

Mer. 03/12/08

L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita come correttore di alberi di derivazione per la logica del primo ordine.

Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.

È inoltre disponibile una spiegazione dettagliata dei comandi da utilizzare nell'esercitazione.

Mer. 10/12/08

L'esercitazione consiste nell'utilizzo del dimostratore interattivo di teoremi Matita come correttore di alberi di derivazione per la logica del primo ordine. In particolare, si richiede di effettuare una semplice dimostrazione nella teoria dell'aritmetica di Peano.

Il testo dettagliato dell'esercizio con le istruzioni per la consegna è disponibile qui.

È inoltre disponibile una spiegazione dettagliata dei comandi da utilizzare nell'esercitazione.

Esempi di domande sugli argomenti del corso (per la prima parte dell'esame):

1. Definire la sintassi delle formule della logica proposizionale
2. Definire le nozioni di conseguenza logica ed equivalenza logica
3. Definire la semantica classica di una formula della logica proposizionale
4. ...
5. Enunciare il teorema di completezza per la deduzione naturale proposizionale
6. Enunciare il teorema di compattezza per la logica proposizionale
7. Enunciare il teorema di correttezza per la deduzione naturale proposizionale
8. Enunciare il teorema di correttezza per la risoluzione proposizionale
9. Enunciare il teorema di completezza per la risoluzione proposizionale
10. Enunciare il teorema di espansione di Shannon per la logica proposizionale
11. Enunciare il teorema di dualità per la logica proposizionale
12. ...
13. Dimostrare il teorema di correttezza per la deduzione naturale proposizionale
14. Dimostrare il teorema di completezza per la deduzione naturale proposizionale
15. Dimostrare il teorema di espansione di Shannon
16. Dimostrare il lemma di sostituzione
17. Dimostrare il teorema di dualità

Esempi di esercizi sugli argomenti del corso (per la seconda parte dell'esame):

1. Definire, per ricorsione strutturale sulle formule del calcolo proposizionale, la funzione flip(F) che sostituisce tutte le occorrenze di A con occorrenze di B in F e viceversa
2. Dimostrare per induzione su F che flip(flip(F)) = F per ogni formula F del calcolo proposizionale
3. Dire quali delle seguenti formule sono classicamente soddisfacibili, quali insoddisfacibili, quali tautologiche:
   • (A ⇒ B) ∧ (B ⇒ A)
   • ¬((A ⇒ C) ∧ (B ∨ ¬A))
   • ¬((A ⇒ C) ∧ (C ∨ ¬A))
   • ¬(A ⇒ (¬B ∧ C)) ∧ ¬(¬C ∨ B)
   Ogni affermazione deve essere adeguatamente motivata.
4. Costruire la tabella di verità per la seguente formula: ¬(A ⇒ ¬(B ∧ A ∨ ¬C))
5. Data la seguente tabella di verità

   A	B	C	D	?
   0	0	0	0	0
   0	0	0	1	0
   0	0	1	0	1
   0	0	1	1	0
   0	1	0	0	1
   0	1	0	1	1
   0	1	1	0	0
   0	1	1	1	1
   1	0	0	0	0
   1	0	0	1	0
   1	0	1	0	1
   1	0	1	1	0
   1	1	0	0	1
   1	1	0	1	1
   1	1	1	0	0
   1	1	1	1	1

   sintetizzare, senza usare la tecnica delle mappe di Karnaugh, una formula in CNF e una in DNF caratterizzate dalla stessa tabella. Ripetere l'esercizio utilizzando le mappe di Karnaugh.
6. Disegnare una mappa di Karnaugh contenente tre implicanti primi dei quali due essenziali e uno non essenziale. Indicare chiaramente quali sono gli implicanti primi e quali sono essenziali. Indicare nella stessa mappa almeno due implicanti non primi.
7. Costruire un ROBDD corrispondente alle seguenti formule:
   • ¬((A ⇒ C) ∧ (B ∨ ¬A))
   • ¬((A ⇒ C) ∧ (C ∨ ¬A))
   • A ∧ ¬(B ∨ C) ⇒ ¬C ∧ (B ⇒ ¬B)
8. Usando esclusivamente equivalenze logiche, mettere le seguenti formule in CNF e in DNF:
   • ¬((A ⇒ C) ∧ (B ∨ ¬A))
   • ¬((A ⇒ C) ∧ (C ∨ ¬A))
   • A ∧ ¬(B ∨ C) ⇒ ¬C ∧ (B ⇒ ¬B)
9. Per ognuna delle seguenti formule, scrivere una formula logicamente equivalente usando solamente i connettivi indicati:
   • ¬((A ⇒ C) ∧ (B ∨ ¬A)) usando solo ∨ e ¬
   • ¬((A ⇒ C) ∧ (C ∨ ¬A)) usando solo ⇒ e ¬
   • A ∧ ¬(B ∨ C) ⇒ ¬C ∧ (B ⇒ ¬B) usando solo ∧ e ¬
10. Dimostrare tramite deduzione naturale le formule tautologiche della seguente lista. Le tautologie intuizioniste debbono essere dimostrare senza ricorrere ad assiomi classici. Per le formule che non sono tautologie classiche dare invece un contro-modello che mostri che non sono tautologiche.
    • (A ⇒ C) ⇒ (¬A ⇒ D) ⇒ ¬ (¬C ∧ ¬D)
    • (A ⇒ C) ⇒ (¬A ⇒ D) ⇒ C ∨ D
    • ¬(¬(A ⇒ C) ∨ ((¬A ⇒ D) ⇒ C ∨ D))
11. Dimostrare tramite il metodo di risoluzione le formule tautologiche della seguente lista. Per le formule che non sono tautologie classiche dare invece un contro-modello che mostri che non sono tautologiche.
    • (A ⇒ C) ⇒ (¬A ⇒ D) ⇒ ¬ (¬C ∧ ¬D)
    • (A ⇒ C) ⇒ (¬A ⇒ D) ⇒ C ∨ D
    • ¬(¬(A ⇒ C) ∨ ((¬A ⇒ D) ⇒ C ∨ D))
12. Dimostrare che la seguente formula è classicamente insoddisfacibile usando il metodo di risoluzione prima e la deduzione naturale poi:
    • (A ∨ ¬(¬C ∧ (⊤ ⇒ ¬B))) ∧ ¬((¬B ⇒ A) ∨ (¬C ⇒ A))
13. Data una formula della logica del primo ordine, dire se questa è valida (e in tal caso darne una dimostrazione), insoddisfacibile (e in tal caso dimostrare la sua negata) o soddisfacibile (e in tal caso fornire un modello in cui questa sia vera e uno in cui questa sia falsa).
14. Dimostrare una data formula della logica del primo ordine tramite deduzione naturale o tramite il metodo di risoluzione.

Compiti (alcuni risolti) dati agli esami di linguaggi:

Compiti del Dott. Sacerdoti Coen.

Compiti dati agli esami di logica negli anni precedenti:

Compiti del Prof. Asperti.

Eserciziario del Dott. Dal Lago.

Compiti del Prof. Martini. Quelli il cui nome termina con "sol" sono risolti.