Logik för dataloger, logik09

Kontrollskrivningar

Kontrollskrivningarna har syftet att kolla pågående inlärningen under kursen. Om man har klarat en kontrollskrivning (betyg E eller bättre) blir man friad från en viss uppgift på respektive kursdel på skriftliga sluttentan.  Åtminstone C på två kursdelar behövs för att kunna gå till muntliga komplementeringstentan (se förklaringen på huvudsidan).

Betygssättning Kontrollskrivningarna är i 90 minuter och består av 3 delar: en E-del, en C-del och en A-del. C-delen blir bara rättad om E-delen blir godkänd (G). Likadant, A-delen blir bara rättad om C-delen blir godkänd. Om C-delen blir nästan godkänd (NG), kommer A-delen inte att rättas och betyget blir D. Om A-delen blir nästan godkänd (NG) blir betyget i så fall B.

Nr.	Datum	Kursdel	Boken	Utdelat
1	15/4 (Ö4)	Satslogik, predikatlogik	1.1, 1.2, 1.4, 2.1 - 2.5	KS1
2	5/5 (Ö7)	Prolog, Induktion, Temporallogik	1.4.2, 1.4.3, 3.1, 3.4	KS2

Vanligaste felen i KS2:

• På 2a har många glömt att predikatet conc tar två listor som argument (bokstäver fungerar inte). Som konsekvens har många till slut fått fram cons(b,a), som inte kan vara en korrekt lista, eftersom a inte är en lista.
• På 2c är induktionen bara över strukturen av listan u.
  
• På 3a har många inte insett att det räcker att man kan hoppa till ett tillstånd där p är sant för att EX p ska vara sant i en stig. De tror att stigen själv måste innehålla ett tillstånd där p är sant.

---

Kontrollskrivning 1. Satslogik, Predikatlogik

Kontrollskrivningen kommer att bestå av flera problem av typen redan betraktad på föreläsningarna och/eller övningarna, inklusive hemtalen. Ett formelblad med reglerna i naturlig deduktion och predikatlogikens semantik  kommer att delas ut under kontrollskrivningen.

Del E

• Enkla bevis i Naturlig deduktion
• Sanningsvärdestabell
• Valueringar och motvalueringar
• Formalisering i sats- och predikatlogik
  

Del C

• Svåra bevis i Naturlig deduktion
• Fria och bundna variabler, variabelinfångande, substitution

Del A

• Svårare bevis i Naturlig deduktion
• Evaluering av predikatlogiska formler i modeller och omgivningar

---

Kontrollskrivning 2.  Prolog, Induktion, Temporallogik

Kontrollskrivningen kommer att bestå av flera problem av typen redan betraktad på föreläsningarna och/eller övningarna, inklusive hemtalen. Ett formelblad med reglerna för CTL modellprovning kommer att delas ut under kontrollskrivningen.

Del E

• Prolog: kunna förstå kod för predikat för listor och enklare databaser och kunna föreslå modifieringar
• Induktiva definitioner över termmängder definierade med BNF
  
• Temporallogik: gäller en formel i CTL i ett visst tillstånd, argumentera
  

Del C

• Prolog: kunna konstruera predikat för listor och enklare datastrukturer
• Enklare bevis med strukturell induktion
• Temporallogik: är två formler i CTL ekvivalenta, argumentera
  
• CTL modellprovning: enklare bevis
  

Del A

• Svårare bevis ned strukturell induktion
• CTL modellprovning: svårare bevis
  

---