Foundations of Logic Programming

1References

From Logic Programming to Prolog
by Krzystof Apt
(available in the library and on web)

Logic Programming and Negation: A survey
by Krzystof Apt and Roland Bol
(available in the library and on web)

Some slides, also used in the past, are available here:

  1. Introduction
  2. Unification
  3. Procedural Interpretation
  4. Declarative Interpretation
  5. Pure Prolog
  6. Common Use of CUT
  7. Negation -- Procedural Interpretation
  8. Negation -- Declarative Interpretation
  9. Termination of Programs

2News

Exam: 7 February 2012, starting at 10:00am, duration 120 min, room E5 (and E6 should E5 not be sufficient).

On 25 January we will meet at 14:30 in room E005 to complete the tutorial of the morning (allow max 20 mins), and after this the FLP course is considered closed.

No FLP lectures on the week starting on 30/1.

Lecture and tutorial on 24 and 25 January will be swapped.

The lecture on 18/1 is cancelled.

An extra tutorial is planned on 19/12/2011 at DS6 in room 2026.
An extra tutorial is planned on 19/12/2011 at DS1.
Christmas break: last day of teaching period is 21/12/2011, lectures resume on 4/1/2012

The lecture on 16/11/2011 is cancelled for national calendar holiday (Buss- und Bettag); it will be recovered on Friday 18/11/2011 at DS1 and it will be a mixed tutorial/lecture session (more tutorial than lecture).
The lecture on 2/11 is cancelled and anticipated to 18/10 DS4.
The lecture on 9/11 is cancelled and anticipated to 24/10 DS1.
The tutorials on 18/10 and 1/11 (this latter, held by Amin) will take place as planned.

3Course Info

Lectures and topics

12.10.11—Lecture 1Introduction to the course and module; slides 1 have been presented in full. Notions of rule, fact, list, occur-check, termination, success, failure have been discussed through examples; comparison of programs in the declarative and imperative programming languages, as well as some pros and cons of declarative (Prolog) programs have been discussed.

18.10.11—Tutorial 1 Solutions and discussion on some of the proposed exercises in the List 1 (be aware, there is a typo in the mult predicate, which is supposed to be a ternary predicate). Recursion and tail-recursion; use of accumulators; use of Prolog libraries for arithmetics.

18.10.11—Lecture 2 Unification (slides 2, up to page 16). Terms, substitutions, application of subtitutions to a term, composition of substitutions, substitutions ordering, unifiers, most general unifier, Martelli-Montanari algorithm.

19.10.11—Lecture 3 Unification (continuation of slides 2). Relations, partial orders, lexicographic orders, Martelli-Montanari algorithm: proofs of correctness, completeness, termination. Presentation of solutions of further exercises from List 1.

24.10.11—Lecture 4 Procedural Interpretation (slides 3, up to page 28). Terminology, SLD-Derivation step, Resolvent, Standardization apart, Computed Answer Substitution, some elements of arbitrarity, Resolution and propagation, similarity of SLD-derivations, answer substitutions and variants, selection rule, switching lemma, independence from the selection rule.

26.10.11—Lecture 5 Procedural Interpretation (termination of slides 3) and Declarative Interpretation (slides 4, up to p.13). Interpretation and models: terminology, algebras, notions of interpretation, model, state, logical consequence,definition of Herbrand universe and Herbrand Base; examples.

01.11.11—Tutorial 2 Solutions and discussion on some of the proposed exercises in the List 2 (up to 2.6b), held by Amin.

15.11.11—Tutorial 3 Solutions and discussion of the remaining exercises in List 2.

18.11.11—Tutorial 4 Solutions and discussion of the exercises in List 3, up to 3.3 included.

23.11.11—Lecture 6 Declarative interpretation (up to slide 30 included): term model, Herbrand model, Implication tree, correct answer vs computer answer, soundness and completeness of SLD-resolution.

29.11.11—Tutorial 5 Solutions and discussions of the remaining exercises in the List 3 (exercise 3.6: there is a typo in the text, the query is ?-double(s(0),Y), double(Y, s(s(s(s(0))))). Solutions and discussion of the List 4 (for the part c, only the interpretation I_1 has been presented).

30.11.11—Lecture 7 (and tutorial 6) Declarative interpretation (completion of the group 4 of slides). Least Herbrand Model; Partially ordered sets, notions of lower/upper bound, least upper bound; operators on cpo's: monotonicity, finitarity, continuity; pre-fixed point,fixed point, and least fixed point (lfp); characterisation of the least Herbrand Model in terms of lfp(T_P). Examples. Sketch of solution of the exercise 3.6 and hints on how to proceed.

07.12.11—Lecture 8 Pure Prolog (group 5 of slides) and extension with cut. Common uses of cut (group 6 of slides). Negation--Procedural interpretation (above, is the item 7 among the slides): preliminary definitions up to p. 7.

13.12.11—Tutorial 7 Correction of the List 5 of exercises (up to 5.3 included).

14.12.11—Lecture 9 Negation--Procedural interpretation (above, is the item 7 among the slides, up to p. 28): (pre-)SLDNF-trees/derivations/resultants; notions of success, failure, floundering; problems with non-ground negative literals in queries; safe selection rule; allowed programs and queries; Prolog's choices.

19.12.11—Tutorial 8 Correction of the List 5 of exercises (the remaining exercises); correction of the List 6 (up to Ex 6.2 included).

19.12.11—Tutorial 9 Correction of the List 6 (the remaining exercises) and List 7.

21.12.11—Lecture 10 Negation--Procedural interpretation (presentation of the slides has been completed). Negation -- Declarative Interpretation: preliminary definitions, completion of a program, examples, dependency graph of a program, notions of hierarchy, strictness, even/odd dependency, stratification of program/query. Correspondence between SLDNF-computed answer and correct answers wrt to completion for ground and allowed queries/programs (up to page 20 included).

04.01.12—Lecture 11 Negation -- Declarative Interpretation (presentation of the slides has been completed). Completeness of SLDNF-Resolution in restricted forms of Programs and queries; definition of fair selection rule, extended consequence operator and characterisation of Herbrand models for extended program as pre-fixpoint and fixpoint of the extended consequence operator; examples of inadequancy of completion (open programs and looping programs); Herbrand Interpretations and models: supportedness, minimality, intended and non-intended models of a program, stratified programs, their standard models and their properties.

10.01.12—Tutorial 10 Correction of the List 8 (up to 8.3 included).

11.01.12—Lecture 12 Termination of Programs (above, is the item 9 among the slides, up to p.18 included) -- Motivations, examples of programs and queries that may or may not terminate, from the logic programming point of view and from the Prolog point of view. Some technicalities on multisets, multiset's ordering, König's lemma. Notion of level mapping for programs, recurrent programs, bounded queries, how to use the multiset ordering on bounded queries, examples, termination of SLD-derivations on recurrent programs and bounded queries.

24.01.12—Lecture 13 Termination of Programs (group 9 of slides has been completed) -- Examples of recurrent programs and examples of why recurrence doesn't capture termination of Prolog programs. Acceptable programs wrt given |.| and given interpretation and bounded queries wrt given |.| and given interpretation. Examples. Relations between recurrent and acceptable programs.

25.01.12—Tutorial 11 Correction of List of exercises 9 and of List of exercises 10 (ex. 1 only). We have agreed to complete the correction of the list 10 today, at 14:30 in room E005 (it will not take long). The FLP will be considered closed at the end of this meeting.

Material covered and to be prepared for the exam

4Tutors and Office Hours

Amin Timany contributes in the smooth running of the course. The Open house slot is a good venue for discussing your questions, and hopefully I can answer them. Otherwise just drop me an email and we'll arrange for an appointment.

25.01.12Paola Bruscoliemail (replace AT by @)