Logik och bevisteknik
    UPPSALA UNIVERSITET
    Matematiska institutionen
    Vera Koponen

    Logik och bevisteknik I, vt 2009

    Allmän information

    • Lärare: Vera Koponen, föreläsningar, lektioner (vera@math.uu.se, 018-471 31 85, Ångströmlaboratoriet, rum 14234), och Anton Hedin, lektioner.
    • Kurslitteratur: Language, Proof and Logic av J. Barwise och J. Etchemendy, CSLI Publications, inklusive CD-skiva med programvaran LPL som ingår i kurslitteraturpaketet.
    • Ditt schema kan du söka på nätet: http://www.teknat.uu.se/student/schema/
    • Information om hur examinationen går till finns längre ner på sidan.
    • Formell kursplan.
    • Lite information om logik och logikkurser vid matematiska institutionen finns här.
    • Wikipedias artiklar om logik och matematisk logik.
    • Fler logikrelaterade länkar, inklusive några tillämpningar, finns längre ner på sidan.

    Stenciler

    • Semantiska träd.
    • En illustration av hur satslogik kan tillämpas.
    • Formella bevis med 'och', 'eller' och 'icke': exempel/övningar med lösningar.
    • Formella bevis där dessutom konnektivet 'implikation' förekommer: exempel/övningar med lösningar.
    • Fler formella bevis, där även 'ekvivalens' dyker upp.
    • Booleska funktioner och konnektiv.
    • Boolesk algebra.
    • Sundhets- och fullständighetssatserna för satslogiken: en skiss av beviset för sundhetssatsen.
    • Satslogiska slutledningar: övningar.
    • Övningar rörande strukturer/modeller och sanning eller falskhet av satser i dessa, och svar/lösningar till övningarna.

    Undervisning

    Undervisningen består av 17 föreläsningar samt 5 lektioner (alltid dubbeltimmar). Föreläsningarna kommer att innehålla såväl teori, dvs introduktion av nya begrepp, metoder och resultat, som behandling av exempel och problemlösning. På lektionerna skall ni i huvudsak arbeta själva, under lärarhandledning, med uppgifter som anges i lektionsplaneringen nedan. OBS! Ni behöver lägga ner betydligt mer tid på eget arbete än den (lilla) tid som ges på de fem lektionerna.
    • Ungefärlig föreläsningsplan.
    • Lektionsplanering med rekommenderade övningsuppgifter.

    Examination

    Betygen som ger godkänt på denna kurs är 3, 4 och 5.

    För betyg 3 finns två vägar:
    En väg är att bli godkänd på punkterna 1 och 2 nedan.
    Alternativt så kan man få betyg 3 genom att bli godkänd på punkt 2 och 3 nedan (och behöver då inte göra punkt 1).

    För att få betyg 4 eller 5 så finns också två möjligheter:
    Antingen genom att bli godkänd på punkt 1 och punkt 2 och sedan så beror betyget på hur många poäng man uppnår på uppgifterna 6-9 på den skriftliga salstentamen som är punkt 3 nedan (och i detta fall behöver man inte göra uppgifterna 1-5 på samma tentamen).
    Alternativt så blir man godkänd på punkt 2 och blir godkänd och uppnår tillräckligt många poäng i punkt 3; i detta fall måste man bli godkänd på uppgifterna 1-5 i denna salstentamen.

    Observera att punkt 1 av examinationen (om ni väljer denna väg, som rekommenderas) är löpande, dvs. ni rekommenderas under kursens gång lösa uppgifter med hjälp av LPL som rättas av Grade Grinder och sedan skickas till er lektionslärare; det finns fyra deadlines; mer information nedan.

      1. Examinationsuppgifter som görs med LPL. Här finns information om dessa. Notera att det finns fyra deadlines.

      2. Muntlig examination: Vi försöker att klara av så många muntliga examina som möjligt under 2-3 dagar i slutet av maj eller början av juni. Mer detaljerad information om tidpunkt anges här och på föreläsningstid mot slutet av kursen. På den muntliga examinationen skall ni kunna redogöra för grundläggande begrepp från kursen, och tar 10-15 minuter per person. Information om vad ni skall kunna på den muntliga examen.

      3. Skriftlig tentamen, den 3 juni. Se tentamensschemat på internet för klockslag och plats. Information om den skriftliga tentamen. Gamla tentor finns längre ner på sidan.

    Logikrelaterade länkar, inklusive några tillämpningar

    • Olika framställningar av de 16 binära konnektiven.
    • Logikens, eller kanske snarare konnektivens, geometri.
    • En sida med diverse program som löser logikrelaterade problem och kan användas online.
    • En sida varifrån man kan ladda ner en automatiserad bevis och (mot)modellsökare för första ordningens logik.
    • Logikprogrammering.
    • Formella metoder: att bevisa att komplexa system gör det de ska, och inte det de absolut inte får göra. På engelska. Mer grundläggande och på svenska.
    • Artificiell intelligens.
    • Venn-diagram på hög nivå.
    • Wikipedias artikel om de komplexitetsteoretiska klasserna P och NP som tar upp relationen mellan logik och frågan om P = NP.
    • Introduktionen till detta examensarbete, Short proofs of finite instances of valid sentences, ger lite inblick i sambandet mellan formella bevissystem och frågan om den komplexitetsteoretiska klassen NP är sluten under komplement, vars svar fortfarande är okänt.
    • Formella system från ett mer generellt perspektiv.

    Gamla tentor

      Tentamen 2009-08-20.
      Tentamen 2009-06-03 med lösningar.
      Tentamen 2008-08-22 med lösningar.
      Tentamen 2008-06-02 med lösningar.

    21 augusti, 2009, Vera Koponen.