Differenze tra le versioni di "Logica per le applicazioni"

Da WikiDsy.
 
(5 versioni intermedie di 2 utenti non 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 ===
 
>>dopo una pausa di 1 settimana per assenza del prof c'è stata lezione, ma non ho appunti, chi può aggiorni<<
 
 
 
=== 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 ===
 

Versione attuale delle 11:51, 10 ott 2006

Disambigua compass.PNG
Questa è una pagina di introduzione al corso: contiene i turni, le modalità d'insegnamento, alcune informazioni generali ed eventuali giudizi sul corso in questione. Se sei giunto qui passando da un link, puoi tornare indietro e correggerlo in modo che punti direttamente alla voce appropriata.

Turni

A.A. passati

Informazioni

Il corso ha anche il nome di Logica matematica.

Giudizio sul corso

I giudizi di seguito espressi sono il parere personale degli studenti,
e potrebbero non rispecchiare il parere medio dei frequentanti.
Non vi è comunque alcun intento di mettere alla gogna i docenti del corso!
Interesse della materia (da 1 a 5 - aiuto)
____________________
Difficoltà del corso (da 1 a 5 - aiuto)
____________________
Difficoltà del corso per non frequentanti (da 1 a 5 - aiuto)
____________________
Ore di studio richieste (da 1 a 5 - aiuto)
____________________