DM509, Fall 2006, 2nd quarter - Weekly Note 7

Exact curriculum (pdf) for the exam is now available.

There will be a spørgetime (session with possibilities for asking questions on the curriculum) Wednesday, January 17, at 14:15 in U46. We will do the entire exam of summer 2006 (pdf), and will discuss any questions on the curriculum and the exam you may have.

There will also be a session where we do the remaining exercises from the last exercise class (exam of summer 2003 (pdf), exercise 4, question c, exam of winter 2000 (pdf), exercise 1, question b, exam of summer 2003 (pdf), exercise 2, and exam of winter 2001 (pdf), exercise 2). This will take place Monday, January 15, at 12:15 in U49.

Lecture December 19

More on Prolog: More built-in predicates. More examples of code. Start on detailed unification algorithm.

Reading

Chapter 6, and parts of Chapter 7 in Clocksin and Mellish. Section 3.2 (handouts) from Nilsson and Maluszynski book.

Comments

The textbook is a bit vague in Chapter 10 (except for the algorithm for conversion to clausal form in Section 10.2). For the interested, a more precise account of the subject can be found in Chapters 1-3 in Ulf Nilsson, Jan Maluszynski: Logic, Programming and Prolog, 2nd edition, Wiley, 1995 (Sections 2.3-4 can be omitted). The book is out of print, but is available online at http://www.ida.liu.se/~ulfni/lpp/. Note that Horn clauses are termed definite clauses in this book.

In relation to the exam, only the algorithm on page 40 in Nilsson and Maluszynski is relevant. It is not deep, but for a full understanding, reading most of Section 3.2, as well as Section 1.5 (and the errata of the book, which corrects an error in Section 1.5) is an advantage (mostly to get the notation used). The rest of the handed out Sections 3.1-3 can be seen as a more elaborate version of (part of) the material in Chapter 10 in Clocksin and Mellish.

Lecture December 21

End of detailed unification algorithm. Prolog and logic. Predicate calculus. Clausal form. Horn clauses. Conversion of predicate calculus formulas to clausal form.

Reading

Chapter 10 in Clocksin and Mellish. Handouts from last lecture. Pages 4-6 (handout) in note by Ernest Davis on predicate calculus.

Comments

Pages 4-6 in the note by Ernest Davis is a slightly more precise version (and also using more standard logical notation) of the algorithm from Section 10.2 in Clocksin and Mellish for converting a predicate calculus formula to clausal form.