2nd CHR Summer School 2011

Programming and Reasoning with Rules and Constraints

5th to 9th of September, 2011 — Cairo, Egypt

Courses

  1. Introduction to CP (2h), Slim Abdennadher, German University in Cairo
  2. Consistency Techniques and Constraint Reasoning (2h), Carmen Gervet, German University in Cairo
  3. Introduction to CHR (2h), Jon Sneyers, K.U.Leuven, Belgium
  4. Implementing Constraint Solvers using CHR (2h), Slim Abdennadher, German University in Cairo and Thom Fruehwirth, University Ulm
  5. CHR - a common platform for rule-based approaches (2h), Thom Fruehwirth, University Ulm
  6. Analysis of CHR Solvers (2h), Slim Abdennadher, German University in Cairo
  7. Equivalence in CHR - A Tool-Oriented Approach (2h), Frank Raiser, Konzept Informationssysteme GmbH, Germany
  8. Probabilistic CHR and an Application in Music (2h), Jon Sneyers, K.U.Leuven, Belgium

Courses Abstracts

Introduction to CP (2 hours)
Slim Abdennadher, German University in Cairo

The use of constraints had its scientific and commercial breakthrough in the 1990s. Programming with constraints makes it possible to model and specify problems with uncertain, incomplete information and to solve combinatorial problems, as they are abundant in industry and commerce, such as scheduling, planning, transportation, resource allocation, layout, design, and analysis. Constraint-based programming languages enjoy elegant theoretical properties, conceptual simplicity, and practical success.

The idea of constraint-based programming is to solve problems by simply stating constraints (conditions, properties) which must be satisfied by a solution of the problem. Constraints can be considered as pieces of partial information. Constraints describe properties of unknown objects and relationships between them. Constraints are formalized as distinguished, predefined predicates in first-order predicate logic. The unknown objects are modeled as variables.

The main goal of this course is to give an introduction to a new programming paradigm based on constraints over different domains, such as Booleans, real (rational) numbers or finite domains. Special emphasis will be put on the practical use of these methods, in particular for solving combinatorial optimizations problems. No prior background knowledge is assumed, although familiarity with Prolog is useful.

Consistency Techniques and Constraint Reasoning (2h)
Carmen Gervet, German University in Cairo

TBA

Introduction to CHR (2 hours)
Jon Sneyers, K.U.Leuven, Belgium

This basic introduction to CHR covers the syntax, semantics, and basic properties using several program examples. No prior background knowledge is assumed, although familiarity with Prolog is useful.

Implementing Constraint Solvers using CHR (2 hours)
Slim Abdennadher, German University in Cairo and Thom Fruehwirth, University Ulm

After the previous introductory session that presents CHR as a general-purpose language, this course presents CHR as a special-purpose language to implement solvers over various domains.

CHR - a common platform for rule-based approaches (2 hours)
Thom Fruehwirth, University 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.

Analysis of CHR Solvers (2 hours)
Slim Abdennadher, German University in Cairo

Program analysis, both static and dynamic, is the central issue of programming environments. The 2 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!

Equivalence in CHR - A Tool-Oriented Approach (2 hours)
Frank Raiser, Konzept Informationssysteme GmbH, Germany

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.

Probabilistic CHR and an Application in Music (2 hours)
Jon Sneyers, K.U.Leuven, Belgium

In this lecture we present CHRiSM, a probabilistic extension of CHR based on CHR(PRISM). PRISM is a probabilistic extension of Prolog in which stochastic models can be represented, probabilistic inference can be done, and the parameters of the model (the underlying probability distributions) can be learned. CHRiSM adds the power of CHR rules to this mix, increasing the expressiveness of the formalism.

We then demonstrate an application, called APOPCALEAPS, which was implemented in CHRiSM. It is a system that generates pop music songs. Its parameters can be tuned manually or learned automatically based on a given set of example songs.