Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

"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

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

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.

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

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à

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

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

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

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.

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

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

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

Argomenti trattati nella lezione di oggi:

- Relazioni tra classi di complessità: P = CO-P; NP != CO-NP
- mdT ristrette
- Teorema di Cook + dimostrazione

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

Argomenti trattati nella lezione di oggi:

- Il teorema di Cook: continuazione e conclusione della dimostrazione

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

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

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

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à

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

Argomenti trattati nella lezione di oggi:

- Dimostrazione del Teorema di Unica Leggibilità
- Semantica delle formule, soddisfacibilità, tautologicità, finita soddisfacibilità
- Teorema di compattezza + dimostrazione

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

Argomenti trattati nella lezione di oggi:

- Teorema di compattezza: dimostrazione
- Equivalenza logica, rimpiazzamento, CNF e DNF

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

Argomenti trattati nella lezione di oggi:

- CNF come insieme di insiemi (clausole)
- Conseguenza logica
- Certificati basati su risoluzione
- Lemma di correttezza + dimostrazione
- Completezza refutazionale

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

Argomenti trattati nella lezione di oggi:

- Teorema di completezza di Robinson + dimostrazione
- Deduzione refutazionale

__________________
The man in black fled across the desert and the gunslinger followed.

Bulma

.grande:maestro.

User info:

Registered: Jun 2002
Posts: 1706 (0.21 al dì)
Location: Rondinera City
Corso: Specialistica in Informatica
Anno: Dott. Mag.
Time Online: 72 Days, 20:00:05: [...]
Status: Offline

Post actions:

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

__________________
The man in black fled across the desert and the gunslinger followed.