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:
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:
Schedule of Classes in April (room E005):
|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):
|2 DS1+DS4||3 DS4||4 DS1|
05.04.12Lecture 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.12Lecture 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.12Lecture 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.12Lecture 4 Modification of M0 instructions to M1. Special arguments: representations for constants and lists. Examples, exercise, discussion.
18.04.12Lecture 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.12Lecture 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.12Lecture 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.12Lecture 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.12Lecture 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.12Lecture 10 Constraint handling rules for description logics. Examples, exercise, discussion.
26.04.12Lecture 11 Answer Set Programming (Part 4). Preliminary definitions, comparisons with Prolog and logic programing. Generalisation to classical negation.
02.05.12Lecture 12 Generalisations: intensional negation, disjunctive head,variables. Examples on Hamiltonian cycles. Comparisons lo logic programming.
02.05.12Lecture 13 ASP for verification. Preliminary notions of Deductive systems based on Rewriting: recalling some notions and terminology of term rewriting system.
03.05.12Lecture 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.12Lecture 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.
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 @)