Deductive Systems—Part 1 of Integrated Logic Systems

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: Part 1, Part 2, Part 3, 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:
an introduction to basic notions in term rewriting is here;
TOM web page, including downloads and installation support
Compact slide presentation of TOM by Horatiu Cirstea and Pierre-Etienne Moreau: Part 1, Part 2, Part 3.

I might provide other references during the course, especially on other topics.

2News

11/5/11 DIES ACADEMICUS (no lectures at TUD)

11-17/6/11 lecture-free period at TUD (Reminder)

3Course Info

Lectures and topics

06.04.11—Lecture 1Introduction to the course. The following notions have been introduced and explained on a running example: abstract machine, heap, register; language L0 and machine M0; compilation of a query of L0, query instructions of M0 and their relation to operations in the heap.

13.04.11—Lecture 2The description of the compilation at the level of L0 and machine M0 has been completed by introducing the following notions, on the same running example: compilation of a L0 program, program instructions of M0 and their relation to the operation in the heap; variable binding and the procedure of dereferencing; the need of operating in read/write mode to perform unification; variable binding and unification (on addresses) without occur-check.

14.04.11—Lecture 3The language L1: atoms, terms, L1-program and L1-query. Control instructions in M1: call and proceed. Argument registers and how to modify the M0 instructions to M1. Handling special arguments: representation of constants and Lists.

27.04.11—Lecture 4The language L2. The need of the Continuation Point (CP) register and modifications of call and proceed instructions in M2. Permanent and temporary variables in rules: the Environment. The instructions to Allocate/Deallocate the environment frame. An example of machine code for M2 for a conditional rule (non-empty body)

4.05.11—Lecture 5The language L3 (Pure Prolog) and modification for the machine M3. Dealing with Backtracking and its implications: registers B, TR, HB. Modifying the information in the Choice Point (CP). The need of the Continuation Point (CP) register and modifications of call and proceed instructions in M2. Modifying Allocate/Deallocate. The choice instructions. Example of compilation of a program with multiple clauses. The cut in Prolog: neck-cut and deep-cut and instructions to implement them.

9.05.11—Lecture 6Semantic Tableau: the method, examples, sketch of proof of correctness.

24.05.11—Lecture 7Semantic Tableau and Constraint Handling Rules and their applications to Description Logics.

01.06.11—Lecture 8Answer Set Programming. Preliminary definitions and comparisons to Prolog and logic programming.

08.06.11—Lecture 9Answer Set Programming. Construction of the stable model. Architecture of an ASP: grounding and propagation. Generalisation of clauses: negation in the head, intensional negation, disjunctive head, variables. A running example of generation of answer set for hamiltonian cycles. Comparisons to logic programming.

22.06.11—Lecture 10 and 11Deductive systems based on term rewriting (the functional perspective). Basic notions: terms, substitutions, matching, rewriting, applications of rewriting, conditional rewriting and generalised rewriting rules. Equality modulo C and modulo AC; matching modulo C and modulo AC. Rewriting modulo: the class rewriting modulo R/A, and comparison on the relations induced on terms.

29.06.11—Lecture 12Introducing TOM: terms, rewriting, matching, strategies over Java. Algebraic specifications, the system Gom, abstract syntax and rules, evaluation of Gom modules (stroke instruction), matching, evaluating rewriting rules.

Material covered and to be prepared for the exam

4Tutors and Office Hours

I don't have 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.

29.6.11Paola Bruscoliemail (replace AT by @)