Semantica Tarskiana.
Problemi SAT.
Ricerca, Conflitto e Backjumping.
Semantica dei Linguaggi Elementari.
Soddisfacibilità Modulo Teorie.
Uso dei software SMT-solver.
Quantificatori in contesti aritmetici.
Il corso si propone di introdurre metodi basilari di logica matematica nell’ambito del ragionamento automatico.
Verranno trattate tecniche di saturazione e completamento e tecniche di backtracking.
Sarà esaminato il potenziale uso di questi strumenti per la ricerca scientifica e per le applicazioni tecniche.
Alla fine del corso, lo studente conoscerà alcune procedure di decisione basilari per il ragionamento automatico, sarà in grado di spiegarne il funzionamento e le saprà utilizzare in pratica, sia svolgendo calcoli con carta e penna, sia al computer con l'impiego di software libero.
Prerequisiti
Nessun prerequisito specifico.
Metodi Didattici
Lezioni frontali: esposizione critica della teoria in programma, con interazione diretta docente-studente per facilitare e assicurare la piena comprensione della materia.
Esercitazioni: guida per gli studenti alla modellizzazione e risoluzione di una vasta scelta di problemi. Le esercitazioni sono condotte in modo da:
-- aiutare gli studenti a sviluppare le capacità di applicare e comunicare le conoscenze acquisite;
-- migliorare la loro indipendenza di giudizio.
Piattaforma Moodle: sviluppo dell’interazione online docente-studente; diffusione di dispense integrative, di esercizi settimanali e di testi delle prove scritte degli anni passati.
Modalità di verifica apprendimento
L’esame è suddiviso in tre parti, di uguale importanza per la formulazione del giudizio finale. La prova è sia scritta che orale.
La prima è volta ad accertare la conoscenza e la comprensione delle nozioni teoriche.
La seconda parte conterrà brevi esercizi di calcolo che possono essere svolti con carta e penna.
La terza parte consisterà nello scrivere un breve script per la soluzione al computer di un problema.
Sarà valutata la chiarezza e la completezza dell’esposizione, la capacità di impostare correttamente i problemi, di scegliere i metodi risolutivi appropriati e la correttezza delle soluzioni ottenute.
Programma del corso
Semantica Tarskiana.
Linguaggi Proposizionali; Funzioni di Verità; Completezza funzionale.
Problemi SAT.
Forme Normali; La Procedura DPLL; Il Calcolo della Risoluzione.
Ricerca, Conflitto e Backjumping.
Ricerca e Conflitto; Regole di Ricerca; Regole di Conflitto.
Semantica dei Linguaggi Elementari.
Strutture; Soddisfacibilità di Clausole Ground; Teorema di Herbrand; Skolemizzazione.
Soddisfacibilità Modulo Teorie.
La procedura CDCL; Esempi di procedure di decisione; Combinazione di procedure di decisione.
Utilizzare un SMT-solver.
Lo standard SMT-LIB2; Sistemi di Transizione e Bounded Model Checking; Utilizzo di z3 all’interno di Python.
Quantificatori in contesti aritmetici.
Aritmetica Lineare sui Reali; Aritmetica Lineare sugli Interi.
Approfondimenti e Complementi.
Aritmetica Non Lineare; Complessità e Teorema di Cook-Levine.