Search programme

​Use the search function to search amongst programmes at Chalmers. The programme overview and the 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
 
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


Page manager Published: Thu 03 Nov 2022.