[Logica per le applicazioni] diario del corso 04/05
Clicca QUI per vedere il messaggio nel forum |
| Walter |
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 :D) 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 :) |
| Walter |
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 :) |
| nous |
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à. |
| Walter |
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. |
| Walter |
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 :) |
| Walter |
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. |
| Walter |
Argomenti della lezione di Lunedì 11 Ottobre
- definizione di clausola, notazione e semantica delle clausole vuote
- preprocessamento di una formula e skolemizzazione (con esempi) |
| Walter |
Argomenti della lezione di Martedì 12 Ottobre
- esempio di skolemizzazione
- calcolo della Risoluzione: introduzione al metodo di unificazione
--- sostituzioni e composizione di sostituzioni |
| Walter |
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 |
| Walter |
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 |
| Walter |
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 |
| Walter |
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 |
| Walter |
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 |
| Walter |
Argomenti della lezione di Lunedì 15 Novembre
- meccanismo di selezione
- esercizi con Spass |
| Walter |
Argomenti della lezione di Martedì 16 Novembre
- esercizi di riepilogo su quanto fatto nelle ultime settimane (con l'ausilio di Spass) |
| Walter |
Argomenti della lezione di Lunedì 22 Novembre
- vincoli
--- vincoli disgiuntivi
- soddisfacibilità
--- attuale
--- estesa
--- "pseudo-soddisfacibilità"
- vincoli sulla risoluzione
- indiscernibilità degli identici
- paramodulazione |
| Walter |
Argomenti della lezione di Martedì 23 Novembre
- ripasso sulla ricerca dei massimali con l'uso dei multinsiemi
- ripasso sui sottotermini
- formule del superposition calculus
--- superposition right
--- superposition left
--- equality resolution
--- equality factoring
Il professore ha annunciato una prossima revisione della dispensa del corso per escludere gli argomenti che non verranno trattati e riordinare i restanti nell'ordine in cui sono stati presentati a lezione. |
| Walter |
Argomenti della lezione di Lunedì 29 Novembre
- esercizi con SPASS (opzioni -PObv , -PRew e -Select)
Importanti avvisi dal sito del corso:
- è in linea qui la nuova versione della dispensa;
- Venerdì 3 dicembre alle 9.30 in aula Delta esercitazioni di laboratorio su SPASS
- le lezioni del 30 Novembre (domani) e del 6 Dicembre sono sospese: la prossima lezione si terrà il 13 Dicembre
Grazie a 10t8or per le informazioni! :) |
| Walter |
Argomenti della lezione di Lunedì 13 Dicembre
- regole di riduzione (forward e backward)
--- clausola ridondante e riduzione forward
--- inferenza ridondante e riduzione backward
- nozione di derivazione
Argomenti della lezione di Martedì 14 Dicembre
- sistemi di riscrittura (non è parte del programma d'esame)
Avvisi di fine corso
Martedì 21 Dicembre avrà inizio il corso integrativo facoltativo, che si concluderà con un progetto: questo sostituirà in tutto o in parte (è ancora da stabilire) la consueta procedura d'esame.
Per qualsiasi informazione sul corso, sulle esercitazioni di laboratorio e sul corso integrativo fare riferimento alla pagina http://homes.dsi.unimi.it/~ghilardi/ls/lpa.html |
|
|
|
