Second Seminar Day on Constraint Handling Rules 6-Jul-2006
Constraint Handling Rules (CHR) is a simple, but elegant declarative rule-based programming language. It combines elements of Constraint Programming, Production Rules, and Rewrite Systems. Typical applications are constraint solving, natural language processing, type checking, and reasoning capabilities for multi-agent systems. Various implementations of CHR exist for Prolog, Java, and other languages. Following the successful first seminar day, 10-May-2006, hosted by the Declarative Languages and Artificial Intelligence research group (DTAI) of the K.U.Leuven (Belgium), a Second Seminar Day is organised by the CHR research group at Ulm. As the research group of Slim Abdennadher at the German University in Cairo is visiting Universität Ulm, Thom Frühwirth, creator of CHR, invites to present recent results and exchange ideas.
- 09:00 CHR Tutorial. Thom Frühwirth, Universität Ulm.
- 10:15 ARM: Automatic Rule Miner. Noha Salem, German University in Cairo.
- 10:45 Break.
- 11:00 Linear Logic Semantics for CHRv. Hariolf Betz, Universität Ulm.
- 11:30 Solving general first order constraints. Khalil Djelloul, Universität Ulm.
- 12:00 Lunch break.
- 14:30 Implementation of an F-Logic Kernel in CHR. Martin Käser, Universität Ulm.
- 15:00 Complexity of the CHR Rational Tree Equation Solver. Marc Meister, Universität Ulm.
- 15:30 Break.
- 15:45 Cairo teaching assistants' interests (10 min each, informal). Noha Salem, Amira Thabet, Ingi Sobhi, Abdellatif Olama, German University in Cairo.
- 16:30 Cairo students' projects using Constraint Programming (10 min each, informal). Amira Gamaleldin, Marlien Edward, Mounir Stino, German University in Cairo.
- 17:00 Closing discussion.
More about the talks
- CHR Tutorial. <LINK 5731>Thom Frühwirth</LINK>, Universität Ulm. Rule-based programming experiences renaissance due to its applications in areas such as Business Rules, Semantic Web, Computational Biology, Verification and Security. Executable rules are used in declarative programming languages, in program transformation and analysis, and for reasoning in artificial intelligence applications. Constraint Handling Rules (CHR) is a concurrent committed-choice constraint logic programming language consisting of guarded rules that transform multi-sets of atomic formulas (constraints) into simpler ones until exhaustion. CHR was initially developed for solving constraints, but has matured into a general-purpose concurrent constraint language over the last decade, because it can embed many rule-based formalisms and describe algorithms in a declarative way. The clean semantics of CHR facilitates non-trivial program analysis and transformation.
- ARM: Automatic Rule Miner. Noha Salem, German University in Cairo. Rule-based formalisms are ubiquitous in computer science. However, a difficulty that arises frequently when specifying or programming the rules in to determine which effects should be propagated by these rules. In this paper, we present a tool called ARM (Automatic Rule Miner) that generates rules for relations over finite domains. ARM offers a rich functionally to provide the user with the possibility of specifying the admissible syntactic forms of the rules. Furthermore, we show that our approach performs well on various examples, e.g. generation of firewall rules or generation of medical diagnosis rules. Thus, it is suitable for users from different fields.
- Linear Logic Semantics for CHRv. <LINK 5746>Hariolf Betz</LINK>, Universität Ulm. Declarative semantics presents a powerful tool for the analysis and verification of CHR programs, a property inherited from its logical and constraint-logical predecessors. My talk is about the linear logic semantics for CHRv, i.e. CHRs with disjunction. At first, a short introduction to linear logic will be given and the already established linear logic semantics for classic CHR will be presented. Subsequently, we will discuss my approach how to extend this result to CHRv.
- Solving general first order constraints. <LINK 5753>Khalil Djelloul</LINK>, Universität Ulm. We show in this talk how can we generalise the elementary notion of "a constraint" to "a general first order formula" with functions, relations and any logical symbols. By the same way, we generalize the notion of solving a constraint in any model M to solving a first order formula in any theory T that has at least M as model. In order to solve a first order constraint P in a theory T, we first introduce the notion of "decomposable theories" and show that a lot of fundamental theories used in computer science are "decomposable". We give then a general algorithm for solving first-order formulas in any decomposable theory T. The algorithm is given in the form of five rewriting rules. It transforms a first-order formula P, which can possibly contain free variables, into a conjunction Q of solved formulas easily transformable into a Boolean combination of existentially quantified conjunctions of atomic formulas. In particular, if P has no free variables then Q is either the formula true or false. The correctness of our algorithm proves the completeness of the decomposable theories.
- Implementation of an F-Logic Kernel in CHR. Martin Käser, Universität Ulm. Frame-Logic is an extension of classical predicate logic which accounts in a declarative way for many features of object-orientation. This talk presents a concise, exploratory CHR implementation of Frame-Logic's core features, based on data-driven forward propagation, including object-oriented constraint syntax, type-checking, and interaction of Frame-Logic deduction with non-monotonic overriding by inheritance.
- Complexity of the CHR Rational Tree Equation Solver. <LINK 5740>Marc Meister</LINK>, Universität Ulm. One of the first CHR programs is the classic constraint solver for syntactic equality of rational trees that performs unification. The worst-case time (and space) complexity of this short and elegant solver so far was an open problem and assumed to be polynomial. In this talk we (this is joint work with Thom Frühwirth) show that under the standard operational semantics of CHR there exist particular computations with n occurrences of variables and function symbols that produce O(2^n) constraints, thus leading to exponential time and space complexity. We also show that the standard implementation of the solver in CHR libraries for Prolog may not terminate due to the Prolog built-in order used in comparing terms. Complexity can be improved to be quadratic for any term order under both standard and refined CHR semantics without changing the equation solver, when equations are transformed into flat normal form.
German University of Cairo teaching assistant team members and their interests (10 min each)
- Noha Salem. Theoretical aspects of CHR, preflow push algorithm, analysis of confluence and other performance criteria, automatic generation of rules (ARM tool).
- Amira Thabet. Business rules and JCHR, automatic generation of rules (ARM tool).
- Ingi Sobhi. Business rules, Prolog and CHR, global constraints in CHR.
- Abdellatif Olama. Global constraints in JCHR, automatic generation of Rules (ARM tool).
German University of Cairo student team members and their projects using CP (10 min each)
- Amira Gamaleldin. Examination scheduling.
- Marlien Edward. Timetable scheduling for advising students.
- Mounir Stino. Timetable scheduling for all students.