Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

In questo thread segnerò lezione per lezione gli argomenti trattati nel corso di Logica per le applicazioni, insegnamento fondamentale per le due lauree specialistiche.
Laddove possibile farò riferimento (leggi: copia&incolla ) all'ottimo diario del corso dell'a.a. 2003/04 ad opera di Bulma, quando la denominazione del corso era semplicemente "Logica".

Oggi si è tenuta la prima lezione, il professore ha dato semplicemente alcune disposizioni organizzative e ha introdotto il corso, da domani comincerà a trattare gli argomenti del programma.

Orario delle lezioni
Il corso si terrà principalmente secondo gli orari pubblicati sul sito del DSI/DICO, ma le 8 ore settimanali di lezione saranno così suddivise:
- 4 ore (Lunedì e Martedì) di teoria
- 2 ore (Giovedì) dedicate all'insegnamento complementare di Logica II, solo ed esclusivamente per chi intende includere questo esame nel suo piano di studi
- 2 ore (Venerdì) di laboratorio in aula Delta
Per un mese circa non si terranno comunque lezioni in laboratorio.
Per chi volesse invece seguire anche il corso di Logica II (6 crediti), il corso sarà parallelo a quello di Logica per le applicazioni ma comincerà nel mese di Novembre.

Testi di riferimento e materiale didattico
Per quanto riguarda il materiale didattico, sono disponibili:
- una dispensa del prof, appena sufficiente ai fini del corso
- un libro del prof ("Sfidare l'indecidibile", Polimetrica 2004), disponibile a breve nelle librerie e più che sufficiente ai fini del corso (anzi, quasi abbondante)
- la documentazione di SPASS, un tool di dimostrazioni automatiche (http://spass.mpi-sb.mpg.de/)
Il prof sta preparando una pagina web del corso, domani ne comunicherà l'indirizzo. Ad ogni modo, è ancora possibile visitare una vecchia pagina del corso su webcen (http://webcen.usr.dsi.unimi.it/2002...ioni/index.html)

Modalità di esame
La finalità del corso è l'apprendimento dell'utilizzo di SPASS, un tool per dimostrazioni automatiche: durante le lezioni si apprenderà, tra le altre cose, proprio l'utilizzo del tool, perciò la frequenza al corso è consigliata per prendere confidenza col programma in maniera immediata.
L'esame sarà principalmente di carattere pratico: richiederà di saper utilizzare SPASS e di comprenderne i principi logici di funzionamento.

La prima lezione è durata poco più di mezz'ora

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Last edited by Walter on 27-09-2004 at 20:50

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Martedì 28 Settembre
Sintassi dei linguaggi elementari:
- definizione formale di linguaggio
- operatori logici
- termini e formule
- termini ground
- sottotermini
- occorrenze vincolate e libere di variabili
- enunciato
- sostituzioni
- definizione di albero come insieme di liste
- lemma di Konig

Indirizzo del sito del corso
http://homes.dsi.unimi.it/~ghilardi/ls/lpa.html

Infine un'avvertimento: siate puntuali a lezione!
Il prof non tollera chi entra in aula a lezione iniziata... siete avvisati

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Last edited by Walter on 28-09-2004 at 19:01

nous

.:Retore Pomposo:.

User info:

Registered: Dec 2001
Posts: 2945 (0.33 al dì)
Location: Fino Mornasco - Como
Corso: Informatica
Anno: Specialista
Time Online: 16 Days, 13:56:49 [...]
Status: Offline

Post actions:

Mi raccomando : se non arrivate per tempo entrare alla pausa.
Se mi permetti di aggiungere una cosa, ha anche definito i sottotermini di t e alcune loro proprietà.

__________________
Cristian,il Nous che invoglia ^_^

"La capa è troppo in la,e la sbarba è troppo giovane..mi sa che qua si va in bianco"
Ryo Saeba (City Hunter)

mozilla

.precettore.

User info:

Registered: Jul 2003
Posts: 93 (0.01 al dì)
Location:
Corso:
Anno:
Time Online: 23:34:57 [...]
Status: Offline

Post actions:

l'interfaccia per SPASS la potete trovare qui:

http://homes.dsi.unimi.it/~ghilardi...spasseditor.zip

per la password dello zip mandatemi un'email dall'indirizzo dell'unimi qui oppure la prossima lezione la diciamo a tutti.

__________________
"Direi che la signorina Lucy è più calorosa di una sposa di Giugno che cavalca nuda un cavallo senza sella in mezzo al Sahara" - Il Colono, Dracula di Francis Ford Coppola

Last edited by mozilla on 28-09-2004 at 19:03

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Originally posted by nous
Se mi permetti di aggiungere una cosa, ha anche definito i sottotermini di t e alcune loro proprietà.

Ottimo, grazie, ho editato ed aggiunto i sottotermini
Il programma della prima lezione si trova nei paragrafi 1.1 e 1.4 delle dispense del corso.
Qualsiasi altra segnalazione è benvenuta.

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Last edited by Walter on 28-09-2004 at 19:07

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Lunedì 4 Ottobre
Oggi sono stati trattati i seguenti argomenti:
- l'operazione di sostituzione (ultimo punto del paragrafo 1.1 delle dispense)
- la semantica dei linguaggi elementari (par 1.2 fino a pag 9)
--- concetto di interpretazione e di dominio
--- L-struttura
--- introduzione alla relazione di verità

Domani verrà molto probabilmente completato il paragrafo 1.2 con la nozione di verità logica.

Aggiunte o correzioni sono sempre benvenute

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Martedì 5 Ottobre

- definizione di verità
- tavole di verità
- chiusura universale
- chiusura esistenziale
- soddisfacibilità
- modello
- conseguenza logica
- verità logica

- introduzione a SPASS
--- interfaccia
--- terminazione dell'applicazione ('proof found', 'completion found') o non terminazione (la divergenza non è eliminabile e non è osservabile dall'esterno)

- introduzione al saturation based theorem proving e alle sue fasi
--- preprocessamento (skolemizzazione) di ipotesi e negazione della tesi
--- main loop (cicli di inferenze)

Nella prossima lezione: skolemizzazione e clausole.

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Last edited by Walter on 11-10-2004 at 13:43

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Lunedì 11 Ottobre

- definizione di clausola, notazione e semantica delle clausole vuote
- preprocessamento di una formula e skolemizzazione (con esempi)

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Martedì 12 Ottobre

- esempio di skolemizzazione
- calcolo della Risoluzione: introduzione al metodo di unificazione
--- sostituzioni e composizione di sostituzioni

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Lunedì 18 Ottobre

- generalità di una sostituzione
- rinomina
- problema di unificazione
- mgu (most general unifier)
- algoritmo di unificazione
--- semplificazione
--- decomposizione
--- orientamento
--- sostituzione
--- fallimento (conflitto, occur check)
- matching

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Martedì 19 Ottobre

- calcolo di risoluzione
-- risoluzione
-- fattorizzazione destra
- derivazione (o proof)
- teorema di completezza
- primi esercizi di derivazione con SPASS

Settimana prossima non ci sarà lezione causa impegni all'estero del professore

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Martedì 2 Novembre

- Clausola Horn
- esercizi di risoluzione
- struttura di un proover
--- worked off clauses & usable clauses
--- algoritmo della given clause
--- inferenze
--- riduzioni
----- forward reduction
----- backward reduction
- esempi di applicazione dell'algoritmo della given clause

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Lunedì 8 Novembre

- ordinamento su termini
--- proprietà irriflessiva
--- proprietà transitiva
--- terminazione
--- stabilità
--- compatibilità
--- proprietà del sottotermine
--- ordinamento totale su termini ground
- terminologia
--- ordine di riscrittura
--- ordine di semplificazione
--- ordine di riduzione
--- ordine stretto
- teorema di Kruskal (solo dimostrazione)
- ordinamento LPO
--- precedenze
--- esercizi di ordinamento LPO

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Martedì 9 Novembre

- ordinamento KBO
--- funzione peso w (ammissibilità di w)
- ordinamento dei multinsiemi
- ordinamento con letterali negativi
- letterali massimali
- risoluzione ordinata
- fattorizzazione destra ordinata

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche

Walter

dsy adminz

User info:

Registered: Mar 2002
Posts: 5304 (0.61 al dì)
Location: Milano 90% - Valle Camonica 10%
Corso: Magistrale in Informatica
Anno: fine!
Time Online: 99 Days, 4:33:05: [...]
Status: Offline

Post actions:

Argomenti della lezione di Lunedì 15 Novembre

- meccanismo di selezione
- esercizi con Spass

__________________
"Ragione e passione sono timone e vela della nostra anima navigante." - Kahlil Gibran
"Senza musica la vita sarebbe un errore." - Friedrich Nietzsche