Sök i programutbudet

Använd sökfunktionen för att leta efter kurser och program i Chalmers utbildningsutbud. Den programplan och utbildningsplan som avser dina studier är i allmänhet från det läsår du började dina studier.

​​​​​​​​​​​​​

Kursplan för

Läsår
DAT060 - Matematisk logik för datavetenskap  
 
Kursplanen fastställd 2015-02-12 av programansvarig (eller motsvarande)
Ägare: MPALG
7,5 Poäng
Betygskala: TH - Fem, Fyra, Tre, Underkänt
Utbildningsnivå: Avancerad nivå
Huvudområde: Datateknik, Informationsteknik
Institution: 37 - DATA- OCH INFORMATIONSTEKNIK


Undervisningsspråk: Engelska
Sökbar för utbytesstudenter
Blockschema: D

Modul   Poängfördelning   Tentamensdatum
Lp1 Lp2 Lp3 Lp4 Sommarkurs Ej Lp
0106 Tentamen 7,5 hp Betygskala: TH   7,5 hp   27 Okt 2015 em H,  04 Jan 2016 em H   15 Aug 2016 em SB

I program

MPALG DATAVETENSKAP - ALGORITMER, PROGRAMSPRÅK OCH LOGIK, MASTERPROGRAM, Årskurs 1 (obligatorisk)
MPCSN DATORER, NÄTVERK OCH SYSTEM, MASTERPROGRAM, Årskurs 2 (valbar)
TKITE INFORMATIONSTEKNIK, CIVILINGENJÖR, Årskurs 3 (valbar)

Examinator:

Professor  Jan Smith
Professor  Thierry Coquand



  Gå till kurshemsida

Behörighet:


För kurser på avancerad nivå gäller samma grundläggande och särskilda behörighetskrav som till det kursägande programmet. (När kursen är på avancerad nivå men ägs av ett grundnivåprogram gäller dock tillträdeskrav för avancerad nivå.)
Undantag från tillträdeskraven: Sökande med en programregistrering på ett program där kursen ingår i programplanen undantas från ovan krav.

Kursspecifika förkunskaper

Kravet för kursen är att ha framgångsrikt slutfört två år med ämnet datavetenskap eller motsvarande. Särskilt relevant är matematik (inklusive diskret matematik), programmering, algoritmer och/eller datastrukturer.

Syfte

Under de senaste åren har kraftfulla verktyg för verifikation av programvaru- och hårdvarusystem utvecklats. Dessa verktyg förlitar sig på ett avgörande sätt i logiska tekniker. Kursen ger en god grund i logik och en kort introduktion till några logiska ramverk som används för att modellera, specificera och modellera datorsystem. Grundläggande kunskaper i logik är en god grund för kurser i programverifiering, formella metoder och artificiell intelligens.

Lärandemål (efter fullgjord kurs ska studenten kunna)

Studenterna ska kunna förstå och använda formella verktyg för kontroll av mjukvara och hårdvara, såsom SAT-lösare och "model checking tools" (som används i programvaruteknik). De skall också kunna förklara innebörden av sundhet och fullständighet för olika logiker (sats-, predikat- och temporal logik) och skriva härledningar i naturlig deduktion i predikatlogik.

Innehåll

Vi täcker: satslogik (avsnitt 1,1-1,5), predikatlogik (avsnitt 2,1-2,6) och model-checking (avsnitten 3.2 och 3.4). Med andra ord, en grundlig introduktion till grundläggande begrepp och metoder i logik: naturlig deduktion, semantik för både sats- och predikatlogik, sundhet och fullständighet, konjunktiv normalform, Horn klausuler, oavgörbarhet av predikatlogik, uttrycksfullhet av predikatlogik, existentiella och universella andra- ordningens logiker.

Organisation

Undervisning ges i form av föreläsningar och övningar.

Litteratur

Huth, Ryan. Logic in Computer Science, se http://www.cs.bham.ac.uk/research/lics/

Examination

För att bli godkänd på kursen krävs godkänd skriftlig tentamen. Baserat på tentamensresultatet ges betygen U,3,4 eller 5.


Sidansvarig Publicerad: on 24 jan 2018.