Kurs-pm

Samband med gamla logikkursen

Denna kurs DD1351 är som den gamla kursen DD1350 förutom att vi har lagt till en introduktion till språket Prolog. Denna del omfattar 4 föreläsningar, en labb och en övning. Med anledning av detta kurspoängen ökat till 7,5 hp och ett ladokmoment (första labben) har tillkommit.

Kursbeskrivning

Kursen ger en introduktion till matematisk logik och dess tillämpningar inom datalogi. Du får lära dig:

  • använda logik för att formalisera egenskaper hos datastrukturer, algoritmer och datorsystem
  • genomföra bevis för att härleda slutsatser utifrån givna premisser
  • behärska olika bevistekniker, såsom naturlig deduktion, induktion. s.k. Hoare-logik för programverifikation, och temporal-logik för systemverifikation
  • förstå hur logiska formler kan ges en precis matematisk (modell-teoretisk) innebörd
  • behärska grunderna för automatisk deduktion
  • förstå och resonera kring viktiga egenskaper hos bevissystem, såsom sundhet, fullständighet och avgörbarhet
  • att använda språket Prolog

 

Kursmål

Studenterna skall lära sig att:

      • använda sig av logik för att formalisera allmänna egenskaper av datalogiska strukturer samt program- och systemegenskaper 
      • behärska olika bevistekniker:
        • naturlig deduktion
        • induktion
        • program- och systemverifikation
      • behärska grunderna till automatisk deduktion

      • tillämpa och förklara grundläggande begrepp inom logikprogrammering: unifiering, backtracking, snitt, negering och olika programmeringstekniker som t.ex. generate-test”

       

      Efter kursen skall studenterna kunna:

            • formalisera och genomföra bevis:
              • av allmänna egenskaper av datalogiska strukturer:
                • naturlig deduktion i satslogik och predikatlogik
                • motivera och genomföra bevis med strukturell induktion
              • av programegenskaper: Hoares logik
              • av systemegenskaper: Temporallogik
            • argumentera för korrektheten hos en viss bevisteknik: sundhet och fullständighet
            • motivera och tillämpa metoder för automatisk deduktion:
              • utföra enkla bevis med modelprövning
              • argumentera för olika bevisteknikers lämplighet till automatisk deduktion: avgörbarhet

            Examination

            Kursen har tre obligatoriska moment i Ladok:

            • LAB1 - Laboration, 1,5, betygsskala: P, F
            • LAB2 - Laborationer,  2,0 betygsskala: P,F
            • TEN1 - Tentamen, 4,0, betygsskala: A, B, C, D, E, FX, F

            Bonussystem

            Kursen examineras bland annat genom en tentamen, och till denna tentamen kan man få bonuspoäng och tillgodoräknade uppgifter på följande sätt:

            • 4 st frivilliga hemtal; ger maximalt 1 poäng/hemtal på tentans E-del
            • 3 st laborationer; ger 1 poäng på tentans E-del för varje labbrapport som ges omdömet VG och som redovisas i tid
            • Det kommer att ske en frivillig kontrollskrivning (KS):
              • KS-en kan ge E eller C (eller F) i betyg
              • Betyg E på KS-en gör att uppgift 1 på tentans E-del är godkänd (motsvarar 4p på tentan)
              • Betyg C på KS-en gör att uppgift 1 på tentans C-del är godkänd (motsvarar 4p på tentan)

            Maximalt kan man alltså ha 7p plus en tillgodoräknad uppgift på tentans E-del, och en tillgodoräknad uppgift på tentans C-del redan innan man börjar skriva. Det lönar sig alltså att hänga med under kursen!

            OBS! Dina bonuspoäng gäller för tentan och omtentan under denna kursomgång, och försvinner sedan för alltid!