Kurs-pm

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 logik för att formalisera egenskaper hos datastrukturer, algoritmer och datorsystem

att använda språket Prolog

genomföra bevis för att härleda slutsatser utifrån givna premisser

kunna använda olika bevistekniker, såsom naturlig deduktion, induktion. s.k. Hoare-logik för programverifikation, och temporal-logik för systemverifikation

kunna använda logiska formler för att ge en precis matematisk

(modell-teoretisk) innebörd av olika matematiska och datalogiska påståenden

resonera kring viktiga egenskaper hos bevissystem, såsom sundhet, fullständighet och avgörbarhet

motivera och tillämpa metoder för automatisk deduktion som att utföra enkla bevis med modelprövning

Moduler

Kursen är uppdelad i 6 stycken moduler. Dessa moduler täcker in områdena Satslogik, Prolog, Predikatlogik, Rekursion, Temporallogik och Hoarelogik.

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

Det finns 3 obligatoriska laborationer i kursen. Momentet LAB1 består av laboration 1. Momentet LAB2 består av laboration 2 och laboration 3. (Detta arrangemang finns på grund av vissa historiska och ladok-tekniska skäl.)

TEN1 examineras först med en uppsättning av 6 st. quiz som görs i ett slags hybridform. De görs online men i en övervakad datorsal. Quizen motsvarar olika moduler i kursen. För att få betyg E krävs att man har klarat alla 6 quizen. Om man gjort det kan man göra en hemtenta som publiceras i slutet av kursen. Hemtentan skickas in online i canvas. Genom att göra hemtentan kan man höja betyget till A-D.

Hemtentan består av en C-del (som ger betyg D-C) och en A-del (som ger betyg B-A). För att kunna få betyg på A-delen krävs att man har fått betyg C på C-delen.

Bedömningen av hemtenta görs enligt följande mål:

D: Studenten skall delvis uppfylla målen för betyg C

C: Studenten skall kunna tillämpa angivna metoder i kursen för att

lösa medelsvåra och väsentligen nya problem

B: Studenten skall delvis uppfylla målen för betyg B

A: Studenten skall kunna välja och tillämpa metoder I kursen för att

lösa svårare och väsentligen nya problem

För att bli godkänd på kursen krävs att alla momenten TEN1, LAB1 och LAB2 är godkända.

Bonussystem

Det finns ett bonussystem som ger bonuspoäng till quizen.  Det kommer att ges 4 frivilliga hemtal . Godkända hemtal ger bonuspoäng på olika quiz enligt följande:

  • Hemtal 1 - I bonuspoäng på quiz 1
  • Hemtal 2 - 1 bonuspoäng på quiz 3
  • Hemtal 3 - 1 bonuspoäng på quiz 4
  • Hemtal 4 - 1 bonuspoäng på quiz 6

Om labbarna klaras av innan eller på det ordinarie redovisningsdatumet ger de också bonuspoäng på quizen enlig:

  • Lab1 - 1 bonuspoäng på quiz 2
  • Lab 2 - 1 bonuspoäng på quiz 1
  • Lab 3 - 1 bonuspoäng på quiz 5

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