|
|
(20 versioni intermedie di 9 utenti non mostrate) |
Riga 1: |
Riga 1: |
− | == Informazioni generali == | + | {{introduzione}} |
| + | == Turni == |
| + | {{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] | |
− | | |
− | === 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 ("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 ===
| |