Deductive Systems (summer semester 2012)

1References

We will initially follow the:

Warren's Abstract Machine - A Tutorial Reconstruction
by Hassan Ait-Kaci
(available on the web, not linked for copyright reasons)

Michael Thielscher has kindly provided some slides he has used in the past:

  1. Prolog - Part 1
  2. Prolog - Part 2
  3. Tableaux - Part 3
  4. Answer Set Programming - Part 4.

In Dan Richardson's course notes you may find the description of the tableau method.

In Thom Frühwirth's paper you may find the application of CHR systems to Description Logics.

Horatiu Cirstea and Pierre-Etienne Moreau are among the developers of the system TOM:

  1. basic notions in term rewriting;
  2. TOM web page, including downloads and installation support
  3. Compact slide presentation of TOM by Horatiu Cirstea and Pierre-Etienne Moreau: Part 1, Part 2, Part 3.

Material covered and to be prepared for the exam

Schedule of Classes in April (room E005):

Mon Tue Wed Thu Fri
5 DS4
11 DS4 12 DS4
17 DS2 18 DS1+DS4 19 DS4 20 DS1
23 DS5 25 DS4 26 DS4

Schedule of Classes in May (room E005):

Mon Tue Wed Thu Fri
2 DS1+DS4 3 DS4 4 DS1
7 8 9 10 11
14 15 16 17 18
21 22 23 24 25

2News

3Course Info

Lectures and topics

05.04.12—Lecture 1 Introduction to the course. Part 1, the Warren Abstract Machine. Notions of abstract machine, heap, register; language L0 and machine M0; compilation of a query L0.

11.04.12—Lecture 2 Query instructions of M0 and their operations in the heap. Compilation of a program of L0, program instructions of M0 and their operations in the heap. Variable binding and dereferencing. Examples, exercises, discussions.

12.04.12—Lecture 3 The need of operating in read/write mode for unification; variable binding and unification without occur check. Language L1: atoms, terms L1-program and L1-query. Control instructions in M1: call and proceed. Argument registers.

17.04.12—Lecture 4 Modification of M0 instructions to M1. Special arguments: representations for constants and lists. Examples, exercise, discussion.

18.04.12—Lecture 5 The language L2. Need of the continuation point (CP) register; modification of call and proceed in M2. Permanent and temporary variables in rules: the environment. Instructions to Allocate/Deallocate environment frames. Example of M2-machine code for a conditional rule with a non-empty body. (refer to Part 2 of the slides).

18.04.12—Lecture 6 The language L3 (Pure Prolog); modifications for M3. Backtracking, and its implications: registers B, TR, HB. Modifying the Choice Point. Need of the continuation point register and adapting call and proceed instructions.

19.04.12—Lecture 7 Modifying allocate and deallocate. Backtracking. The choice instructions. Examples of compilation of a program with multiple clauses. Cut in prolog: neck-cut, deep-cut, instructions. Examples and discussion.

20.04.12—Lecture 8 Modifying allocate and deallocate. Backtracking. The choice instructions. Examples of compilation of a program with multiple clauses. Cut in prolog: neck-cut, deep-cut, instructions. Examples and discussion.

23.04.12—Lecture 9 Semantic tableaux (Part 3). Introductory notions: Definitional Normal Form, Skolemisation, Tableaux, examples of refutation, properties. Introductory notions of Description Logics. Use of tableaux in description logics. Example, exercises, discussion.

25.04.12—Lecture 10 Constraint handling rules for description logics. Examples, exercise, discussion.

26.04.12—Lecture 11 Answer Set Programming (Part 4). Preliminary definitions, comparisons with Prolog and logic programing. Generalisation to classical negation.

02.05.12—Lecture 12 Generalisations: intensional negation, disjunctive head,variables. Examples on Hamiltonian cycles. Comparisons lo logic programming.

02.05.12—Lecture 13 ASP for verification. Preliminary notions of Deductive systems based on Rewriting: recalling some notions and terminology of term rewriting system.

03.05.12—Lecture 14 Conditional Rewriting and generalised rewriting rules. Equality modulo C and modulo AC; matching modulo C and modulo AC. Rewriting modulo: the class R/A and comparisons on the relations induced on terms. Examples, exercise, and discussions.

04.05.12—Lecture 15 Presesntation of TOM: Terms, rewriting, matching, strategies over Java. Examples of Algebraic specifications, the system Gom, Abstract syntax and rules, evaluation of Gom modules, matching, evaluation of rewriting rules.

4Tutors and Office Hours

This course has no tutors. 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.05.12Paola Bruscoliemail (replace AT by @)