Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

Docenti: Silvio Ghilardi per la parte teorica, Anna Morpurgo per la parte di prolog e Lorenzo Sacchetti per le esercitazioni

Orari: lunedì e venerdì dalle 9.00 alle 10.30

Orario ricevimento del prof: Venerdì alle 11.30

Materiale didattico: niente libri di testo, solo la dispensa scaricabile dal sito del corso

Sito del corso: http://homes.dsi.unimi.it/~logica/logimat/

Modalità d'esame: parte scritta obbligatoria e parte facoltativa. La parte facoltativa può essere di 3 tipi:

• matematico-logica: dimostrazioni matematiche e logiche, i docenti di riferimento sono Ghilardi e Sacchetti
  
• filosofico-culturale: approfondimento sulla storia e filosofia della logica, il docente di riferimento è Ghilardi
  
• di programmazione: progettino in prolog, il docente di riferimento è Morpurgo
  

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

LOGICA PROPOSIZIONALE
-enunciati atomici (o lettere proposizionali)
-enunciati composti
-connettivi logici
-definizione di formula (o enunciato)
-differenza sintassi-semantica
-assegnamento del valore di verità
-deduzione del valore di verità di alcuni enunciati composti dato il valore di verità degli enunciati atomici che li compongono (come A and B, not A, A or B, A=>B)

darkAntAreS

...bloup will rule you...

User info:

Registered: Jun 2004
Posts: 267 (0.04 al dì)
Location: gorgonzola(MI)
Corso: informatica
Anno: x
Time Online: 3 Days, 14:49:45 [...]
Status: Offline

Post actions:

solo un breve ringraziamento per Polsy: GRAZIE! oggi ho perso la metro e non c'ero a lezione

thx per il lavoro che stai facendo, di cuore



p.s.: appena Polsy legge qui (max venerdi) cancellate pure...era solo uno sfogo di sollievo

__________________
"Ash nazg durbatulûk, ash nazg gimbatul, ash nazg thrakatulûk agh burzum-ishi krimpatul"

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

lol prego!

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

-precedenze dei connettivi logici
-tavole di verita`
-definizione di tautologia e di formula soddisfacibile
-problema di SAT (satisfiability)
-valutazione di sillogismi tramite tavole di verita`

info: le dimostrazioni sono richieste solo come parte facoltativa, per la parte scritta bastano gli enunciati dei teoremi
ci saranno alcune lezioni dedicate a dimostrazioni e storia della logica, ma saranno a fine corso cosi` chi non vuole fare la parte relativa a quell`argomento sapra` quando non venire

Last edited by Polsy on 08-03-2005 at 00:20

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

-cenni sui metodi di calcolo automatico
-definizione di multiinsieme e sequente
-regole generali sulla valutazione di espressioni nei sequenti
-esercizi su come calcolare il valore di una formula coi sequenti

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

-ancora esercizi sui sequenti
-definizioni di formula dimostrabile e di albero di prova
-teoremi di validità e di completezza

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

PROCEDURA DPLL
-definizioni di: atomo, letterale, clausola, formula normale congiuntiva, formule equisoddisfacibili
-cosa fa un sat solver e come riconoscere una tautologia tramite un sat solver
-trasformazione di una formula in FNC (algoritmo di clausificazione + metodo strutturale per trasformare una formula normale negativa in formula normale congiuntiva)

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

Dato che venerdì eravamo 4 gatti per colpa dello sciopero il prof ha spiegato un altro metodo di risoluzione di formule logiche, argomento al di fuori del programma che di solito insegna nel corso per la specialistica e che non verrà chiesto all'esame.

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

CONCLUSIONE DPLL
assegnamento parziale progressivo di valori di verità per la dimostrazione di un insieme di clausole secondo le regole di: split, assert, subsume, resolve, pure literal

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

in ritarderrimo....
LOGICA DI 1° ORDINE (PREDICATIVA)
concetti di: costanti individuali, variabili, simboli di relazione n-aria, simboli di operazione n-aria, connettivi, quantificatori
definizioni di: linguaggio elementare, termine, formula

alcuni avvisi: tra una settimana ghilardi conta di finire il programma di teoria e lunedì prossimo inizierà il seminario di prolog a orario tradizionale non alle 9
inoltre venerdì 15 e 22 ci sarà esercitazione con sacchetti (così finalmente sapremo se si fanno compitini o meno)
se ho scritto ca**ate correggetemi, sono arrivata in ritardo e mi sono fatta dire gli avvisi e gli argomenti della prima ora un po' in fretta...

aralc

User info:

Registered: Nov 2002
Posts: 13 (0.00 al dì)
Location: Trecate
Corso: comunicazione digitale
Anno: 2°
Time Online: 3 Days, 9:27:25 [...]
Status: Offline

Post actions:

qualcuno mi sa dire dove posso trovare i risultati dell'appello del 7 aprile 05?

Grazie

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

definizioni di: occorrenza libera/vincolata, sostituzione, problema di unificazione, soluzione, Most General Unifier
altri concetti accennati: alfa-conversione, enunciati (o sentenze)

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

ALGORITMO DI UNIFICAZIONE
regole:
- simplify
- decompose
- replace
- orient
- conflict
- occur check
AVVISO
è online la
dispensa sulla DPLL ed è protetta da password, se a qualcuno serve me la chieda via pm
inoltre qui alle pagine 19-24 c'è spiegato l'algoritmo di unificazione

Polsy

.arcimaestro.

User info:

Registered: Dec 2003
Posts: 477 (0.06 al dì)
Location:
Corso: Info phd
Anno:
Time Online: 17 Days, 17:11:50 [...]
Status: Offline

Post actions:

- funzione di interpretazione
- L-struttura
- linguaggio espanso
- interpretazione
- definizione induttiva di verità di un enunciato in una L-struttura
- modello
- conseguenza logica