bild
Skolan för
datavetenskap
och kommunikation
KTH / CSC / Kurser / DD1350 / logik12 / Labbar

Logik för dataloger, logik12

Labbar

Inbokning till redovisning

Beskrivning

Laborationerna i kursen har syftet att fordjupa förståelsen av några utvalda logiska koncept och ge en känsla för praktisk användning av verktyg baserade på logik. Laborationerna utförs och redovisas individuellt eller i par.
 
Nr. Datum Aktivitet
1 27/9 + 28/9 Lab1  hjälptillfälle 1
2 4+5/10 Lab1  hjälptillfälle 2
3 25+26/10 Lab1  redovisning
4 23/11 Lab2  hjälptillfälle 1
5 30/11 Lab2  hjälptillfälle 2
6 7/12 Lab2  redovisning

Labbsalar

Alla bokade labbsalar har Ubuntu datorer med både sicstus-prolog och gnu-prolog.

Labbgrupper

Studenterna är indelade i två labbgrupper, beroende på första bokstaven i familjenamnet på den yngste i teamet:
  • labbgrupp 1:  A - J
  • labbgrupp 2:  K - Ö
Första 2-timmarsblock är för första labbgruppen, och andra 2-timmarsblock är för andra labbgruppen.

Hjälptillfällen

Hjälptillfällen är bokade i 2-timmarsblock. Ni får ta plats och sätta sig i sima-kön.

Laborationsuppgift 1

Första laborationen handlar om att konstruera och implementera en beviskollare till bevis i satslogik som är presenterade i naturlig deduktion. Labbuppgiften finns här.

Laborationsuppgift 2

Andra laborationen handlar om att konstruera och implementera en modellprovare till tillstånd i övergångssystem och formler i CTL. Labbuppgiften finns här.

Inbokning till labbredovisning

Händer med hjälp av systemet REMORES.

Copyright © Sidansvarig: Dilian Gurov <dilian@csc.kth.se>
Uppdaterad 2012-08-16