A. Satslogik
- Informell matematisk argumentation
- Formella bevismetoder: naturlig deduktion
- Syntax och semantik
- Sundhet, fullständighet och avgörbarhet
B. Predikatlogik
- Syntax och semantik, Kripke-strukturer
- Bevismetoder: naturlig deduktion
- Sundhet, fullständighet och oavgörbarhet, Gödels satser
C. Prolog
- Resolution och logikprogrammering: unifiering, backtracking, negering, snitt och låddiagram
D. Induktionsbevis
- Matematisk och fullständig induktion
- Induktiva definitioner och strukturell induktion
E. Temporallogik
- Syntax och semantik
- Bevismetoder: modellprövning
F. Hoare-logik
- Programsemantik och programspecifikation
- Programverifikation
- Syntax och semantik: Kripke-strukturer
- Bevismetoder: modellprövning
Efter godkänd kurs ska studenten kunna:
- specificera allmänna egenskaper hos matematisk-datalogiska strukturer och bevisa dessa med hjälp av naturlig deduktion i satslogik och predikatlogik,
- specificera induktiva definitioner hos datastrukturer och bevisa dessa med strukturell induktion,
- specificera och bevisa systemegenskaper med hjälp av temporal logik,
- specificera och bevisa programegenskaper med hjälp av Hoarelogik,
- tillämpa metoder för automatisk deduktion och utföra enkla bevis med modellprövning,
- tillämpa och förklara grundläggande begrepp inom logikprogrammering: unifiering, backtracking, snitt, negering och olika programmeringstekniker som t.ex. generate-test
i syfte att
- behärska de bevistekniker som behövs i kommande kurser i utbildningen.
För högre betyg ska studenten dessutom kunna:
- argumentera för korrektheten hos en viss bevisteknik: sundhet och fullständighet,
- argumentera för bevisteknikers lämplighet till automatisk deduktion: avgörbarhet.
