CM20019—Computation III: Formal Logic and Semantics

1 Textbooks

We use Dan Richardson's notes Formal systems, logic and semantics (distributed in class) and Steffen Hölldobler's slides for propositional and predicate logic.

You might find the book Logic for Computer Science: Foundations of Automatic Theorem Proving by Jean Gallier useful (it is available on the web).

For Prolog, you might find these slides useful.

2 News

3 Course Info

In the following, I will link some material distributed or used in the past for this course: please disregard any information related to the organisation of the course: it is possibly not valid any more. Also, keep in mind that I might change the presentation, sometimes substantially. The material we cover is clearly indicated below.

Usually, in every lecture I suggest some exercises, and then I report these suggestions on this web page. I always suggest exercises on this page after lectures. You are supposed to seriously try, and hopefully solve, all the suggested exercises. In the tutorials, you can check the correctness of your solution and we will go through the difficulties you might have encountered. The solutions to the exercises will not be put on the web, they will be given at tutorials. Be active! This is an easy course if you are active and follow these suggestions, but it becomes very difficult otherwise, and you risk to fail your exam!

Lectures and topics

Material covered and to be prepared for the exam

In Dan Richardson's notes Formal systems, logic and semantics:

In Steffen Hölldobler's slides for propositional logic:

In Steffen Hölldobler's slides for predicate logic:

For a more formal treatment of semantics of first order languages, check 5.3.1, 5.3.2 and 5.3.3 in Gallier's book.


Solutions will be posted here at the end of the corresponding tutorials' week.


There is a single coursework assignment, set on 12 November 2007, distributed in class and available here, to be completed individually, and to be submitted on 22 November 2007. The coursework constitutes 25% of the final grade for this unit.

Please note that the way I wrote the answers is what I consider the ideal way. In other words, if you answer the same way as I did, you get full marks. This is also true for the exam: the coursework and the suggested answers are representative of what you will find at the examination. Do not think that writing more is better: try to be correct and concise.

4 Tutors and Office Hours

Sylvie Anne-Sophie Girard, Tom Gundersen, Ana Carolina Martins Abbud.

Martin Brain and Jonty Needham lead the lab classes.

When you want to talk with me, just drop me an email and we'll arrange for an appointment.

14.12.2007 Alessio Guglielmi email (replace AT by @)