LOGICA
Docenti
- Scheda dell'insegnamento
- Obiettivi formativi
- Prerequisiti
- Contenuti
- Metodi didattici
- Verifica dell'apprendimento
- Testi
- Altre informazioni
Il corso si propone di fornire le conoscenze dei meccanismi di base dell'inferenza logica, attraverso lo studio delle fondamentali nozioni di logica proposizionale classica e del primo ordine. Tali conoscenze sono rivolte a formare e ad aumentare la capacità di astrazione delle informazioni attraverso la rappresentazione simbolica e quindi la capacità della comprensione di un linguaggio scientifico astratto e simbolico. Verranno accennati alcuni approfondimenti su strumenti di carattere più applicativo come i SAT-solver e le logiche non classiche (temporali e fuzzy) per la verifica dei programmi. I risultati di apprendimento attesi comprendono la capacità di saper individuare eventuali errori in una argomentazione matematica, e di avere una proprietà di linguaggio tale da poter enunciare un teorema e descrivere una sua dimostrazione. La conoscenza dei meccanismi logici del ragionamento matematico permette l’acquisizione di adeguate capacità per l'approfondimento delle proprie conoscenze e per lo sviluppo individuale di nuove competenze.
Per un proficuo apprendimento di questo insegnamento lo studente deve padroneggiare le nozioni matematiche e le tecniche dimostrative impartite nell’insegnamento fondamentale di Algebra e Geometria del primo anno, che dunque costituisce propedeuticità obbligatoria.
Logica Proposizionale
• Che cosa è la logica: metodi inferenziali e deduzione. Il linguaggio della logica proposizionale. Connettivi proposizionali. Semantica della logica proposizionale. Tavole di verità . Formule soddisfacibili e tautologie. (4h)
• Insiemi soddisfacibili, conseguenze logiche, teorema di deduzione. Equivalenza logica, algebra delle classi di equivalenza delle formule, algebre di Boole. Completezza funzionale e forme normali disgiuntive e congiuntive. Le equivalenze fondamentali, trasformazione di una formula in forma normale. (6h)
• Teorema di compattezza e lemma di König. (2h)
• Metodi di dimostrazione automatica: i Tableaux. Teorema di completezza e correttezza per i tableaux, Hintikka set. (4h)
• Altri sistemi deduttivi: Sequenti. Clausole, risoluzione, procedura di Davis Putnam, completezza e correttezza della procedura di Davis-Putnam. Clausole di Krom e clausole di Horn (6h)
Logica dei Predicati
• Il linguaggio della logica dei predicati, termini e formule. Campo d'azione di un quantificatore, variabili libere e vincolate, sostituzioni. (2h)
• Strutture, interpretazioni e valutazioni Formule soddisfacibili e valide. Modelli di una formula. Equivalenze logiche per la logica dei predicati. Forme normali prenesse, Forma di Skolem. Trasformazione di una formula in forma di Skolem e equisoddisfacibilità. (6h)
• Tableaux per la logica dei predicati, teorema di correttezza e completezza per i tableaux (4h)
• Teoria di Herbrand: universo e Base di Herbrand, modelli di Herbrand. Estensioni di Herbrand, teorema di Herbrand. (4h)
• Risoluzione per il calcolo proposizionale e per la logica dei predicati, algoritmo di unificazione. Teorema di completezza per la risoluzione proposizionale, lifting lemma, teorema di completezza per il calcolo dei predicati. (6h)
• Clausole di Horn, programmazione logica e risoluzione SLD. Esempi di programmi. (4h)
Logiche non classiche
• Strutture di Kripke. Logica modale minimale, esempi di formule modali che caratterizzano proprietà delle strutture di Kripke, Logica temporale. (4h)
• Tavole di verità di logiche a più valori, T-norme e fuzzy sets, logica delle t-norme continue. (4h)
Il corso si articola in lezioni frontali (32 ore) ed esercitazioni (24 ore). Le lezioni sono dedicate all'illustrazione degli argomenti oggetto del corso. Gli argomenti trattati a lezione sono oggetto di
esercitazioni che prevedono la partecipazione attiva degli studenti e comprendono la risoluzione di esercizi relativi all’applicazione delle nozioni e dei risultati presentati a lezione. Gli esercizi presentati costituiscono una fondamentale linea guida per la preparazione dell’esame.
L’obiettivo della prova d’esame è l'accertamento dell’acquisizione delle conoscenze e delle abilità descritte nella sezione “Obiettivi del corso”, valutando il livello di conoscenza e la capacità di applicare le nozioni e le tecniche dimostrative viste a lezione.
L’esame consiste in una prova scritta articolata secondo il seguente schema: (parte A) due domande relative alla presentazione e applicazione delle nozioni presentate nell’insegnamento; (parte B) dimostrazione di uno dei teoremi presentati a lezione; (parte C) cinque esercizi sullo schema di quelli presentati a lezione.
L’attribuzione del voto finale sarà determinata per il 30% dalla conoscenza delle definizioni e dalla capacità di applicarle (parte A), pre il 20% dalla conoscenza e comprensione delle dimostrazioni dei teoremi (parte B), per il 50% dalla capacità di applicare le nozioni apprese nel corso alla soluzione degli esercizi (parte C).
Il voto finale è espresso in trentesimi.
Logica ad Informatica, di Asperti, Ciabattoni.Ed. McGraw-Hill
Le slide delle lezioni in formato PDF sono messe a disposizione sulla piattaforma e-learning di Ateneo ove sono disponibili anche il testo dei problemi visti durante le esercitazioni e le soluzioni proposte.
Il docente riceve su appuntamento, previa richiesta via e-mail a mauro.ferrari@uninsubria.it. Il docente risponde solo alle e-mail firmate e provenienti dal dominio studenti.uninsubria.it.
Cerchi il programma? Potrebbe non essere ancora stato caricato o riferirsi ad insegnamenti che verranno erogati in futuro.
Seleziona l‘anno in cui ti sei immatricolato e troverai le informazioni relative all'insegnamento del tuo piano di studio.