First International Summer School
on Constraint Handling Rules

August 30th - September 3rd, 2010
Leuven, Belgium

Lecture abstracts

Analysis of CHR Solvers (5 hours)

Slim Abdennadher, German University in Cairo

Program analysis, both static and dynamic, is the central issue of programming environments. The 6 hour course provides an overview about several techniques to prove properties of CHR solvers. In particular, we will discuss:

The course is based on several research papers, especially the paper As time goes by: Constraint Handling Rules - A Survey of CHR Research from 1998 to 2007 and on a chapter of the book Constraint Handling Rules. No special background is needed!

Abduction and language processing with CHR (5 hours)

Henning Christiansen, Roskilde University, Denmark

Abduction refers to the sort reasoning that infers facts by means of which a given observation can be explained. This can be understood as reasoning backwards from an observed effect to its possible cause, e.g., from symptoms to diagnosis. Abduction is often accompanied by so-called integrity constraints that limit the inferred facts or causes to be what is believed to conform with some possible world.

CHR allows an elegant encoding of abduction, by mapping abducible facts into CHR constraints and integrity constraints into CHR rules. Combining this with Prolog as a general knowledge representation yields an easy-to-use and powerful environment for abductive reasoning. When, furthermore, this is combined with Prolog's grammar notation, DCGs, we obtain a system abductive language interpretation. These techniques can be used directly in CHR+Prolog or via the HYPROLOG system which adds utilities and a thin layer of syntactic sugar on top.

CHR Grammars represent another system in which CHR rules are applied for bottom-up analysis, which can also be combined with abduction in CHR as described.

Finally, we show how probabilistic abduction can be expressed and implemented in a CHR program which searches for the best, i.e., the most probable, explanation of the observation.

A basic background in logic programming will be helpful for this course, but is not strictly necessary. With or without a background in linguistics, students can benefit from that parts on language analysis.

Literature
A detailed reading list will be prepared, based on the following references:

Abdennadher+Christiansen: An Experimental CLP Platform for Integrity Constraints and Abduction. Proc. FQAS2000, pp. 141--152, Advances in Soft Computing series, Springer, 2000.
– First reference to abduction in CHR. pdf

Christiansen+Dahl: HYPROLOG: A New Logic Programming Language with Assumptions and Abduction, Proc. International Conference on Logic Programming, ICLP'05, pp. 159-173, 2005. Lecture Notes in Computer Science 3668.
– pdf

Christiansen: CHR grammars. International Journal on Theory and Practice of Logic Programming, vol. 4+5, special issue on Constraint Handling Rules, pp. 467-501, 2005.
– pdf

Christiansen: Implementing Probabilistic Abductive Logic Programming with Constraint Handling Rules, Constraint Handling Rules, Current Research Topics. T. Schrijvers, T. Frühwirth (eds.). Lecture Notes in Artificial Intelligence 5388, Springer 2008. pp. 85-118.
– pdf

Christiansen. Executable specifications for hypothesis-based reasoning with Prolog and Constraint Handling Rules, Journal of Applied Logic, vol 7, 2009. pp. 341-362.
– pdf

Christiansen: Artificial Intelligence and Intelligent Systems: Logic programming as a framework for Knowledge Representation and Artificial Intelligence. Roskilde University, 2006.
– A course note with pedagogical introductions to Prolog and CHR with applications for abduction; many examples. pdf

Websites
HYPROLOG: Source code, User's guide, examples.
CHR Grammars: Source code, User's guide, examples.

CHR - a common platform for rule-based approaches (4h)

Thom Frühwirth, University of Ulm

This course provides an overview of rule-based programming and formalisms in computer science by embedding them into the Constraint Handling Rules (CHR) language. These embeddings give us the possibility to compare and analyse the different approaches on the common basis of CHR. In particular we discuss:

The course is based on a chapter of the book Constraint Handling Rules.

A basic background in any of the rule-based approaches mentioned can be helpful for the course, but is not strictly necessary.

Computability and complexity of CHR (3.5 hours)

Jon Sneyers, K.U.Leuven

In this course we look at the computability and complexity of CHR. We start by showing how to simulate Turing machines and other models of computation in CHR. Next, we study the time and space complexity of CHR, first for an abstract "CHR machine", then for real CHR systems. In particular, we will see the complexity-wise completeness result. Finally we consider at several variants and fragments of CHR and their properties w.r.t. computability, expressiveness and complexity.

The course is based on a number of recent publications, including:

A basic background in complexity theory is helpful for the course, but not strictly necessary. Part of this course builds upon the implementation course by Peter Van Weert.

Implementation of CHR systems (3.5 hours)

Peter Van Weert, K.U.Leuven

In recent years, CHR has matured to a powerful general purpose language, increasingly used for applications such as constraint solving, computational linguistics, and multi-agent systems. Considerable research has therefore been devoted to the efficient compilation and execution of CHR programs, resulting in several very efficient CHR systems for Prolog, Java, C, and Haskell.

This 4 hour tutorial provides a lucid, comprehensive overview of the efficient compilation and optimization techniques used by current state-of-the-art CHR systems. Using high-level pseudocode and clarifying examples, we first introduce the innovating lazy rule evaluation methodology, and then gradually discuss more advanced analysis and optimization techniques. We compare our approach with the popular Rete matching algorithm, used by mainstream commercial systems. Throughout, we will show that knowing how rule engines work helps you write better, more efficient rule-based programs.

The course is partly based on the article "Efficient Lazy Evaluation of Rule-Based Programs". Slides from a previous seminar are available in PowerPoint 2007 or PDF format.

No background in compiler construction is required at all. A basic knowledge of programming is sufficient.

Equivalence in CHR — A Tool-Oriented Approach (1 hour)

Frank Raiser, University of Ulm

In this presentation, we investigate equivalence with respect to CHR states and formulations of the operational semantics of CHR. Our aim is to familiarize listeners with these topics and supply them with tools that facilitate formal analysis of operational behavior of CHR programs.

First, we introduce an axiomatic definition for equivalence of CHR states. Together with a decidable, sufficient, and necessary criterion, it offers a tool for discussing equality of resulting computation states.

Next, we consider the operational semantics of CHR, which forms the basis for formal analysis of properties of CHR programs. We present two formulations on different abstraction levels that are equivalent to each other, as well as to the traditional high-level operational semantics of CHR. We further demonstrate advantages gained from selecting these formulations over others.

Finally, we introduce an operation for merging CHR states and discuss its properties. It corresponds closely to the monotonicity property of CHR, which is an integral aspect of formal analysis of CHR execution. Hence, it finds applications in macro step proofs, and more generally, in restricting computational contexts to relevant parts of a state.

CHR and Linear Logic &mdash Analysis of Multi-Paradigm CHR Programs (1 hour)

Hariolf Betz, University of Ulm

In this talk, we investigate the relationship between linear logic and CHR as well as the multi-paradigm language extension CHR with Disjunction (DCHR). Our aim is to give the participants an impression of linear logic, to make them aware of its relationship to CHR and to show how this relationship can be applied to analyse and compare multi-paradigm CHR programs.

Firstly, we give an introduction to linear logic. We observe how the power of linear logic to embed classical logic on the one hand and to model concurrent systems on the other hand make it a natural foundation for CHR. We formalize this relationship by presenting a translation from CHR into linear logic and a theorem stating its soundness and completeness.

Secondly, we investigate how this relationship can help us to gain a better understanding of CHR. We exemplarily show how linear logic justifies the axiomatic definition of state equivalence. We furthermore discuss how we can use linear logic to decide a form of operational equivalence for confluent CHR programs.

Thirdly, we extend our results to DCHR. We give an axiomatic definition of state equivalence in DCHR and we present an equivalence-based operational semantics for DCHR. We then adapt our results for CHR to DCHR. Finally, we see how we can apply our findings to formalize and decide operational equivalence of multi-paradigm CHR programs.

Download lecture slides

Here you can download the slides that will be used in the lectures. There is no need to print these: every participant will get a set of handouts.

Other planned activities

Introduction to CHR and practical session

On the first day there will be a CHR tutorial and a practical session.

Programming contest

(more information will follow)

Social activity

A visit to the AB InBev beer brewery. (more information will follow)

Schedule

 (enlarge)