Tu sei qui

Logica Matematica

Logica Matematica
Corso di Laurea Triennale in Informatica F004

SCV0076
Docente: Brunella Gerla


CFU SSD LEZIONI ANNO LINGUA
6 MAT/01 48 II Italiano


Obiettivi dell’insegnamento e risultati di apprendimento attesi
Conoscenza e capacità di comprensione
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.
Conoscenza e capacità di comprensione applicate
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.
Autonomia di giudizio e abilità comunicative
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.
Capacità di apprendere
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.

Prerequisiti
Non è previsto alcun prerequisito, ma è consigliata una conoscenza di base di concetti di matematica (notazioni insiemistiche, prodotti cartesiani, funzioni).

Contenuti e programma del corso
Logica Proposizionale

  • Il linguaggio della logica proposizionale. Connettivi proposizionali. Semantica della logica proposizionale. Tavole di verità . Formule soddisfacibili e tautologie. (2h)
  • Insiemi soddisfacibili, conseguenze logiche, teorema di deduzione. Equivalenza logica, algebra delle classi di equivalenza delle formule, algebre di Boole. (4h))
  • Completezza funzionale e forme normali disgiuntive e congiuntive. Le equivalenze fondamentali, trasformazione di una formula in forma normale. Teorema di compattezza e lemma di König. (4h)
  • Metodi di dimostrazione automatica: i Tableaux. Teorema di completezza e correttezza per i tableaux, Hintikka set. (4h)
  • Clausole, risoluzione, procedura di Davis Putnam, completezza e correttezza della procedura di Davis-Putnam. Clausole di Krom e clausole di Horn (4h)

Logica dei Predicati

  • Il linguaggio della logica dei predicati, termini e formule. Campo d'azione di un quantificatore, variabili libere e vincolate, sostituzioni. Strutture, interpretazioni e valutazioni. Formule soddisfacibili e valide. Modelli di una formula. Equivalenze logiche per la logica dei predicati. (4h)
  • Forme normali prenesse, Forma di Skolem. Trasformazione di una formula in forma di Skolem e equisoddisfacibilità. (2h)
  • 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. (4h)
  • Clausole di Horn, programmazione logica e risoluzione SLD. Esempi di programmi. (4h)
  • Insiemi aritmetici, Teoria dei numeri naturali, Teoremi di incompletezza di Gödel. (2h)

Logiche non classiche

  • Strutture di Kripke. Logica modale minimale, esempi di formule modali che caratterizzano proprietà delle strutture di Kripke, Logica temporale. (3h)
  • Tavole di verità di logiche a più valori, T-norme e fuzzy sets, logica delle t-norme continue. (3h)

Tipologia delle attività didattiche
Lezioni frontali.

Testi e materiale didattico

  • Logica ad Informatica, di Asperti, Ciabattoni.Ed. McGraw-Hill.
  • Testi di approfondimento:
    • Logica: metodo breve di D. Mundici, Ed. Springer.
    • Logiche non-classiche di Dario e Claudia Palladino.
    • Mathematical Logic for Computer Science - di Mordechai Ben-Ari, ed. Springer.
    • Logica Matematica di Toffalori, Cintioli. Ed. McGraw-Hill
  • Letture: Il diavolo in cattedra di Piergiorgio Odifreddi, ed. Einaudi.
  • Dispense e slide delle lezioni sul sito di e-learning.

Modalità di verifica dell’apprendimento
L’esame consiste in un colloquio orale teso all'accertamento dell’acquisizione e della corretta comprensione dei contenuti del corso. E’ previsto un accertamento della capacità di argomentazione logica, tramite l’esposizione delle dimostrazioni di 2 teoremi studiati nel corso. Inoltre sarà richiesta la conoscenza dei metodi di dimostrazione automatica tramite lo svolgimenti di semplici esercizi durante la prova orale. Esempi di domande fatte all’esame orale si trovano sul sito di e-learning del corso. L’attribuzione del voto finale sarà determinata al 50% dalla conoscenza e comprensione delle dimostrazioni dei teoremi, al 30% dalla conoscenza di definizioni e esempi dei concetti affrontati durante il corso e al restante 20% dal corretto svolgimento degli esercizi.

Orario di ricevimento
IIl docente è a disposizione per il ricevimento studenti un pomeriggio a settimana (da determinare in base all’orario del corso) e su appuntamento da concordare tramite posta elettronica.

Theme by Danetsoft and Danang Probo Sayekti inspired by Maksimer