Laurea in Informatica

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

• Docente: prof. Giuseppe Rosolini (email: rosolini at disi.unige.it)
  
• Informazioni generali: Descrizione, Programma, Testi di Riferimento. Informazioni sulle prove d'esame,

Descrizione

Programma

• Richiami di logica del prim'ordine
  • Conseguenza logica
  • Equivalenza logica
• Dimostrazioni formali
  • Teorie
  • Sistemi formali per la dimostrazione: deduzione naturale, calcolo dei sequenti di Gentzen
  • Diagrammi semantici
  • Teorema di correttezza
  • Teorema di completezza
• Applicazioni della logica del prim'ordine
  • Modelli di Herbrand e risoluzione
  • Teoria dei numeri, teorema di incompletezza

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

• conseguenze logiche ed equivalenze
• confutazione con il metodo dei diagrammi semantici
• le regole derivate per il calcolo della Deduzione Naturale
• il calcolo della Deduzione Naturale

Informazioni sul lavoro da svolgere

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:
   
   • Nome e Cognome dello studente nella prima riga
   • a seguire, tutte le conseguenze che non si è riusciti a verificare, usando la scrittura per esteso ogni volta, evitando le denominazioni quali associativa, De Morgan, ecc.
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:
   
   • il nome del file consiste della stringa alfabetica ottenuta concatenando il cognome dello studente con la prima lettera del suo nome
   • le dimostrazioni salvate nel file sono delle conseguenze (e equivalenze) che si è riusciti a verificare, facendo attenzione a non aggiungere condizioni al contorno. NB: segnaliamo in quali conseguenze e equivalenze compaiono sin condizioni al contorno:

     • Equivalenze	counita' per ?	x non libera in P
       	Beck-Chevalley per ?	x non libera in Q
       	unita' per !	x non libera in P
       	Beck-Chevalley per !	x non libera in Q
       Equivalenze utili	P=>(!x.Q) l=| !x.(P=>Q)	x non libera in P
       	(?x.Q)=>P l=| !x.(Q=>P)	x non libera in P
       	P=>(?x.Q) l=| ?x.(P=>Q)	x non libera in P
       	(!x.Q)=>P l=| ?x.(Q=>P)	x non libera in P
       Calcolo di Hilbert	(A5)	x non libera in P

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 U¹) sono tali da rendere f_*[[P]] vuoto e di quali letture sono tali da renderlo tutto U⁰, dove f è l'unica funzione da U a U⁰.
   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.