"False"
Umeå universitet
printicon
Huvudmenyn dold.
Kursplan:

Grundläggande logik och modellteori, 7,5 hp

Engelskt namn: Fundations of Logic and Model Theory

Denna kursplan gäller: 2009-01-19 till 2011-06-12 (nyare version av kursplanen finns)

Kurskod: 5DV102

Högskolepoäng: 7,5

Utbildningsnivå: Grundnivå

Huvudområden och successiv fördjupning: Datavetenskap: Grundnivå, har mindre än 60 hp kurs/er på grundnivå som förkunskapskrav

Betygsskala: TH teknisk betygsskala

Ansvarig institution: Institutionen för datavetenskap

Beslutad av: teknisk-naturvetenskapliga fakultetsnämnden, 2009-03-24

Innehåll

Kursen tar upp satslogik, predikatlogik och modellteori. Under kursen behandlas begrepp som syntax, semantik, bevis, sundhet och fullständighet, likhet, Horn-formler, unifiering och resolution. Moment 1, teori, 4.5 högskolepoäng 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. Under momentet skapas den här förtrogenheten genom att förmedla sats- och predikatlogikens begrepp och tekniker ur en datavetenskaplig synvinkel. Även temporal logik behandlas i samband med att modellteori diskuteras. 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 • modeller för logiska system och hur dessa används för att verifiera egenskaper. Moment 2, färdighetsträning, 3 högskolepoäng Momentet utgörs av ett antal obligatoriska uppgifter. Teori från moment 1 tillämpas under grundläggande färdighetsträning kring användandet av definitioner, notationer och formella system inom logiken.

Förväntade studieresultat

Efter avslutad kurs ska studenten kunna: • förklara skillnaden och samspelet mellan syntax och semantik • förklara och använda sig av grundläggande begrepp, definitioner och notationer inom satslogik, predikatlogik och modellteori • visa en grundläggande förståelse för satslogiska bevissystem och kunna praktiskt använda sig av bevisregler och axiom • redogöra för begreppen sundhet och fullständighet inom bevissystem • definiera och använda sig av Hornklausuler • uppvisa goda kunskaper och praktiska förmågor kring resolution, inbegripande att kunna omvandla formler till CNF, redogöra för resolutionsregeln, utföra substitution och unifiering, beräkna mest generella unifieraren samt utföra resolutionsbevis • diskutera satisfierbarhet, sundhet och fullständighet för resolution både inom satslogik och predikatlogik • definiera vad som menas med en modell för de olika logiska system som behandlats i kursen • redogöra för de grundläggande skillnaderna i vad som går att uttrycka i de olika logikerna • visa en grundläggande förståelse för hur modeller kan användas inom olika typer av verifikation

Behörighetskrav

Univ:För tillträde till kursen krävs, Introduktion till diskret matematik (5MA008) och en grundläggande kurs i programmeringsmetodik som t.ex. Grundläggande programmeringsteknik och datorsystem (5DV074) eller motsvarande kunskaper. Dessutom är det en stark rekommendation att ha läst ytterligare minst en kurs i matematik och/eller kursen Datavetenskapens grunder (5DV037).

Undervisningens upplägg

Undervisningen bedrivs i form av föreläsningar, övningar i mindre grupper samt handledning i samband med studenternas arbete med obligatoriska uppgifter. Utöver schemalagda aktiviteter krävs även individuellt arbete med materialet.

Examination

Examinationen sker dels genom skriftlig tentamen (på moment 1) dels genom ett antal obligatoriska uppgifter (på moment 2). På moment 1 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å moment 2 ges endast betygen Underkänd (U) eller Godkänd (G). 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). För att bli godkänd på hela kursen krävs att samtliga prov och obligatoriska moment är godkända. Betyget utgör en sammanfattande bedömning av resultaten vid examinationens olika delar och sätts först när alla obligatoriska moment är godkända. För studerande som inte godkänns vid ordinarie provtillfälle anordnas ytterligare provtillfälle. En student som utan godkänt resultat har genomgått två prov för en kurs eller en del av en kurs, har rätt att få en annan examinator utsedd, om inte särskilda skäl talar emot det (HF 6 kap. 22 §). Begäran om ny examinator ställs till styrelsen för Institutionen för datavetenskap. 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