# Logic in Computer Science — LP1 2015/2016

## News

• 2015-11-17: You can browse or collect your graded exam at the student office. 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.

• 2015-10-22: Assignment 6 is now corrected and can be picked up in office 6103.

• 2015-10-22: You should read the relevant sections in the book on model-checking for CTL (section 3.6.1) and its fixed point characterization (all of section 3.7).

• 2015-10-15: Here is some material from Tuesday's lecture not in the book.

• 2015-10-15: The book "Mathematical Logic for Computer Science", by M. Ben-Ari, contains a presentation of Hilbert-style proof systems, together with an understandable proof of decidability for LTL). It is available online from the Chalmers library.

• 2015-10-13: Here and here is some material of last week's lectures not in the book.

• 2015-10-08: There will be no lecture the last week (19th-23rd October) and the exercise session is on Tuesday (20th October, 10:00 - 11:45 in HB3) instead of Friday.

• 2015-10-08: Assignment 6 is now available (see below). Note that the deadline is on Tuesday, October 20th, 10:00.

• 2015-10-05: Here is a summary of last week's lectures.

• 2015-10-02: Assignment 5 is now available (see below).

• 2015-10-02: Here are some old exams: 2013-10-22, test exam, 2007-04-10, 2011-10-18, 2012-08-22 and 2012-10-25.

• 2015-09-24: Assignment 4 is now available (see below).

• 2015-09-22: Here is the list of the (randomly selected) student representatives.

• GU-students have to register in the Student Portal (see below).

## 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 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 3 first 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.

## Schedule

There will be no lecture the last week (19th-23rd October) and the exercise session is on Tuesday (20th October, 10:00 - 11:45 in HB3) instead of Friday.

Lectures
Tuesday 10:00 - 11:45 in HB3 and Friday 8:00 - 9:45 in HB3.
Exercise Sessions
Friday 10:00-11:45 in HB3.

## For GU-Students

This semester GU-students have to register online via the Student Portal at GU. The registration is obligatory in order to attend the course. Note that you need to register yourself on the course the same day as the first lecture, otherwise you will lose your place.

## Plan for the Lectures

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

## Exam

The exam is on 27 October 2015, starting at 14:00 in HA, HB, and HC.

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

On the exam you are only allowed the use the deduction rules on page 27 of the course book, the introduction and elimination rules for equality and quantifiers, and the copy rule. So in particular De Morgan's rules are not allowed (unless they are proved as separate lemmas).

## 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 2016.

Your solutions must be handed in before the weekly exercise session. The first deadline is in study week two, i.e. September 11th, 10.00. You can hand them in the return box on the 6th floor, in the lectures, 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 on the exercise sesssion the week after; alternatively 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 Commitee for further investigation.

## Exercises

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

• 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.

## Contact Information

#### Lecturers:

Jan Smith, mail: `jan(dot)smith(at)chalmers(dot)se`

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

Thierry is also the examiner of the course.

#### Assistants:

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

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