Corso di laurea magistrale in Informatica

Conoscenze di base di teoria degli insiemi, matematica discreta, logica matematica, e nozioni elementari di linguaggi formali. Sono tipicamente fornite da insegnamenti come Fondamenti dell'Informatica (INF0348), Logica Matematica (INF0336).

L’insegnamento è tra quelli a scelta libera. In linea con gli Obiettivi formativi specifici del CdS in Informatica (LM18), l'insegnamento fornisce strumenti formali adatti a descrivere senza ambiguità concetti e proprietà necessari negli ambiti in cui opera un informatico: quello informale, tipico di contesti in cui si interagisce con persone in fase progettuale, e quello più rigido e formale, tipico del contesto implementativo, operando su sistemi informatizzati. 

CONOSCENZA E CAPACITÀ DI COMPRENSIONE. La conoscenza è relativa a: (A) principali modelli per il calcolo proposizionale (classico, intuizionsta, à la Kripke, ...); (B) algoritmi di soddisfacibilità e strumenti che li implementano; (C) sistemi deduttivi, relative proprietà e strumenti che implementano sistemi deduttivi. La capacità di comprensione riguarderà: (A) lettura, interpretazione e sintesi di formule di calcoli proposizionalo, in accordo con i vari modelli proposti; (B) motivi per cui dimostrazioni di proprietà di algoritmi di soddisfacibilità e sistemi deduttivi sono rilevanti e perché esse valgono.

CAPACITÀ DI APPLICARE CONOSCENZA E COMPRENSIONE. Si realizzano, sapendo costruire manualmente, o in maniera semi-automatica, tramite gli strumenti opportuni, dimostrazioni o esercizi specfici di formalizzazione, usando algoritmi di soddisfacibilità e sistemi deduttivi in accordo con semantiche note.

AUTONOMIA DI GIUDIZIO. Si esercita maturando conoscenza, capacità di comprensione e applicazione di algoritmi di soddisfacibilità  o sistemi deduttivi, semantiche e proprietà associate, col fine di modellare requisiti relativi al funzionamento di sistemi informatizati. 

ABILITÀ COMUNICATIVE. Si realizzano, innalzando l'abilità media nel descrivere proprietà di sistemi informatizzati, o algoritmi, tramite formule logiche, algoritmi o sistemi deduttivi associati.

CAPACITÀ DI APPRENDIMENTO. Si realizza e migliora come conseguenza della sollecitazione mentale che deriva dal dover descrivere proprietà di sistemi informatizzati, o algoritmi, tramite formule logiche, algoritmi di soddisfacibilità e sistemi deduttivi associati, in accordo con la semantica intesa.

Allineamento su concetti base: sintassi e semantica di Calcolo Proposizionale Classico.

Parte I

• Calcolo Proposizionale Classico e Procedure di Decisione: introduzione agli algoritmi come DPLL (Davis-Putnam-Logemann-Loveland) e CDCL (Conflict-Driven Clause Learning); pratica con applicazioni reali tramite SAT solver (ad esempio, MiniSAT);
• Calcolo Proposizionale Classico e Teoria (Strutturale) della Dimostrazione: studio di sistemi come il sistema di sequenti LK; dimostrazione delle principali proprietà (come correttezza e completezza) e pratica con strumenti come Rocq (ex Coq)/LEAN.

Parte II

• Dai Proof Assistant al Calcolo Proposizionale Intuizionista: approfondimento della teoria strutturale della dimostrazione, con focus su sistemi come Gentzen-style LJ, integrati con semantica costruttiva; principali proprietà;
• Corrispondenza Curry-Howard: esplorazione dell'equivalenza fra tipi e prove nell'ambito della logica intuizionista.

Parte III

• Dal Calcolo Proposizionale Classico alle Logiche Modali:
  • Sistemi deduttivi principali come il sistema di sequenti K (o S4) per calcoli proposizionali modali;
  • Introduzione alla semantica di Kripke per interpretare le logiche modali.

Le lezioni saranno tradizionali, tendenzialmente organizzate con l'illustrazione di esempi motivanti, dei concetti formali che generalizzano gli esempi, per quanto possibile, accompagnati da descrizioni intuitive, e da esperimenti su strumenti adatti.

 

Esame scritto in presenza. I compiti saranno costituiti da domande relative ai contenuti del programma didattico: (i) teoremi e parti di dimostrazioni; (ii) definizioni di algoritmi, loro simulazione e proprietà; (iii) esercizi relativi ai concetti chiave sviluppati.