DISI Laurea in Informatica


Corso di Logica Matematica - a.a. 2004/05


Descrizione

Lo scopo del corso è di offrire i risultati fondamentali della logica matematica chiarendo come il calcolo logico sia ausiliario alle altre materie. Si provvede dunque a fissare l'intuizione di che cosa sia una dimostrazione corretta, basata su regole generali prefissate, presentando modi per produrre dimostrazioni e controesempi mediante modelli.

Programma


Testi di riferimento

M. Ben-Ari
Logica matematica per l'informatica, Prentice Hall International, 1998
J. Barwise, J. Etchemendy
The language of first order logic, Cambridge University Press, 1993
E. Mendelson,
Introduzione alla logica matematica, Boringhieri, 1972
G. Rosolini,
Lucidi usati nel corso (aggiornati al 24/2)
G. Rosolini,
Calcoli formali (aggiornati al 30/5) da usare con JAPE per
Un sito mirror non ufficiale (in caso di difficoltà con il sito ufficiale di JAPE) è http://users.comlab.ox.ac.uk/bernard.sufrin/JAPE/jape.org/index.html


Informazioni sul lavoro da svolgere

Per ottenere il riconoscimento dei 3 crediti formativi del corso, è richiesta la partecipazione attiva alle lezioni (o l'equivalente lavoro di recupero) insieme con lo svolgimento dei compiti connessi alla partecipazione. Chiaramente, questi si svolgono settimana per settimana e richiedono circa due o tre ore in totale.

In dettaglio, vengono elencati di seguito, aggiornati di settimana in settimana:

  1. Spedire al docente prima del 3 marzo un messaggio con argomento "settimana1" e che contiene un elenco formato nel modo seguente:
  2. Spedire al docente prima del 17 marzo un messaggio con argomento "settimana2" e che ha come allegato un file di dimostrazioni ottenuto con JAPE con le seguenti caratteristiche:
  3. Spedire al docente prima del 31 marzo un messaggio con argomento "settimana3" il cui testo contiene esempi che mostrano che le due conseguenze qui sotto non sono corrette:
    ((~A)=>(~B))& A l= B
    ~(A&B) l= (~A)&(~B)
    Il testo deve contenere anche i valori di A, B, C che non rendono corretta la conseguenza C & A l= B ed i valori di A, B, C che non rendono corretta la conseguenza C l= A => B. Si noti che questi sono gli stessi, così da verificare che
    C & A l= B se e solo se C l= A => B.
  4. Spedire al docente prima del 7 aprile un messaggio con argomento "settimana4" il cui testo contiene
    1. il risultato del calcolo di
      f[0]  f[X]  f*[0]  f*[X]
      per una generica funzione f:X-> Y.
    2. la determinazione di quali letture di un'affermazione P (come sottoinsieme di U1) sono tali da rendere f*[[P]] vuoto e di quali letture sono tali da renderlo tutto U0, dove f è l'unica funzione da U a U0.
    3. la determinazione della correttezza o meno delle conseguenze
      • ?x. (P => Q(x)) l= P -> !x. Q(x), con x non libera in P
      • ?x. Q(x) l= Q(x)
      Per ciascuna conseguenza, a secondo della risposta, si deve allegare il file pdf della dimostrazione di correttezza fatta usando la teoria LaB.jt in JAPE, oppure si deve scrivere nel testo del messaggio la presentazione dell'universo U e delle letture che non verificano la conseguenza. Per ciascuna conseguenza, a secondo della risposta, si deve allegare il file pdf della dimostrazione di correttezza fatta usando la teoria LaB.jt in JAPE, oppure si deve scrivere nel testo del messaggio la presentazione dell'universo U e delle letture che non verificano la conseguenza.
  5. Spedire al docente prima del 28 aprile un messaggio con argomento "settimana5" il cui testo elenca tutte le conseguenze corrette contenute nell'elenco di 8 possibili conseguenze del pannello "Problemi" della teoria H.j da aprire dopo aver caricato LaB.jt.
  6. (Esercitazione facoltativa) Spedire al docente prima del 24 maggio un messaggio con argomento "settimana6" il cui testo descrive la dimostrazione (magari allegando il file pdf della dimostrazione ottenuta) dell'ultima conseguenza nel pannello "Il calcolo della Deduzione Naturale di Gentzen", disponibile caricando G.j (nella teoria LaB.jt, con l'eventuale aggiunta di H.j).
    Sperimentare il calcolo della Deduzione Naturale, aiutandosi con le note esplicative.
La prova finale consiste in una diretta verifica del lavoro svolto durante il corso.
Date per la prova finale: 23 giugno 2005, ore 9:00, 11 luglio 2005, ore 15:00, 22 settembre 2005, ore 10:00, ?? ottobre 2005, ore ??:??,