Kursplan fö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.