Logik för dataloger, logik09

---

Senaste Nytt

• Här är omtentan från augusti 2009 och lösningen. Omtentorna är deponerade hos CSC-skolans studentexpedition.
  
• Här är tentan och lösningen. Tentorna är deponerade hos CSC-skolans studentexpedition.
  
• Här är kursplanen.

---

Examination

Skriftlig tentamen (OBS: ingen anmällan nödvändig!)

Kursen betraktas att bestå av tre delar:

1. Satslogik, Predikatlogik
2. Prolog, Induktion, Temporallogik
3. Hoare-logik

Skriftliga tentan blir tisdagen den 26 maj kl. 14-16 i ett antal övningssalar: D32, D34, D35, D41, D42, E32, E33, E34, E35, E36. Den kommer att bestå av 7 uppgifter:

• Del 1: två uppgifter på E-nivå
• Del 2: två uppgifter på E-nivå
• Del 3: två uppgift på E-nivå och en på C-nivå
  

Om man har klarat första kontrollskrivningen är man friad från första uppgiften i del 1, och om man har klarat andra kontrollskrivningen är man friad från första uppgiften i del 2. Bonuspoängen från hemtalen räknas till godkännt på respektive kursdel. Se modelltentan för mer information.

Själva tentan är följd av obligatorisk kamraträttning (ca. 1 timme) i sal F1:

• Man rättar anonyma tentor så den personliga integriteten hotas inte.
• Rättningen görs tillsammans under en rättningssession då tentans  lösningar och bedömningsmallen gås igenom. Man kan fråga om  oklarheter, och om man ändå är osäker på bedömningen av en uppgift så  kan man ange det. 
• Lärarteamet går igenom alla tentor efter kamraträttningen.
• Resultaten kommer att publiceras dagen efter.
  

Muntlig komplettering

Åtminstone C på två kursdelar och godkänd på tentan behövs för att kunna gå till muntliga komplementeringstentan.
 
Muntliga kompletteringen kommer att äga rum tisdagen den 2 juni (och dagen efter, vid behov) i en av våra seminariesalar. Vi kommer att använda sig av samma bokningssystem som vi använder till labbredovisningen, med 20-minuterslots per person. Både teoretiska frågor och problemlösning kan ingå i muntan.

Betygssättning

Till slutbetyget bidrar förljande moment:

• 2 kontrollskrivningar, till kursdel 1 resp. 2 (betyg F-A)
• 1 obligatorisk skriftlig sluttenta, alla kursdelar (betyg F-E på kursdel 1 och 2, betyg F-C på kursdel 3)
  
• 1 muntlig komplementeringstenta (betyg F-A)

	KS1	KS2	TEN1	Betyg utan KT	Betyg med KT
Del1	F-A		F-E	F-A	F-A
Del2		F-A	F-E	F-A	F-A
Del3			F-C	F-C	F-A

---

Teorifrågor

Efter kursen skall studenterna kunna svara på följande teorifrågor:

Satslogik

• C-nivå
• förklara naturlig deduktion (se Labb 1)
  
• förklara sundheten och fullständigheten hos naturlig deduktion
• förklara satslogikens avgörbarhet
  
• A-nivå
• argumentera för sundheten hos naturlig deduktion
• argumentera för satslogikens avgörbarhet

Predikatlogik

• C-nivå
• förklara substitution och variabelinfångande
• förklara kvantifikatorreglerna i naturlig deduktion
• förklara sundheten och fullständigheten hos naturlig deduktion
• förklara predikatlogikens oavgörbarhet
  
• A-nivå
• förklara modeller och formella semantiken
• avgöra ekvivalens mellan två formler på semantisk nivå
  

Induktion

• C-nivå
• förklara hur strukturell induktion fungerar
  
• A-nivå
• förklara varför strukturell induktion fungerar

Temporallogik

• C-nivå
• förklara modeller och CTLs formella semantik
  
• A-nivå
• argumentera för sundheten och fullständigheten hos bevissystemet
• argumentera för eller emot modellprovningens avgörbarhet (se Labb 2)
  

Hoare-logik

• C-nivå
• förklara partiell och total korrekthet
• förklara Hoare-logikens regler
  
• A-nivå
• förklara slinginvarianter
• argumentera för Hoare-logikens (dvs reglernas) sundhet
  

---