Logica per le applicazioni
Informazioni generali
Orari delle lezioni
LUNEDI': 11.30-13.30 (in aula beta)
MERCOLEDI': 9.30-11.30 (in aula beta)
VENERDI' : 9.30 -11.30 (in aula delta)
Cercate di essere puntuali! :)
Orario di ricevimento studenti
Attenersi all'orario di ricevimento, evitate telefonate o mail al di fuori dell'orario
Sito del corso
Il sito del corso è: [1]
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.
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)
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à concorato 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 librerai 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! ;)