Search programme

​Use the search function to search amongst programmes at Chalmers. The study programme and the study programme syllabus relating to your studies are generally from the academic year you began your studies.

Syllabus for

Academic year
DAT060 - Logic in computer science  
Matematisk logik för datavetenskap
 
Syllabus adopted 2015-02-12 by Head of Programme (or corresponding)
Owner: MPALG
7,5 Credits
Grading: TH - Five, Four, Three, Fail
Education cycle: Second-cycle
Major subject: Computer Science and Engineering, Information Technology
Department: 37 - COMPUTER SCIENCE AND ENGINEERING


Teaching language: English
Open for exchange students: Yes
Block schedule: D

Course elements   Credit distribution   Examination dates
Sp1 Sp2 Sp3 Sp4 Summer course No Sp
0106 Examination 7,5c Grading: TH   7,5c   30 Oct 2018 pm M   07 Jan 2019 pm M   19 Aug 2019 pm SB_M  

In programs

MPCSN COMPUTER SYSTEMS AND NETWORKS, MSC PROGR, Year 2 (elective)
TKITE SOFTWARE ENGINEERING, Year 2 (elective)
TKITE SOFTWARE ENGINEERING, Year 3 (elective)
MPALG COMPUTER SCIENCE - ALGORITHMS, LANGUAGES AND LOGIC, MSC PROGR, Year 1 (compulsory)

Examiner:

Thierry Coquand


  Go to Course Homepage

 

Eligibility:


In order to be eligible for a second cycle course the applicant needs to fulfil the general and specific entry requirements of the programme that owns the course. (If the second cycle course is owned by a first cycle programme, second cycle entry requirements apply.)
Exemption from the eligibility requirement: Applicants enrolled in a programme at Chalmers where the course is included in the study programme are exempted from fulfilling these requirements.

Course specific prerequisites

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

Aim

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.

Learning outcomes (after completion of the course the student should be able to)

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). Theyshould 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.

Content

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.

Literature

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

Examination including compulsory elements

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


Published: Fri 18 Dec 2009. Modified: Mon 28 Nov 2016