204SM - LOGICA 2018

Schema della sezione

• Seleziona sezione Introduzione

  Introduzione

  Minimizza tutto Espandi tutto

  • Seleziona attività Annunci

    

    Annunci Forum
• Seleziona sezione Programma e materiali del corso, Introduzione al 10.o problema di Hilbert. (5 marzo h.11-13, Aula 5A edif. H2bis)

  Programma e materiali del corso, Introduzione al 10.o problema di Hilbert. (5 marzo h.11-13, Aula 5A edif. H2bis)

  • Seleziona attività Lucidi introduttivi al 10.o problema di Hilbert

    

    Lucidi introduttivi al 10.o problema di Hilbert File PDF
  • Seleziona attività Appunti sul 10.o problema di Hilbert (Dispensa estesa)

    

    Appunti sul 10.o problema di Hilbert (Dispensa estesa) File PDF
  • Seleziona attività Esercizi sul 10.o problema di Hilbert (il primo è svolto all'ultima pagina)

    

    Esercizi sul 10.o problema di Hilbert (il primo è svolto all'ultima pagina) File PDF
  • Seleziona attività Le lezioni delle date 2, 3 aprile e 9, 10 aprile v...

    Le lezioni delle date 2, 3 aprile e 9, 10 aprile verranno tenute in inglese dal prof. Ernst-Erich Doberkat, vedi

    http://www.cs.tu-dortmund.de/nps/de/Home/Personen/D/Doberkat__Ernst-Erich.html

    che tratterà i seguenti temi:

        * Modal logics and Kripke models

        * Expressivity

        * Model morphisms

        * Categories and Coalgebras

        * Bisimulations 

  • Seleziona attività Tre temi fra cui scegliere quello da discutere con il prof. Ernst-Erich Doberkat durante l'esame

    

    Tre temi fra cui scegliere quello da discutere con il prof. Ernst-Erich Doberkat durante l'esame File PDF
• Seleziona sezione Di che si occupa la logica formale? Cos'e`---intesa matematicamente---una logica? (6 marzo h.14-16, Aula 5A edif. H2bis)

  Di che si occupa la logica formale? Cos'e`---intesa matematicamente---una logica? (6 marzo h.14-16, Aula 5A edif. H2bis)

  • Seleziona attività Cenni introduttivi sulla logica formale (Lucidi)

    

    Cenni introduttivi sulla logica formale (Lucidi) File PDF
  • Seleziona attività Cos'e` (intesa matematicamente) una logica? (Lucidi)

    

    Cos'e` (intesa matematicamente) una logica? (Lucidi) File PDF
  • Seleziona attività Cos'e` (intesa matematicamente) una logica? (Dispensa)

    

    Cos'e` (intesa matematicamente) una logica? (Dispensa) File PDF
  • Seleziona attività Esempio (per ora solo accennato): La logica proposizionale 'classica'. (Lucidi)

    

    Esempio (per ora solo accennato): La logica proposizionale 'classica'. (Lucidi) File PDF
• Seleziona sezione Approfondimento sulla semantica della logica proposizionale; riduzione dei suoi enunciati a forma 3CNF. Logiche booleane. (12 marzo h.11-13, Aula 5A, edif. H2bis)

  Approfondimento sulla semantica della logica proposizionale; riduzione dei suoi enunciati a forma 3CNF. Logiche booleane. (12 marzo h.11-13, Aula 5A, edif. H2bis)

  • Seleziona attività Lucidi un po' arricchiti sulla logica proposizionale classica.

    

    Lucidi un po' arricchiti sulla logica proposizionale classica. File PDF
  • Seleziona attività Riduzione di enunciati a forma 3CNF equisoddisfacibile

    

    Riduzione di enunciati a forma 3CNF equisoddisfacibile File PDF
• Seleziona sezione Soddisfacibilita` proposizionale, per formule in 3CNF. Consistenza, logiche booleane e teorema di Lindenbaum (19 marzo, h.11-13, aula 5A edificio H2bis)

  Soddisfacibilita` proposizionale, per formule in 3CNF. Consistenza, logiche booleane e teorema di Lindenbaum (19 marzo, h.11-13, aula 5A edificio H2bis)

  • Seleziona attività Vedi la terza pagina (recentemente aggiunta) della...

    Vedi la terza pagina (recentemente aggiunta) della dispensa della lezione scorsa sulla riduzione a forma 3CNF

  • Seleziona attività Per il resto, proseguire nella lettura dei lucidi ...

    Per il resto, proseguire nella lettura dei lucidi "Cos'è una logica?" del 6 marzo scorso, della dispensa associata agli stessi e del Capitolo 1 delle `Lecture Notes in Logic' di Martin Davis, 1993.

  • Seleziona attività Approfondimento suggerito: Documentarsi sul lemma ...

    Approfondimento suggerito: Documentarsi sul lemma di Zorn e ri-dimostrare per suo tramite il teorema di Lindenbaum, senza l'ipotesi semplificatrice impiegata nei lucidi e nella dispensa del corso.

• Seleziona sezione Logiche booleane minimali e teorema di Post. Un linguaggio di programmazione 'a registri' Turing-completo. (20 marzo 2019, h.14-16, aula 5A)

  Logiche booleane minimali e teorema di Post. Un linguaggio di programmazione 'a registri' Turing-completo. (20 marzo 2019, h.14-16, aula 5A)

  • Seleziona attività Proseguire nella lettura dei lucidi "Cos'è una log...

    Proseguire nella lettura dei lucidi "Cos'è una logica?" del 6 marzo scorso, della dispensa associata agli stessi e del Capitolo 1 delle `Lecture Notes in Logic' di Davis del 1993.
    

  • Seleziona attività Lucidi in versione provvisoria, che per ora coprono un linguaggio di programmazione "a registri" Turing-completo

    

    Lucidi in versione provvisoria, che per ora coprono un linguaggio di programmazione "a registri" Turing-completo File PDF
• Seleziona sezione Gödelizzazione e diagonalizzazione (26 marzo 2019, h.11-13 aula 5A edificio H2bis)

  Gödelizzazione e diagonalizzazione (26 marzo 2019, h.11-13 aula 5A edificio H2bis)

  Gödelizzazione e diagonalizzazione

  • Seleziona attività Dispensetta su di un insieme ricorsivamente enumerabile che non è decidibile

    

    Dispensetta su di un insieme ricorsivamente enumerabile che non è decidibile File PDF
  • Seleziona attività Dall'abbinamento alla codifica di sequenze

    

    Dall'abbinamento alla codifica di sequenze File PDF

    Qui sopra si trova un esempio di Gödelizzazione, applicato alle equazioni diofantee; però in Dropbox trovate un'estesa trattazione su 'lucidi' del tema "Dall'abbinamento alla codifica di sequenze".

  • Seleziona attività Una conseguenza sorprendente del teorema DPR come ridimostrato da Matiyasevich nel 1974

    

    Una conseguenza sorprendente del teorema DPR come ridimostrato da Matiyasevich nel 1974 File PDF
• Seleziona sezione Completamento di qualche punto lasciati in sospeso nelle recenti lezioni (27 marzo 2019, h.14-16 aula 5A)

  Completamento di qualche punto lasciati in sospeso nelle recenti lezioni (27 marzo 2019, h.14-16 aula 5A)

  • Seleziona attività Versione completa dei lucidi sul teorema DPR presentati due lezioni fa

    

    Versione completa dei lucidi sul teorema DPR presentati due lezioni fa File PDF
  • Seleziona attività Elencazione di tutte le sequenze di enunciati che formano dimostrazioni nel calcolo proposizionale 'standard'

    

    Elencazione di tutte le sequenze di enunciati che formano dimostrazioni nel calcolo proposizionale 'standard' File PDF
  • Seleziona attività Completare la lettura dei lucidi "Cos'e` una logic...

    Completare la lettura dei lucidi "Cos'e` una logica?" esposti tra il materiale del 6 marzo

• Seleziona sezione Modulo "Introduction to modal logics and their coalgebraic interpretation" svolto dal prof. E.-E. Doberkat nelle date 02/04, 3/04 e 09/04, 10/04 2019, usuale orario e luogo

  Modulo "Introduction to modal logics and their coalgebraic interpretation" svolto dal prof. E.-E. Doberkat nelle date 02/04, 3/04 e 09/04, 10/04 2019, usuale orario e luogo

  AVVISO! La lezione del 3 aprile iniziera` alle 13:15 anzichè alle 14:15

  • Seleziona attività La lezione del 10 aprile subirà la stessa anticipa...

    La lezione del 10 aprile subirà la stessa anticipazione di orario.

  • Seleziona attività Appunti sulla materia, scritti dal prof. Doberkat

    

    Appunti sulla materia, scritti dal prof. Doberkat File PDF
• Seleziona sezione I linguaggi interpretati che soggiacciono alla logica predicativa del prim'ordine (16 aprile 2019, h.11-13 & 17 aprile 2019, h.14-16. Aula 5A edificio H2bis)

  I linguaggi interpretati che soggiacciono alla logica predicativa del prim'ordine (16 aprile 2019, h.11-13 & 17 aprile 2019, h.14-16. Aula 5A edificio H2bis)

  • Seleziona attività Qualche teoria assiomatica del prim'ordine

    

    Qualche teoria assiomatica del prim'ordine File PDF

    Come motivazione di partenza, vengono presentate tre teorie assiomatiche:

    1. teoria elementare dei gruppi
    2. aritmetica di Dedekind-Peano
    3. teoria  degli insiemi di Vaught

    Qualche cenno su problematiche meta-logiche che le riguardano:

    1. equipollenza di sistemi di assiomi differenti (perfino nel linguaggio in cui vengono enunciati), indecidibilità
    2.  assiomatizzabilità finita, indecidibilità essenziale
    3. indecidibilità essenziale in un contesto ridotto "all'osso", che verrà esteso in una teoria in grado di fungere da fondamento per  l'intero corpus delle discipline matematiche

  • Seleziona attività Linguaggi predicativi del prim'ordine

    

    Linguaggi predicativi del prim'ordine File PDF

    Come ulteriore esempio motivante, viene presentata---nella versione assiomatica del 1967---la geometria elementare di Tarski; poi vengono proposti lessico, sintassi, semantica di un generico linguaggio predicativo del prim'ordine. Per ora non viene proposto alcun apparato deduttivo: una volta aggiunto anche quello, saremo appieno dentro il calcolo predicativo del 1.o ordine, adatto a far da supporto a un'infinità di teorie, rilevanti sia per la matematica che per la programmazione dichiarativa. 

  • Seleziona attività semantica dei linguaggi della logica predicativa del 1.o ordine

    

    semantica dei linguaggi della logica predicativa del 1.o ordine File PDF
• Seleziona sezione Assiomi di una teoria degli insiemi (30 aprile 2019, h.11--13, aula 5A edif. H2bis)

  Assiomi di una teoria degli insiemi (30 aprile 2019, h.11--13, aula 5A edif. H2bis)

  • Seleziona attività Una versione assiomatica della teoria degli insiemi di Zermelo-Fraenkel (riporta anche, alla fine, l'assioma di finitezza di Tarski)

    

    Una versione assiomatica della teoria degli insiemi di Zermelo-Fraenkel (riporta anche, alla fine, l'assioma di finitezza di Tarski) File PDF
  • Seleziona attività Traduzione di formule della logica predicativa del 1.o ordine nella versione algebrica della logica diadica

    

    Traduzione di formule della logica predicativa del 1.o ordine nella versione algebrica della logica diadica File PDF
• Seleziona sezione Calcolo predicativo del prim'ordine (7 maggio, h.11-13, aula 5A edif. H2bis; 8 maggio, h.13-16, aula 5A edif. H2bis)

  Calcolo predicativo del prim'ordine (7 maggio, h.11-13, aula 5A edif. H2bis; 8 maggio, h.13-16, aula 5A edif. H2bis)

  • Seleziona attività Dalla formulazione del calcolo predicativo del prim'ordine fino al teorema di completezza che assicura la derivabilità di tutte le conseguenze logiche (in senso semantico) da/di un insieme di premesse

    

    Dalla formulazione del calcolo predicativo del prim'ordine fino al teorema di completezza che assicura la derivabilità di tutte le conseguenze logiche (in senso semantico) da/di un insieme di premesse File PDF

    In precedenza abbiamo visto (e prima di guardare questi lucidi richiameremo) la definizione di sintassi e semantica della logica predicativa: fin qui avevamo definito, in tutto, un linguaggio interpretato. Ora forniremo una versione del calcolo, cioè introdurremo una nozione di derivabilità che riguarda gli enunciati del linguaggio in questione. 

    Gioca un ruolo importante, nella verifica che il linguaggio predicativo diventa, una volta  che lo si sia munito anche dell nozione di derivabilità, una logica booleana: il teorema di deduzione.

    La piena rispondenza fra calcolo e semantica si basa su due teoremi: correttezza (in inglese 'soundness') e completezza. Il primo ci garantisce che da un insieme E di enunciati  non possiamo derivare altro che 'conseguenze logiche'  (questa locuzione riguarda la semantica) di E: dunque il calcolo non largheggia indebitamente. Il secondo ci assicura che tutte le conseguenze logiche di E sono derivabili da E: dunque al calcolo non manca nulla.

    Entrano in gioco, nel corso della dimostrazione,  interpretazioni di Herbrand, il cui dominio è interamente costituito di termini. Importante anche un meccanismo definitorio dovuto a Skolem e perciò chiamato skolemizzazione.

  • Seleziona attività Due esercizi sui linguaggi predicativi del 1.o ordine

    

    Due esercizi sui linguaggi predicativi del 1.o ordine File PDF
• Seleziona sezione Completezza del calcolo predicativo del 1.o ordine (14 maggio, h.11-13, aula 5A edif. H2bis; 15 maggio, h.13-15, aula 5A edif. H2bis)

  Completezza del calcolo predicativo del 1.o ordine (14 maggio, h.11-13, aula 5A edif. H2bis; 15 maggio, h.13-15, aula 5A edif. H2bis)
• Seleziona sezione Avviso sulla calendarizzazione delle ultime lezioni e sulle date d'esame.

  Avviso sulla calendarizzazione delle ultime lezioni e sulle date d'esame.

  Le ultime lezioni sono previste nelle seguenti date / orari:

  Mercoledì 15 maggio, h.13:00/15:00

  Venerdì 17 maggio, h.9:00/11:00

  Martedì 21 maggio, h.11:00/13:00

  Mercoledì 22 maggio Lezione annullata

  Martedì 28 maggio, h.11:00/13:00

  Mercoledì 29 maggio, h.13:00/16:00

  Venerdì 31 maggio, h.9:00/11:00

  Gli appelli estivi d'esame sono previsti nelle seguenti date / orari:

           17 Giugno, h.10:00
  

            4 Luglio,    h.10:00

           25 Luglio, h.10:00
  
  
• Seleziona sezione Programmazione tramite clausole di Horn (17 maggio, h.9:00/11:00, aula 4C edif. H2bis; 21 maggio, h.11:00/13:00, aula 5A edif. H2bis)

  Programmazione tramite clausole di Horn (17 maggio, h.9:00/11:00, aula 4C edif. H2bis; 21 maggio, h.11:00/13:00, aula 5A edif. H2bis)

  • Seleziona attività Linguaggi clausolari, clausole di Horn e modello minimo. (Lucidi)

    

    Linguaggi clausolari, clausole di Horn e modello minimo. (Lucidi) File PDF
  • Seleziona attività Clausole di Horn e computabilità. (Lucidi)

    

    Clausole di Horn e computabilità. (Lucidi) File PDF
  • Seleziona attività Completezza di Turing della programmazione tramite clausole di Horn. (Dispensa)

    

    Completezza di Turing della programmazione tramite clausole di Horn. (Dispensa) File PDF
• Seleziona sezione Clausole di Horn, modello minimo, domande e risposte; Programmazione tramite clausole e tramite regole di produzione grammaticale in Prolog (28 maggio, h.11:00/13:00, aula 5A edif. H2bis; 29 maggio, h.13:00/15:00, aula 5A edif. H2bis)

  Clausole di Horn, modello minimo, domande e risposte; Programmazione tramite clausole e tramite regole di produzione grammaticale in Prolog (28 maggio, h.11:00/13:00, aula 5A edif. H2bis; 29 maggio, h.13:00/15:00, aula 5A edif. H2bis)

  • Seleziona attività Esempietto di programma Prolog

    

    Esempietto di programma Prolog File PRO
  • Seleziona attività Semplici esempi di grammatiche espresse tramite produzioni in Prolog

    

    Semplici esempi di grammatiche espresse tramite produzioni in Prolog File PRO
• Seleziona sezione Indecidibilità della logica predicativa: teorema di Church applicato alle basi di clausole di Horn (31 maggio, h.9:00/12:00, aula 4B edif. H2bis)

  Indecidibilità della logica predicativa: teorema di Church applicato alle basi di clausole di Horn (31 maggio, h.9:00/12:00, aula 4B edif. H2bis)

  • Seleziona attività Lucidi sul teorema di Church nella versione riguardante le clausole di Horn

    

    Lucidi sul teorema di Church nella versione riguardante le clausole di Horn File PDF