Kursen tar upp satslogik och predikatlogik och behandlar begrepp som syntax, semantik, bevis, sundhet och fullständighet, likhet, Horn-formler, unifiering och resolution.
Moment 1, teoridel, 3 hp
Det krävs förtrogenhet med formella logiska system för att förstå grundläggande begrepp inom många datavetenskapliga områden såsom artificiell intelligens, databassystem och beräkningsteori. Kursens syfte är att skapa den här förtrogenheten genom att förmedla sats- och predikatlogikens begrepp och tekniker ur en datavetenskaplig synvinkel.
Särskild vikt läggs på
- skillnaden mellan sanning och bevis, dvs. definitionen av begreppet sanning å ena sidan och utvecklandet av formella system för att härleda sanningsvärdet av ett påstående å andra sidan
- algoritmiska aspekter på bevissystem med tonvikt på resolution
Moment 2, laborationsdel, 1.5 hp
Delmomentet utgörs av en laborationskurs med ett antal obligatoriska inlämningsuppgifter
Förväntade studieresultat
Efter avslutad kurs ska studenten kunna:
- förklara grundläggande koncept inom formell logik
- tillämpa logik inom olika datavetenskapliga områden
- särskilja de logiska komponenterna i ett datavetenskapligt-analytiskt problem
- granska logisk stringens i formella presentationer
- producera formellt logiska lösningar inom datavetenskapliga tillämpningar
Behörighetskrav
Univ: För tillträde till kursen krävs, förutom grundläggande behörighet, kurserna Algebra, 5p (MATA96) eller Diskret matematik, 7.5 hp (5MA006), Datavetenskapens grunder, 7.5 hp (5DV037) och Datastrukturer och algoritmer, 7.5 hp (5DV043) eller motsvarande kunskaper.
Undervisningens upplägg
Undervisningen bedrivs i form av föreläsningar, arbete i datorlabb och övningar i mindre grupper. Utöver schemalagda aktiviteter krävs även individuellt arbete med materialet.
Examination
Examinationen sker dels genom skriftlig tentamen dels genom obligatoriska uppgifter. På hela kursen ges något av betygen Underkänd (U), Godkänd (3), Icke utan beröm godkänd (4) eller Med beröm godkänd (5). På den skriftliga tentamen sätts något av betygen Underkänd (U), Godkänd (3), Icke utan beröm godkänd (4) eller Med beröm godkänd (5). På de obligatoriska uppgifterna ges endast betygen Underkänd (U) eller Godkänd (G). För att bli godkänd på hela kursen krävs att samtliga delar av examinationen är godkända. Betyget utgör en sammanfattande bedömning av resultaten vid examinationens olika delar och sätts först när alla prov och obligatoriska uppgifter är godkända.
För studerande som inte godkänns vid ordinarie provtillfälle anordnas ytterligare provtillfälle.
Studerande som två gånger underkänts i prov, har rätt att hos styrelsen för Institutionen för datavetenskap begära att annan lärare utses för att sätta betyg på honom/henne. Den som godkänts i ett prov får ej undergå förnyat prov för högre betyg.
TILLGODORÄKNANDE
I en examen får denna kurs ej ingå, helt eller delvis, samtidigt med en annan kurs med likartat innehåll. Vid tveksamheter bör den studerande rådfråga studievägledare vid Institutionen för datavetenskap.
Litteratur
Litteraturlistan är inte tillgänglig via den webbaserade utbildningskatalogen.
Kontakta aktuell institution.
