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.

*22.9.07*There will be no tutorials in Week 1.*7.10.07*There will be a single coursework assignment on 12 November 2007, to be completed individually, and to be submitted on 22 November 2007.*19.10.07*I will be absent on Monday 22 and Tuesday 23 October; Monday's lecture will be taught by Paola Bruscoli.

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!**

*1.10.07—Lecture 1*Introduction to the course: proof that 3 + 2 = 5 and some considerations about this.*5.10.07—Lecture 2*Introduction to the course, informal presentation of the relation between syntax and semantics; introduction to the definition of*formal system*.*8.10.07—Lecture 3*Definitions of*formal system*and*string rewriting system*; brief reminding of the notion of*computability*.*12.10.07—Lecture 4*Definitions of*grammar*and*term*; brief discussion of the notion of*computable set*.*15.10.07—Lecture 5*Definitions of*substitution*and*composition of substitutions*.*19.10.07—Lecture 6*Definitions of*unifier*,*most general unifier*and*unification algorithm*.*22.10.07—Lecture 7**First order language*and*free and bound variables*.*26.10.07—Lecture 8**Interpretation*and*valuation*.*29.10.07—Lecture 9**Semantics of first order languages*(except for universal and existential quantification);*entailment*.*2.11.07—Lecture 10*Semantics of first order languages for*universal*and*existential quantification*;*validity*.*5.11.07—Lecture 11*Notion of*model*and introduction to*Prolog*(proof that 2 < 4).*9.11.07—Lecture 12*Introduction to*Prolog*(problem: X < Y).*12.11.07—Lecture 13**Procedural interpretation*of Prolog.*16.11.07—Lecture 14**Input*and*output*in Prolog; example with a program that computes addition.*19.11.07—Lecture 15*More on*input*and*output*in Prolog;*lists*, program*append*for lists.*23.11.07—Lecture 16*More on*lists*, the*bubblesort*algorithm in Prolog; Prolog code for this lecture.*26.11.07—Lecture 17*Prolog's*cut*primitive; introduction to*resolution*, concepts of*soundness*and*completeness*.*30.11.07—Lecture 18**Conjunctive normal form*for propositional logic,*resolution*.*3.12.07—Lecture 19**Resolution*for propositional logic.*7.12.07—Lecture 20**Resolution*for predicate logic:*prenex normal form*and*skolemisation*.*10.12.07—Lecture 21*Formal notion of*skolemisation*and*resolution step*for predicate logic.*14.12.07—Lecture 22**Completeness*of resolution.

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

- Chapter 1: 1.1, 1.2, 1.3, 1.4.
- Chapter 2 (all of it).
- Chapter 3: 3.2, 3.5, 3.8, 3.9.
- Chapter 4: 4.1, 4.2, 4.3, 4.4, 4.5, 4.7, 4.8, 4.14.1.
- Chapter 9: 9.2, 9.3, 9.4, 9.5, 9.6, 9.11, 9.13.

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

- Pages: 21-23, 29-36, 43-50, 85-90.

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

- Pages: 33-47, 53-59.

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.

- Exercise 1: tutors comment on students' solutions in week 2 (starting from 8 October 2007); solutions.
- Exercise 2: tutors comment on students' solutions in week 3 (starting from 15 October 2007); solutions.
- Exercise 3: tutors comment on students' solutions in week 4 (starting from 22 October 2007); solutions.
- Exercise 4: tutors comment on students' solutions in week 5 (starting from 29 October 2007); solutions.
- Exercise 5: tutors comment on students' solutions in week 6 (starting from 5 November 2007); solutions.
- Exercise 6: tutors comment on students' solutions in week 7 (starting from 12 November 2007); solutions.
- Exercise 7: this exercise is primarily for the lab sessions; however, tutors comment on students' solutions in weeks 7 and 8 (starting from 12 November 2007); solutions.
- Exercise 8: this exercise is primarily for the lab sessions; however, tutors comment on students' solutions in weeks 8 and 9 (starting from 19 November 2007); solutions.
- Exercise 9: this exercise is primarily for the lab sessions; however, tutors comment on students' solutions in weeks 9 and 10 (starting from 26 November 2007); solutions.
- Exercise 10: tutors comment on students' solutions in week 11 (starting from 10 December 2007); solutions.

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.

- Coursework; coursework with solutions.

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.

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 @)