DAT060 / DIT202 Logic in computer science

Course-PM

DAT060 / DIT202 Logic in Computer Science

LP1 HT20 (7.5 hp)

The course is offered by the department of Computer Science and Engineering.

 

Contact Details

  • Examiner and lecturer: Thierry Coquand <coquand @ chalmers.se>
  • Lecturer: Ana Bove <bove @ chalmers.se>
  • Teaching assistant:
    • Jeremy Pope <popje @ chalmers.se>
    • Nachiappan Valliappan <nacval @ chalmers.se>

 

Course Purpose

Powerful tools for verifying software and hardware systems have been developed. These tools rely in a crucial way on 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.

 

Schedule

TimeEdit

Overview of Topics and Reading Material per Week

Week Topics Reading Material/Book Sections
1 Recap logic, sets, relations, functions, induction sets relations functions notes on induction Structural induction
1.4.2
2 Natural deduction for propositional logic 1.1-1.3
3 Semantics of propositional logic, normal forms 1.4-1.5 except 1.4.2
4 Natural deduction and semantics for predicate logic 2.1-2.4
5

Undecidability of predicate logic and Post correspondence problem
Fixpoint and SAT solving
Guest lecture: Applications of propositional and predicate logic

2.5
6

Expressivity of predicate logic, compactness, Gödel's incompletness theorem
Linear temporal logic

2.6, 3.2
7 LTL, CTL
Guest lecture on model checking using temporal logic.
3.2-3.5
8

Algorithms, fix-point characterization

Repetition, old exams

 

3.6-3.7

 

Exercises

Week 1: exercises1.pdf

Weeks 2--8: exercises2-8.pdf

 

Course Literature

Logic in Computer Science by Michael Huth and Mark Ryan, second edition.

See http://www.cs.bham.ac.uk/research/lics/

Exercises marked with an asterisk ("*") in the text book have solutions.

(There used to be an electronic version of the book available via Chalmers library, please check!)

 

Course Design

The course consists of a series of lectures and exercise sessions.

The language of instruction is English.

 

Changes Made since the Last Occasion

Extra lectures (including a guest lecture) and consultation/exercise classes were already introduced in LP1 2019.
In LP1 2020 we will try to have two guest lectures to better show the applications of the course.
However, our first priority this year is that the run in distance mode is as smooth as possible.

 

Learning Objectives and Syllabus

After completing the course the student is expected to be able to:

Knowledge and understanding:

  • explain when a given formula is a tautology,
  • explain the notion of model of a first-order language and of temporal logic,
  • explain when a first-order and a temporal logic formula is semantically valid,
  • explain how to check if a branching-time temporal logic formula is valid in a given model,
  • explain the meaning of the soundness and completeness theorems for propositional and predicate calculus.

Competence and skills:

  • write and check proofs in natural deduction for propositional and predicate calculus,
  • specify properties of a reactive system using linear-time temporal logic and branching time temporal logic.

Judgement and approach:

  • judge the relevance of logical reasoning in computer science, i.e. for modelling computer systems,
  • analyse the applicability of logical tools to solve problems in computer science, i.e. finding bugs with the use of model checking.

 

Link to the syllabus on

 

Examination Form

OBS: We follow Chalmers and GU directives regarding exams during Covid-19 times so what we write here might change due to these circumstances. In that case we will inform as soon as possible.

Information about examination at Chalmers during Covid-19 times.

Exam in October: via Zoom at https://chalmers.instructure.com/courses/12955
                                        Duration of the exam: 4 hours+30 min to upload your solution.
                                        The exam will be monitored so you must have a camera.
                                         We are trying to figure out all details on how things will proceed, we will upload
                                        information about this soon.

The course is examined by an individual written exam taken place in an examination hall at the end of the course.

The exams has a maximum of 60 points and the passing grades in the exam are as follow:

Chalmers
U: 0-29
3: 30-40
4: 41-50
5: 51-60
GU
U: 0-29
G: 30-45
VG: 46-60

Note:

When making a natural deduction proof in the exam you are allowed to use any of the rules presented in page 27 of the book plus the introduction and elimination rules for both the universal and existential quantifiers, unless it is stated otherwise in an exercise.

In other words, you are allowed to use all introduction and elimination rules (including those for double negation) and the derived rules MT, PBC and LEM, unless stated otherwise.

No other result can be used unless it is proved.

Non-obligatory assignments:

There will be 5-6 non-obligatory individual assignments. Each assignment gives up to ten points and 10% of those points count as bonus points in the written exam. These bonus points are valid for the whole academic year 20/21.

Solution to the assignments will be discussed in the Friday exercise session after the submission.

All submissions must include your name, personal number and email address, and be stapled together if they are handed in paper. Your solutions must be clear and readable; everything must be carefully motivated!

As always in life, you should not cheat! Any suspicious on cheating will be taken seriously and must be reported to the Disciplinary Committee for further investigation.

Exam dates for 2020/2021: 27 October 2020 pm, 4 January 2021 pm, 16 August 2021 pm.

 

Course Evaluation

Student Representatives

CTH

Erik Ljungdahl <ljerik @ student.chalmers.se>
André Olsson <oandre @ student.chalmers.se>
Viktor Truvé <truvev @ student.chalmers.se>
Daniel Willim <willim @ student.chalmers.se>

GU

Jakob Alexander Fihlman <gusfihlja @ student.gu.se>
Isabella Fransson <gusisabefr @ student.gu.se>

Meetings

First meeting: Thursday 17/9 15:15 via zoom, protocol1.pdf

Second meeting: Friday 16/10 15:00 via zoom, protocol2.txt

Course summary:

Date Details Due