Behörighetskrav

40 poäng i matematik eller datalogiska ämnen inklusive Algebra DV2 och Logik och bevisteknik DV1.

Syfte

Att ge fördjupade kunskaper i logik och dess

tillämpningar i datalogi.

Innehåll

Axiomsystem, teorier och modeller. Avgörbara och oavgörbara teorier.

Konstruktiv logik: lambdakalkyl, intuitionistisk logik, typteori,

programextraktion från bevis.

Modal logik, Kripkemodeller och möjligavärldars-semantik.

Fullständighetssatsen och automatisk bevisföring.

Två av följande ämnen: resolutionsmetoden, modellkontroll,

algoritmer för satslogik och binära beslutsdiagram (BDD).

Undervisning

Föreläsningar, lektioner, grupparbeten och laborationer.

Examination

Vid kursens slut anordnas ett skriftligt prov på hela kursen. Obligatoriska moment kan också

förekomma under kursens gång. För studerande som underkänts i det ordinarie slutprovet anordnas

två extra provtillfällen varje läsår, i augusti och vid höstterminens eller vårterminens slut.