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 - Logic in computer science
 
Kursplanen fastställd 2012-02-18 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   25 Okt 2012 em H,  17 Jan 2013 em M,  19 Aug 2013 em V

I program

TKITE INFORMATIONSTEKNIK, CIVILINGENJÖR, Årskurs 3 (valbar)
MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Årskurs 1 (obligatorisk)

Examinator:

Professor  Jan Smith
Professor  Thierry Coquand


Kursutvärdering:

http://document.chalmers.se/doc/b5543d8c-6bf3-4a02-9e2a-db0acd8aab37


  Gå till kurshemsida

Behörighet:

För kurser inom Chalmers utbildningsprogram gäller samma behörighetskrav som till de(t) program kursen ingår i.

Kursspecifika förkunskaper

The requirement for the course is to have succesfully completed two years with the subject Computer Science or equivalent. Particularly relevant are Mathematics (including Discrete mathematics), Programming, Algorithms and/or data structures.

Syfte

In recent years, powerful tools for verifying software and hardware systems have been developed. These tools rely in a crucial way in logical techniques. This course provides a sound basis in logic and a short introduction to some logical frameworks used in modelling, specifying and verifying computer systems. A sound basic knowledge in logic is a welcome prerequisite for courses in program verification, formal methods and artificial intelligence.

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

The students should be able to understand and use formal tools for checking software and hardware, such as SAT-solver and model checking tools (used in software engineering). He should also be able to explain the meaning of soundness and completeness for various logic (propositional, predicate and temporal logic) and to write derivation trees in natural deduction in predicate logic.

Innehåll

We cover: propositional logic (sections 1.1 to 1.5), predicate logic (sections 2.1 to 2.6) and model-checking (sections 3.2 and 3.4). In other words, a thorough introduction to fundamental notions of logic: natural deduction, semantics both of propositional and predicate logic, soundness and completeness, conjunctive normal forms, Horn clauses, undecidability of predicate logic, expressiveness of predicate logic, existential and universal second-order logic plus an introduction to model checking: Linear-time temporal logic (LTL) and Branching-time temporal logic (CTL).

Organisation

Two lectures and one exercise session every week.

Litteratur

The course will follow the book by Michael Huth and Mark Ryan with the same name, see http://www.cs.bham.ac.uk/research/lics/

Examination

The course is examined by a written exam at the end of the course.


Sidansvarig Publicerad: on 24 jan 2018.