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