|
|
| (3 versioni intermedie di uno stesso utente non sono mostrate) |
| Riga 1: |
Riga 1: |
| − | [[Categoria:Corsi]][[Categoria:Corsi Primo Semestre]]
| + | {{introduzione}} |
| − | <!-- non cancellare le righe precedenti -->
| + | == Turni == |
| − | == Informazioni generali == | + | {{Turno|(Ghilardi)}} |
| | | | |
| − | === Orari delle lezioni === | + | == A.A. passati == |
| | + | {{Annipassati|2005-2006|(Ghilardi)}} |
| | | | |
| − | LUNEDI': 11.30-13.30 (in aula beta)<br>
| + | == Informazioni == |
| − | MERCOLEDI': 9.30-11.30 (in aula beta)<br>
| |
| − | VENERDI' : 9.00 -10.45 (in aula beta)
| |
| | | | |
| − | L'orario del venerdì è effettivo: la lezione inizia alle 9 in punto
| + | Il corso ha anche il nome di '''Logica matematica'''. |
| | | | |
| − | Cercate di essere sempre puntuali! :)
| + | === Giudizio sul corso === |
| | + | {{Giudizio}} |
| | + | {{Giudizio/Interesse}} |
| | + | {{Giudizio/Difficoltà}} |
| | + | {{Giudizio/Nonfrequentanti}} |
| | + | {{Giudizio/Ore}} |
| | | | |
| − | === Orario di ricevimento studenti ===
| + | [[Categoria:Corsi Primo Semestre]][[Categoria:Corsi Magistrale]] |
| − | | |
| − | Attenersi all'orario di ricevimento, evitate telefonate o mail al di fuori dell'orario
| |
| − | | |
| − | === Sito del corso ===
| |
| − | | |
| − | Il sito del corso è:
| |
| − | [http://homes.dsi.unimi.it/~ghilardi/ls/lpa.html] | |
| − | | |
| − | Il sito per il corso integrativo è [http://www.loria.fr/~ranise/milano2006/]
| |
| − | | |
| − | === Videolezioni ===
| |
| − | | |
| − | Le videolezioni sono diponibili a questo indirizzo:
| |
| − | [http://streaming.dico.unimi.it/]
| |
| − | | |
| − | === Materiale didattico ===
| |
| − | | |
| − | - La dispensa reperibile sul sito del prof
| |
| − | - Il dimostratore automatico SPASS scaricabile da Internet secondo le indicazioni presenti sul sito del prof
| |
| − | | |
| − | === Modalità d'esame ===
| |
| − | | |
| − | Orale con presentazione di un proprio esercizio formalizzato in SPASS. Durante l'orale verranno anche fatte domande sulla teoria spiegata a lezione e presente sulla dispensa.
| |
| − | Una modalità alternativa prevedere la presentazione di un progetto. <br>
| |
| − | | |
| − | === Corso integrativo di logica ===
| |
| − | Durante le ore del corso sono previste delle esercitazioni con il dottor Zucchelli e in piu' l'Ingegner Ranise svolge "Metodi formali per la verifica dei protocolli" dal 24 Ottobre circa durante le ore di lezione.
| |
| − | Le prime 2 o 3 lezioni sono obbligatorie, poi facoltative per chi volesse fare l'esame con la modalità alternativa (progetto)
| |
| − | | |
| − | === Rapporto con la laurea triennale ===
| |
| − | Chi avesse fatto come complementare logica matematica durante la laurea triennale, deve obbligatoriamente fare anche questo esame (i programmi sono distinti) <br> Logica matematica e logica per le applicazioni per la specialistica hanno invece lo stesso programma
| |
| − | | |
| − | === Recupero del debito ===
| |
| − | Il professor Ghilardi ha detto che non ha molto senso fare Logica Matematica come complementare della triennale. Se volete fare qualcosa riguardante la logica, contattate il prof e concordate un programma, oppure fate un corso integrativo che partirà più avanti con progetto annesso.
| |
| − | | |
| − | === Altri corsi ===
| |
| − | Al secondo semestre c'è Logica II, un esame a moduli, il cui programma è molto variabile e verrà concordato in seguito
| |
| − | | |
| − | === Iniziative e seminari ===
| |
| − | C'è la possibilità di fare una scuola di Logica sul Lago di Garda per una settimana circa, verso primavera. Possibilità di borse di studio.
| |
| − | | |
| − | == Diario del corso ==
| |
| − | === Lezione di Lunedi' 3-10-05 ===
| |
| − | | |
| − | Sono state presentate le modalità del corso e introdotto cosa è SPASS: un dimostratore automatico, a cui diamo in pasto problemi di logica (basati sulla logica di saturazione per la logica del primo ordine) per vederceli risolti. In pratica, inseriamo le ipotesi e la tesi, e poi SPASS ci comunica se la tesi immessa è effettivamente conseguenza logica delle ipotesi.
| |
| − | | |
| − | Esistono anche altri dimostratori automatici come E (sotto Unix) e Vampire. E' stata progettata da due dottorandi della facoltà un'interfaccia Java che facilita l'inserimento delle clausole (la trovate sul sito del prof, nella parte delle esercitazioni, inserendo la password "jarinterfaccia".
| |
| − | | |
| − | La libreria TPTP contiene una serie di problemi che possono essere risolti con SPASS
| |
| − | | |
| − | === Lezione di Mercoledi' 5-10-05 ===
| |
| − | Sono state introdotte nozioni e definizioni di:
| |
| − | -linguaggio formale
| |
| − | -termine
| |
| − | -enunciato
| |
| − | -ground
| |
| − | | |
| − | e spiegate la differenza tra la logica preposizionale, la logica del primo ordine e la logica di ordini superiori.
| |
| − | | |
| − | Comunque, vi consiglio di guardarvi le videolezioni, sono un validissimo aiuto! ;)
| |
| − | | |
| − | === Lezione di Venerdì 7-10-05 ===
| |
| − | | |
| − | Abbiamo introdotto con esempi il concetto di verità e di conseguenza logica (in particolar modo, la nozione di verità data da Tarski), nonchè dell'interpretazione dei simboli del linguaggio.
| |
| − | | |
| − | === Lezione di Lunedì 10-10-05 ===
| |
| − | | |
| − | Nozione di interpretazione, verità logica e conseguenza logica. Teorema di compattezza. Problema fondamentale della logica
| |
| − | | |
| − | === Lezione di Mercoledì 12-10-05 ===
| |
| − | | |
| − | Dimostratori automatici<br>
| |
| − | Skolemizzazione<br>
| |
| − | Funzionamento ed esempio di problema in SPASS<br>
| |
| − | | |
| − | === Lezione di Venerdì 14-10-05 ===
| |
| − | Operazioni di skolemizzazione: forma normale negativa, forma normale prenessa, skolemizzazione vera e propria e trasformazione in forma normale congiuntiva della matrice, con esempi ed esercizi finali
| |
| − | | |
| − | === Lezione di Lunedì 17-10-05 ===
| |
| − | Esercizi sulla skolemizzazione e introduzione al problema della rilevazione delle contraddizioni
| |
| − | | |
| − | === Lezione di Mercoledì 19-10-05 ===
| |
| − | Teorema dell'unificazione. Concetto di sostituzione simultanea e sequenziale. Definizione di rinomina e di problema di unificazione. Enunciazione delle sei regole per gli algoritmi di unificazione e successivi esempi ed esercizi
| |
| − | | |
| − | === Lezione di Venerdì 21-10-05 ===
| |
| − | Regola di risoluzione di Robinson. Regola di fattorizzazione destra; teorema di completezza refutazionale. Esempi con la skolemizzazione e l'unificazione.
| |
| − | | |
| − | === Lezione di Lunedì 24-10-05 ===
| |
| − | Corso integrativo di logica. Vedi: http://www.loria.fr/~ranise/milano2006/
| |
| − | | |
| − | === Lezione di Mercoledì 26-10-05 ===
| |
| − | Vedi: http://www.loria.fr/~ranise/milano2006/
| |
| − | | |
| − | === Lezione di Venerdì 28-10-05 ===
| |
| − | Continuazione sulla struttura del dimostratore automatico, Regole di Riduzione, Algoritmo della Given Clause con esempi
| |
| − | | |
| − | === Lezione di Lunedì 31-10-05 ===
| |
| − | Nozioni di Logica Tradizionale e Sillogistica Aristotelica. Esempi di sillogismi calcolati con SPASS.
| |
| − | Dispenza scaricabile dal sito del Prof. Minari, Università di Firenze: http://www.philos.unifi.it/persone/minari.htm, sezione Dispense | Logica Tradizionale (log_trad.pdf).
| |
| − | | |
| − | === Lezione di Mercoledi' 02-11-05 ===
| |
| − | Esercizi: abbiamo ricavato la forma logica da un testo, abbiamo ricavato tutti gli assiomi e le congetture e abbiamo testato il risultato con Spass.
| |
| − | | |
| − | === Lezione di Venerdi' 04-11-05 ===
| |
| − | Abbiamo visto il significato di letterali massimali.
| |
| − | Il prof ha spiegato gli ordini di riduzione (KBO e LPO), le proprieta' degli ordinamenti, insiemi di ordine stretto.
| |
| − | Abbiamo visto il prodotto lessicografico e i multinsiemi (inclusione,unione e sottrazione).
| |
| − | Proprieta' degli ordinamenti in ordini stretti > su P terminanti.
| |
| − | | |
| − | === Lezione di Lunedì 07-11-05 ===
| |
| − | Corso integrativo. Vedi: http://www.loria.fr/~ranise/milano2006/
| |
| − | | |
| − | === Lezione di Mercoledi' 09-11-05 ===
| |
| − | Ordini di riscrittura, ordine di riduzione, proprieta' altamente desiderabili (ordini di semplificazione, teorema di Kruskal).
| |
| − | Ordinamenti Lpo con casi da verificare, esempi.
| |
| − | Ordinamenti Kbo con precondizione e casi da verificare, esempi.
| |
| − | | |
| − | === Lezione di Venerdi' 11-11-05 ===
| |
| − | Letterali Massimali e strettamente massimali<br>
| |
| − | Metodo per la definizione dei massimali.<br>
| |
| − | Risoluzione ordinata; factoring ordinato<br>
| |
| − | Soluzione dei letterali negativi<br>
| |
| − | Esempi
| |
| − | | |
| − | === Lezione di Lunedì' 14-11-05 ===
| |
| − | Risoluzione Ordinata con selezione (ripasso)<br>
| |
| − | Factoring ordnato<br>
| |
| − | Albero delle posizioni<br>
| |
| − | Proprietà fondamentali degli alberi<br>
| |
| − | Paramodulazione Destra<br>
| |
| − | Sovrapposizione Destra e Sinistra (SPR e SPL)<br>
| |
| − | Altre regole: equality factoring e regole di riduzione<br>
| |
| − | Esempi
| |
| − | | |
| − | === Lezione di Mercoledi' 16-11-05 ===
| |
| − | Lezione del corso integrativo
| |
| − | [http://homes.dsi.unimi.it/~ranise/lezione4.pdf slides] | |
| − | | |
| − | === Lezione di Venerdi' 18-11-05 ===
| |
| − | Lezione del corso integrativo
| |
| − | [http://homes.dsi.unimi.it/~ranise/lezione5.pdf slides]
| |
| − | | |
| − | === Lezione di Lunedi' 28-11-05 ===
| |
| − | Sovrapposizione destra e sinistra.Regola di risoluzione per l'uguaglianza,factoring per l'uguaglianza.
| |
| − | Regole di riduzione: Regola di riscrittura o demodulazione.
| |
| − | Esempio con Spass.
| |
| − | | |
| − | === Lezione di Mercoledi' 30-11-05 ===
| |
| − | Esercitazione: Assassinio al palazzo di Dreadbury ([http://homes.dsi.unimi.it/~zucchell/teaching/lpalab0506/testi.txt testo]): Formalizzazione ed esecuzione<br>
| |
| − | [http://homes.dsi.unimi.it/~zucchell/teaching/lpalab0506/ Sito di riferimento] | |
| − | | |
| − | === Lezione di Venerdi' 02-12-05 ===
| |
| − | Esercitazione: Assassinio al palazzo di Dreadbury - Analisi dell'esecuzione<br>
| |
| − | [http://homes.dsi.unimi.it/~zucchell/teaching/lpalab0506/ Sito di riferimento]
| |
| − | | |
| − | === Lezione di Lunedì' 05-12-05 ===
| |
| − | nota: ULTIMA LEZIONE del corso<br>
| |
| − | Esempi di superposition<br>
| |
| − | Regola di inferenza, definizione di inferenza ridondante<br>
| |
| − | Definizione di successione di insiemi di clausole
| |
| − | | |
| − | === il corso è terminato ===
| |
