Syllabus for |
|
| DAT060 - Logic in computer science |
| |
| Owner: TITEA |
|
|
5,0 Credits (ECTS 7,5) |
| Grading: TH - Five, Four, Three, Not passed |
| Level: B |
|
Department: 37 - COMPUTER SCIENCE AND ENGINEERING
|
Teaching language: English
| Course module |
|
Credit distribution |
|
Examination dates |
|
Sp1 |
Sp2 |
Sp3 |
Sp4 |
|
No Sp |
| 0106 |
Examination |
5,0 c |
Grading: TH |
|
|
5,0 c
|
|
|
|
|
|
18 Dec 2006 am V, |
10 Apr 2007 pm V, |
Contact examiner |
In programs
TDATA COMPUTER SCIENCE AND ENGINEERING - Other elective courses, Year 4 (elective)
TITEA SOFTWARE ENGINEERING, Year 3
DCMAS MSc PROGR IN DEPENDABLE COMPUTER SYSTEMS, Year 1 (elective)
Examiner:
Professor
Jan Smith
Professor
Thierry Coquand
Eligibility:
For single subject courses within Chalmers programmes the same eligibility requirements apply, as to the programme(s) that the course is part of.
Course specific prerequisites
Knowledge in mathematics, including a course in Discrete mathematics, and in programming.
Content
As for the content, the idea is to 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)
Literature
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