# DAT060/DIT201, Logic in Computer Science — LP1 2018/2019

## News

• November 19: You can browse or collect your graded exam at the CSE Student Office, Campus Johanneberg. But if you want to query any grading decision you must not remove the exam from the office; if you think there is something wrong with the grading, please let us know and we will have a look into it and give you the possiblity to discuss with us if necessary.
• October 30: Sample solutions for the exam are available.
• October 29: For those who picked up their Assignment 6 today after lunch we might not have recorded your points on Assignment 6 yet, unless you have put yourself on the list. Please come to the office where you picked up Assignment 6 in the next couple of days to double check the records. We are sorry for the inconvenience caused.
• October 30: Giovanni found a mistake in the sample solution for exercise 2.3.1a).
• October 26: An alternative solution for Problem 6.2 is available.
• October 25: A sample solution for Problem 5.2 is available.
• October 23: Marked Assignment 6 can be picked up on Monday, October 29th. Sample solutions are available.
• October 17: Daniel found a mistake in the sample solution for exercise 3.2.2b).
• October 15: Assignment 6 is due on Tuesday, October 23rd.
• October 9: Summary of the lecture.
• October 9: The office hours on Thursday, October 11 are cancelled.
• October 9: A collection of old exams is available.
• October 4: Assignment 5 is due on Tuesday, October 16th.
• October 3: Remember the exceptional schedule next week, with the exercise session on Tuesday and the second lecture on Wednesday.
• October 2: Summary of the lecture. Here is an updated version.
• October 2: Other presentation of predicate logic.
• September 28: Assignment 4 is due on Friday, October 5th.
• September 24: The student representatives have been selected.
• September 20: Assignment 3 is due on Friday, September 28.
• September 13: Assignment 2 is due on Friday, September 21.
• September 7: Assignment 1 is due on Friday, September 14.

## Goals of the Course

The goal of the course is to present the fundamental basic notions of logic that are important in computer science. One presents propositional and predicate logic in natural deductions the way it is done in most interactive theorem provers, with a suggestive box notation for proofs. One presents also the basis of model checking and temporal logic (LTL and CTL). One does not cover a detailed proof of the completeness theorem for predicate logic (and one gives a sketch of completeness for propositional logic) but what is important is that the students understand well the meaning of the various completeness theorems. (On the other hand one gives a proof of undecidability of predicate logic via Post systems.) In the same spirit, one does not present complete proofs of decidability for LTL and CTL but one presents in detail the fixed-point semantics of CTL.

The content of the course is roughly the first three chapters of Huth and Ryan "Logic in Computer Science".

There are some slides motivating the course.

## Text Book

This course uses Logic in Computer Science by Michael Huth and Mark Ryan (available as an eBook from the Chalmers Library).

## Schedule

### Lectures

Tuesday, 10:00–11:45 in HB3 and Friday, 8:00–9:45 in HB3 (except: October 9th, October 12th and October 26th)
Tuesday, October 9th, 8:00–9:45 in HB3
Wednesday, October 10th, 8:00–9:45 in HC4

### Exercise Sessions

Friday, 10:00–11:45 in HB3 (except: October 12th and October 26th)
Tuesday, October 9th, 10:00–11:45 in HB3

### Office hours

Thursday, 14:00–14:59 in 6103A (or via e-mail to the assistants)

## Plan for the Lectures

Week Chapters Topics Exercises Assignments Solutions
1 1.1, 1.2 Propositional logic, natural deduction Week 1 ex1.pdf -
2 1.3, 1.4, 1.5 Formal language, proof by induction, semantics, normal form Week 2 ex2.pdf -
3 2.1, 2.2, 2.3 Predicate logic, natural deduction Week 3 ex3.pdf -
4 2.4 Semantics of predicate logic Week 4 ex4.pdf -
5 2.5, 2.6 Undecidability, expressivity of predicate logic Week 5 ex5.pdf sol52.txt
6 3.2, 3.3, 3.4, 3.5 LTL, CTL Week 6 ex6.pdf sol6.pdf, sol62.txt
7 3.6, 3.7 Algorithms, fixed-point characterization, repetition Week 7 - -

## Assignments

There will be six non-obligatory assignments which should be handed in individually. Each assignment gives ten points and 10% of those points count as bonus points in the exam. The bonus points are only valid for the exams held before September 2019.

Your solutions must be handed in before the weekly exercise session. The first deadline is in study week two, i.e. Friday, September 14th, at 10:00. You can hand them in the return box by the printers and restrooms on the 6th floor (will be emptied no later than 9:45), in the beginning of the exercise session, or in office 6103A. Please do not hand them in by email.

Graded submissions will be handed back during the exercise session the week after; afterwards you can pick them up in room 6103A.

All submissions must include your name, email address, and be stapled together. Your solutions must be clear and readable; everything must be carefully motivated!

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

## Exam

The exam is on Tuesday, October 30th 2018, starting at 14:00 in Maskin-salarna.

The exam has 60 points in total. No books or written help is allowed during the exam.

On the exam you are only allowed to use the basic deduction rules on page 27 of the course book, ¬¬e, LEM, PBC, the introduction and elimination rules for equality (pp. 107, 108) and quantifiers (pp. 109, 110, 112, 113), and the copy rule (p. 20). So in particular, ¬¬i, Modus tollens and De Morgan's rules are not allowed (unless you also provide their proof, then they can be used as lemmas).

## Exercises and old exams

Here is a list of exercises from a previous year, some with comments. Exercises marked with an asterisk ("*") in the text book have solutions.

Here is a collection of old exams from the years 2007, 2011, 2012, 2013, and 2016–2018.

• An interactive introduction to natural deduction for propositional and predicate calculus with several good examples.

• A text on the tree method (looking systematically for a countermodel).

• A prover to practice natural deduction (only for propositional logic).

• A short note on how to decide an LTL formula. This is not required for the exam, but I found the explanations in the book difficult to follow and wanted to have a method which can be applied by hand on small examples.

• A general presentation of some notions of the course and a nice application of the use of temporal logic.

## Student representatives

• Felix Jansson (Chalmers: firstlast.96@gmail.com)
• Erik Källberg (Chalmers: kalerik)
• Stanislaw Zwierzchowski (Chalmers: stazwi)

## Contact Information

### Lecturers

Simon Huber, mail: `simon.huber(at)cse(dot)gu(dot)se`

Thierry Coquand, mail: `thierry.coquand(at)cse(dot)gu(dot)se`

Thierry is also the examiner of the course.

### Assistants

Andrea Vezzosi, mail: `vezzosi(at)chalmers(dot)se`

Fabian Ruch, mail: `fabian.ruch(at)cse(dot)gu(dot)se`