 | |
Il progetto dsy.it è l'unofficial support site dei corsi di laurea del Dipartimento di Scienze dell'Informazione e del Dipartimento di Informatica e Comunicazione della Statale di Milano. E' un servizio degli studenti per gli studenti, curato in modo no-profit da un gruppo di essi. I nostri servizi comprendono aree di discussione per ogni Corso di Laurea, un'area download per lo scambio file, una raccolta di link e un motore di ricerca, il supporto agli studenti lavoratori, il forum hosting per Professori e studenti, i blog, e molto altro...
In questa sezione è indicizzato in textonly il contenuto del nostro forum |
[Ragionamento Automatico I] Diario del corso 04/05
Clicca QUI per vedere il messaggio nel forum |
| Bulma |
"Metodi per il Ragionamento Automatico I" è un corso complementare per le lauree triennali e le specialistiche.
Il corso terminerà verso metà Aprile, quando avrà invece inizio il secondo modulo (Metodi per il Ragionamento Automatico II). Mentre il modulo I darà i fondamenti della materia, il modulo II sarà un corso monografico sulla logica polivalente.
Seguono alcune informazioni generali sul corso (modulo I):
Docente: S. Aguzzoli
Orari delle lezioni:
lunedì 9.00 - 11.30
martedì 9.00 - 10.30
mercoledì 9.00 - 10.30
in auletta 4 (via Comelico).
Note: l'inizio delle lezioni è stato posticipato di mezz'ora rispetto agli orari riportati sul sito del DSI. La lezione del lunedì può anche terminare prima delle 11.30, a seconda delle necessità.
Sito del corso:
Il sito del corso è questo. Attualmente è ancora in costruzione. ;)
Materiale didattico:
Appunti presi a lezione.
Modalità d'esame:
L'esame consiste di un orale sugli argomenti trattati a lezione. E' anche possibile sostituire parte dell'orale con una tesina su un argomento del corso, naturalmente concordato col docente.
Prerequisiti: Nessun prerequisito richiesto.
Programma:
1. Complessità computazionale:
- Macchine di Turing deterministiche e non deterministiche
- Classi P e NP
- Riduzioni polinomiali, NP-completezza
- Teorema di Cook
- Esempi di riduzioni polinomiali
2. Logica proposizionale:
- Nozioni base sintattiche e semantiche
- Calcolo proposizionale
- Teorema di compattezza
- Principio di risoluzione di Robinson e sua completezza
- Correttezza e completezza della procedura refutazionale di Davis-Putnam
- Model building, casi facili e difficili (Krom, Horn)
3. Logica del Primo Ordine:
- Nozioni base sintattiche e semantiche
- Forme normali prenesse, di Skolem, congiunte
- Universo di Herbrand
- Modelli Tarskiani e di Herbrand
- Teorema di Herbrand
- Teorema di completezza
4. Introduzione alla logica polivalente:
- Le t-norme
- Basic Logic di Hajek
- Sottovarietà di BL-algebre |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Cos'è il ragionamento automatico
- La storia del ragionamento automatico: Aristotele, Boole, Frege
- Generatore naive di teoremi; teorema di completezza di Godel, teorema di Church
Avviso: La lezione del 2 Marzo è sospesa. |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Calcolabilità: il problema della fermata
- Complessità: esempio del massimo comune divisore
- Preliminari matematici: insiemi, relazioni, funzioni
- Alfabeto, parola, linguaggio
- Esempi di problemi (alias linguaggi) di diversa complessità |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Variabili, letterali, clausole, CNF
- Riduzione fra linguaggi
- Il problema CNF-SAT; assegnamento a variabili e CNF
- Potere espressivo delle CNF
- Riduzione del problema del Commesso Viaggiatore a CNF-SAT
- Funzione computabile in modo efficiente |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Efficiente = polinomiale: motivazioni
- Schema di risoluzione per problemi "guru" (NP)
- Macchina di Turing deterministica
- Digressione: esistono funzioni non computabili
Avviso: La lezione di mercoledì 9 Marzo è sospesa causa sciopero dei mezzi pubblici. |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Linguaggio riconosciuto da una mdT deterministica; esempio (ODD)
- mdT non deterministiche; schema per problemi NP; esempio (COMPOSITE)
- Linguaggio riconosciuto da una mdT non deterministica
- Classe P e NP
- Tesi di Church e Tesi di Church estesa
- Riduzione polinomiale; problemi NP-hard e NP-completi; metodo per trovare problemi NP-completi |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Relazioni tra classi di complessità: P = CO-P; NP != CO-NP
- mdT ristrette
- Teorema di Cook + dimostrazione |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Il teorema di Cook: continuazione e conclusione della dimostrazione |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Problema 3CNFSAT, dimostrazione della sua NP-completezza
- Problema KNAPSACK, dimostrazione della sua NP-completezza
- Codificare problemi: regole anti-padding |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Il problema CLIQUE, dimostrazione della sua NP-completezza
- Soddisfacilibità di formule proposizionali, definizione di formula, teorema di unica leggibilità |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Dimostrazione del Teorema di Unica Leggibilità
- Semantica delle formule, soddisfacibilità, tautologicità, finita soddisfacibilità
- Teorema di compattezza + dimostrazione |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Teorema di compattezza: dimostrazione
- Equivalenza logica, rimpiazzamento, CNF e DNF |
| Bulma |
Argomenti trattati nella lezione di oggi:
- CNF come insieme di insiemi (clausole)
- Conseguenza logica
- Certificati basati su risoluzione
- Lemma di correttezza + dimostrazione
- Completezza refutazionale |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Teorema di completezza di Robinson + dimostrazione
- Deduzione refutazionale |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Procedura refutazionale di Davis-Putnam
- Teorema di completezza della DPP + dimostrazione
- Frammento KROM, KROMSAT è in P
- Frammento HORN, sua espressività, HORNSAT è in P |
| Bulma |
Argomenti trattati nella lezione di oggi:
- HORNSAT è in P (continuazione)
- Risoluzione lineare, risoluzione di input, risoluzione SLD
- La logica del I ordine: introduzione |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Logica del Primo Ordine: sintassi e semantica |
| Bulma |
Argomenti trattati nella lezione di oggi:
- La semantica Tarskiana
- Sostituzioni
- Algebra della formule del I ordine
- Forma normale prenessa, skolemizzazione, equisoddisfacibilità
|
| Bulma |
Argomenti trattati nella lezione di oggi:
- La semantica di Herbrand |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Teorema di Herbrand + dimostrazione |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Teorema di Herband, completezza e loro conseguenze
- Semidecidibilità di UNSAT al primo ordine |
| Bulma |
Argomenti trattati nella lezione di oggi:
- Sostituzioni, composizione di sostituzioni, unificatore e mgu
- Teorema di unificazione
- Clausole ortogonali, separatori, fattorizzazione, principio di risoluzione
- SFR deduzione, correttezza e completezza
Questa è stata l'ultima lezione del primo modulo del corso.
:ciao: |
|
|
|
|
