As time goes by: Constraint Handling Rules - A survey of CHR research from 1998 to 2007
---
paper_title: Constraint Handling Rules

paper_content:

Constraint Handling Rules (CHR) is both a theoretical formalism based on logic and a practical programming language based on rules. This book, written by the creator of CHR, describes the theory of CHR and how to use it in practice. It is supported by a website containing teaching materials, online demos, and free downloads of the language. After a basic tutorial, the author describes in detail the CHR language and discusses guaranteed properties of CHR programs. The author then compares CHR with other formalisms and languages and illustrates how it can capture their essential features. Finally, larger programs are introduced and analyzed in detail. The book is ideal for graduate students and lecturers, and for more experienced programmers and researchers, who can use it for self-study. Exercises with selected solutions, and bibliographic remarks are included at the ends of chapters. The book is the definitive reference on the subject.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: Projection in adaptive Constraint Handling

paper_content:

Constraint solving in dynamic environments requires an immediate adaptation of the solutions if the constraint problems are changing. Constraint solving with Constraint Handling Rules (CHR) is extended with incremental algorithms, thus supporting the solution of dynamic constraint satisfaction problems (DCSPs). Unfortunately, constraint processing with CHR introduces a lot of new variables which require additional memory space and reduce run-time performance. Most of the variables may be eliminated without any loss of information. Thus, memory may be kept rather small and run-time performance may be improved. This paper describes the use of projection with CHR in order to eliminate irrelevant variable bindings and maintain the constraint store quite small. In detail, some projection algorithms are presented to eliminate variables which are introduced during constraint processing with CHR. Projection is called early projection if it is applied together with each rule application, thus eliminating recently introduced irrelevant variable bindings while keeping the derived constraint store quite small. This kind of projection is well-suited when solving Dynamic Constraint Satisfaction Problems, especially after constraint deletion, when many superfluous variable binding have to be deleted as well. Consequently, the modifications that are required for an adaptation are reduced. This may result in an improved performance of the adaptation algorithms and a better performance for non-adaptive constraint processing with CHR is also expected.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: Essentials of Constraint Programming

paper_content:

1. Introduction.- I. Constraint Programming.- 2. Algorithm = Logic + Control.- 3. Preliminaries of Syntax and Semantics.- 4. Logic Programming.- 5. Constraint Logic Programming.- 6. Concurrent Constraint Logic Programming.- 7. Constraint Handling Rules.- II. Constraint Systems.- 8. Constraint Systems and Constraint Solvers.- 9. Boolean Algebra B.- 10. Rational Trees RT.- 11. Linear Polynomial Equations R.- 12. Finite Domains FD.- 13. Non-linear Equations I.- III. Applications.- 14. Market Overview.- 15. Optimal Sender Placement for Wireless Communication.- 16. The Munich Rent Advisor.- 17. University Course Timetabling.- IV. Appendix.- A. Foundations from Logic.- A.1 First-Order Logic: Syntax and Semantics.- A.2 Basic Calculi and Normal Forms.- A.2.1 Substitutions.- A.2.2 Negation Normal Form and Prenex Form.- A.2.3 Skolemization.- A.2.4 Clauses.- A.2.5 Resolution.- List of Figures.- References.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: A linear-logic semantics for constraint handling rules

paper_content:

One of the attractive features of the Constraint Handling Rules (CHR) programming language is its declarative semantics where rules are read as formulae in first-order predicate logic. However, the more CHR is used as a general-purpose programming language, the more the limitations of that kind of declarative semantics in modelling change become apparent. We propose an alternative declarative semantics based on (intuitionistic) linear logic, establishing strong theorems on both soundness and completeness of the new declarative semantics w.r.t. operational semantics.
---
paper_title: A Unified Semantics for Constraint Handling Rules in Transaction Logic

paper_content:

Reasoning on Constraint Handling Rules (CHR) programs and their executional behaviour is often ad-hoc and outside of a formal system. This is a pity, because CHR subsumes a wide range of important automated reasoning services. Mapping CHR to Transaction Logic (τ R) combines CHR rule specification, CHR rule application, and reasoning on CHR programs and CHR derivations inside one formal system which is executable. This new τ R semantics obviates the need for disjoint declarative and operational semantics.
---
paper_title: Unfolding in CHR

paper_content:

Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption and more generally to optimize a given program. Essentially it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. One of the basic operations which is used by most program transformation systems is unfolding which consists in the replacement of a procedure call by its definition. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages and, to the best of our knowledge, no one has considered unfolding of CHR programs. This paper is a first attempt to define a correct unfolding system for CHR programs. We define an unfolding rule, show its correctness and discuss some conditions which can be used to delete an unfolded rule while preserving the program meaning.
---
paper_title: Aggregates for Constraint Handling Rules

paper_content:

Constraint Handling Rules (CHR) [2,3,4] is a general-purpose programming language based on committed-choice, multi-headed, guarded multiset rewrite rules. As the head of each CHR rule only considers a fixed number of constraints, any form of aggregation over unbounded parts of the constraint store necessarily requires explicit encoding, using auxiliary constraints and rules.
---
paper_title: Abstract Critical Pairs and Confluence of Arbitrary Binary Relations

paper_content:

In a seminal paper, Huet introduced abstract properties of term rewriting systems, and the confluence analysis of terminating term rewriting systems by critical pairs computation. In this paper, we provide an abstract notion of critical pair for arbitrary binary relations and context operators. We show how this notion applies to the confluence analysis of various transition systems, ranging from classical term rewriting systems to production rules with constraints and partial control strategies, such as the Constraint Handling Rules language CHR. Interestingly, we show in all these cases that some classical critical pairs can be disregarded. The crux of these analyses is the ability to compute critical pairs between states built with general context operators, on which a bounded, not necessarily well-founded, ordering is assumed.
---
paper_title: Probabilistic Constraint Handling Rules

paper_content:

Abstract Classical Constraint Handling Rules (CHR) provide a powerful tool for specifying and implementing constraint solvers and programs. The rules of CHR rewrite constraints (non-deterministically) into simpler ones until they are solved. In this paper we introduce an extension of Constraint Handling Rules (CHR), namely Probabilistic CHRs (PCHR). These allow the probabilistic “weighting” of rules, specifying the probability of their application. In this way we are able to formalise various randomised algorithms such as for example Simulated Annealing. The implementation is based on source-to-source transformation (STS). Using a recently developed prototype for STS for CHR, we could implement probabilistic CHR in a concise way with a few lines of code in less than one hour.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: A compositional semantics for CHR

paper_content:

Constraint Handling Rules (CHR) are a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multi-headed guarded rules which allow one to rewrite constraints into simpler ones until a solved form is reached.CHR has received a considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multi-headed clauses, there are several aspects of the CHR semantics which have not been clarified yet. In particular, no compositional semantics for CHR has been defined so far.In this paper we introduce a fix-point semantics which characterizes the input/output behavior of a CHR program and which is and-compositional, that is, which allows to retrieve the semantics of a conjunctive query from the semantics of its components. Such a semantics can be used as a basis to define incremental and modular analysis and verification tools.
---
paper_title: Observable confluence for constraint handling rules

paper_content:

Constraint Handling Rules (CHR) are a powerful rule based language for specifying constraint solvers. Critical for any rule based language is the notion of confluence, and for terminating CHR programs there is a decidable test for confluence. But many CHR programs that are in practice confluent fail this confluence test. The problem is that the states that illustrate non-confluence are not observable from the initial goals of interest. In this paper we introduce the notion of observable confluence, a more general notion of confluence which takes into account whether states are observable. We devise a test for observable confluence which allows us to verify observable confluence for a range of CHR programs dealing with agents, type systems, and the union-find algorithm.
---
paper_title: Abstract interpretation for constraint handling rules

paper_content:

Program analysis is essential for the optimized compilation of Constraint Handling Rules (CHRs) as well as the inference of behavioral properties such as confluence and termination. Up to now all program analyses for CHRs have been developed in an ad hoc fashion.In this work we bring the general program analysis methodology of abstract interpretation to CHRs: we formulate an abstract interpretation framework over the call-based operational semantics of CHRs. The abstract interpretation framework is non-obvious since it needs to handle the highly non-deterministic execution of CHRs. The use of the framework is illustrated with two instantiations: the CHR-specific late storage analysis and the more generally known groundness analysis. In addition, we discuss optimizations based on these analyses and present experimental results.
---
paper_title: Compiling Constraint Handling Rules for Efficient Tabled Evaluation

paper_content:

Tabled resolution, which alleviates some of Prolog's termination problems, makes it possible to create practical applications from high-level declarative specifications. Constraint Handling Rules (CHR) is an elegant framework for implementing constraint solvers from high-level specifications, and is available in many Prolog systems. However, applications combining the power of these two declarative paradigms have been impractical since traditional CHR implementations interact poorly with tabling. In this paper we present a new (set-based) semantics for CHR which enables efficient integration with tabling. The new semantics coincides with the traditional (multi-set-based) semantics for a large class of CHR programs. We describe CHRd, an implementation based on the new semantics. CHRd uses a distributed constraint store that can be directly represented in tables. Although motivated by tabling, CHRd works well also on non-tabled platforms. We present experimental results which show that, relative to traditional implementations, CHRd performs significantly better on tabled programs, and yet shows comparable results on non-tabled benchmarks.
---
paper_title: The Refined Operational Semantics of Constraint Handling Rules

paper_content:

Constraint Handling Rules (CHRs) are a high-level rule-based programming language commonly used to write constraint solvers. The theoretical operational semantics for CHRs is highly non-deterministic and relies on writing confluent programs to have a meaningful behaviour. Implementations of CHRs use an operational semantics which is considerably finer than the theoretical operational semantics, but is still non-deterministic (from the user’s perspective). This paper formally defines this refined operational semantics and proves it implements the theoretical operational semantics. It also shows how to create a (partial) confluence checker capable of detecting programs which are confluent under this semantics, but not under the theoretical operational semantics. This supports the use of new idioms in CHR programs.
---
paper_title: Guard and Continuation Optimization for Occurrence Representations of CHR

paper_content:

Constraint Handling Rules (CHR) is a high-level rule-based language extension, commonly embedded in Prolog. We introduce a new occurrence representation of CHR programs, and a new operational semantics for occurrence representations, equivalent to the widely implemented refined operational semantics. The occurrence representation allows in a natural way to express guard and continuation optimizations, which remove redundant guards and eliminate redundant code for subsumed occurrences. These optimizations allow CHR programmers to write self-documented rules with a clear logical reading. We show correctness of both optimizations, present an implementation in the K.U.Leuven CHR compiler, and discuss speedup measurements.
---
paper_title: User-definable rule priorities for CHR

paper_content:

This paper introduces CHRrp: Constraint Handling Rules with user-definable rule priorities. CHRrp offers flexible execution control which is lacking in CHR. A formal operational semantics for the extended language is given and is shown to be an instance of the theoretical operational semantics of CHR. It is discussed how the CHR rp semantics influences confluence results. A translation scheme for CHRrp programs with static rule priorities into (regular) CHR is presented. The translation is proven correct and bench-mark results are given. CHRrp is related to priority systems in other constraint programming and rule based languages.
---
paper_title: On Completion of Constraint Handling Rules

paper_content:

Constraint Handling Rules (CHR) is a high-level language for writing constraint solvers either from scratch or by modifying existing solvers. An important property of any constraint solver is confluence: The result of a computation should be independent from the order in which constraints arrive and in which rules are applied. In previous work [1], a sufficient and necessary condition for the confluence of terminating CHR programs was given by adapting and extending results about conditional term rewriting systems. In this paper we investigate so-called completion methods that make a non-confluent CHR program confluent by adding new rules. As it turns out, completion can also exhibit inconsistency of a CHR program. Moreover, as shown in this paper, completion can be used to define new constraints in terms of already existing constraints and to derive constraint solvers for them.
---
paper_title: Abstract Critical Pairs and Confluence of Arbitrary Binary Relations

paper_content:

In a seminal paper, Huet introduced abstract properties of term rewriting systems, and the confluence analysis of terminating term rewriting systems by critical pairs computation. In this paper, we provide an abstract notion of critical pair for arbitrary binary relations and context operators. We show how this notion applies to the confluence analysis of various transition systems, ranging from classical term rewriting systems to production rules with constraints and partial control strategies, such as the Constraint Handling Rules language CHR. Interestingly, we show in all these cases that some classical critical pairs can be disregarded. The crux of these analyses is the ability to compute critical pairs between states built with general context operators, on which a bounded, not necessarily well-founded, ordering is assumed.
---
paper_title: Integration and Optimization of Rule-based Constraint Solvers

paper_content:

One lesson learned from practical constraint solving applications is that constraints are often heterogeneous. Solving such constraints requires a collaboration of constraint solvers. In this paper, we introduce a methodology for the tight integration of CHR constraint programs into one such program. CHR is a high-level rule-based language for writing constraint solvers and reasoning systems. A constraint solver is well-behaved if it is terminating and confluent. When merging constraint solvers, this property may be lost. Based on previous results on CHR program analysis and transformation we show how to utilize completion to regain well-behavedness. We identify a class of solvers whose union is always confluent and we show that for preserving termination such a class is hard to find. The merged and completed constraint solvers may contain redundant rules. Utilizing the notion of operational equivalence, which is decidable for well-behaved CHR programs, we present a method to detect redundant rules in a CHR program.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: Proving termination of CHR in Prolog : A transformational approach

paper_content:

Constraint Handling Rules (CHR) is a concurrent, comitted-choice, logic programming language. It is constraint-based and has guarded rules that rewrite multisets of atomic formulas [1]. Its simple syntax and semantics make it wellsuited for implementing custom constraint solvers. Despite the amount of work directed to CHR, not much has been done on termination analysis. To the best of our knowledge, there were no attempts made to automate termination proofs. The first and, until now, only contribution to termination analysis of CHR is reported in [2] and shows termination of CHR programs under the theoretical semantics [1] of CHR. Termination is shown, using a ranking function, mapping sets of constraints to a well-founded order. A ranking condition, on the level of the rules, implies termination. Although termination conditions in CHR take a different form than in Logic Programs (LP) and Term-Rewrite Systems (TRS), [2] shows that achievements from the work on termination of LP and TRS are relevant and adaptable to the CHR context. In this paper, we present a termination preserving transformation of CHR to Prolog. This allows the direct reuse of termination proof methods from LP and TRS for CHR, yielding the first fully automatic termination proving for CHR. We implemented the transformation and used existing termination tools for LP and TRS on a set of CHR programs to demonstrate the usefulness of our approach. In [3], we formalize the transformation and prove soundness w.r.t. termination.
---
paper_title: A new approach to termination analysis of Constraint Handling Rules

paper_content:

Constraint Handling Rules (CHR) is a concurrent, committed-choice constraint programming language (see [2]). It is a rule-based language, in which multisets of atomic constraints are rewritten using guarded rules. It has a simple syntax and declarative semantics, and is very suitable for implementing constraint solvers. Although the language is strongly related to Logic Programming (LP) and to lesser extent also to Term-Rewrite Systems (TRS), termination analysis of CHR has received little attention. To the best of our knowledge, the only contribution so far is reported in [3]. This study is limited to CHR programs with only one type of rules: the so called ’simplification rules’. The work shows that, for this class of programs, termination analysis techniques developed for LP (see [1]) can be adapted to CHR. In this paper, we present a new approach to termination analysis of CHR which is applicable to a much larger class of CHR programs. We propose a new termination condition and show its applicability to CHR programs with rules that are not only of the simplification type. We have successfully tested the condition on a benchmark of programs, using a prototype analyser.
---
paper_title: The computational power and complexity of constraint handling rules

paper_content:

Constraint Handling Rules (CHR) is a high-level rule-based programming language which is increasingly used for general-purpose programming. We introduce the CHR machine, a model of computation based on the operational semantics of CHR. Its computational power and time complexity properties are compared to those of the well-understood Turing machine and Random Access Memory machine. This allows us to prove the interesting result that every algorithm can be implemented in CHR with the best known time and space complexity. We also investigate the practical relevance of this result and the constant factors involved. Finally we expand the scope of the discussion to other (declarative) programming languages.
---
paper_title: Logical Algorithms

paper_content:

Bottom-up logic programming can be used to declaratively specify many algorithms in a succinct and natural way, and McAllester and Ganzinger have shown that it is possible to define a cost semantics that enables reasoning about the running time of algorithms written as inference rules. Previous work with the programming language Lollimon demonstrates the expressive power of logic programming with linear logic in describing algorithms that have imperative elements or that must repeatedly make mutually exclusive choices. In this paper, we identify a bottom-up logic programming language based on linear logic that is amenable to efficient execution and describe a novel cost semantics that can be used for complexity analysis of algorithms expressed in linear logic.
---
paper_title: Memory Reuse for CHR

paper_content:

Two Constraint Handling Rules compiler optimizations that drastically reduce the memory footprint of CHR programs are introduced. The reduction is the result of reusing suspension terms, the internal CHR constraint representation, and avoiding the overhead of constraint removal followed by insertion. The optimizations are defined formally and their correctness is proved. Both optimizations were implemented in the K.U.Leuven CHR system. Significant memory savings and speedups were measured on classical and well-known benchmarks.
---
paper_title: Complexity of a CHR solver for existentially quantified conjunctions of equations over trees

paper_content:

Constraint Handling Rules (CHR) is a concurrent, committed- choice, rule-based language. One of the first CHR programs is the classic constraint solver for syntactic equality of rational trees that performs unification. We first prove its exponential complexity in time and space for non-flat equations and deduce from this proof a quadratic complexity for flat equations. We then present an extended CHR solver for solving existentially quantified conjunctions of non-flat equations in the theory of finite or infinite trees. We reach a quadratic complexity by first flattening the equations and introducing new existentially quantified variables, then using the classic solver, and finally eliminating particular equations and quantified variables.
---
paper_title: As Time Goes By II: More Automatic Complexity Analysis of Concurrent Rule Programs

paper_content:

Abstract In previous papers we showed that from a suitable termination order (called ranking) one can automatically compute the worst-case time complexity of a CHR constraint simplification rule program from its program text. We combined the worst-case derivation length of a query predicted from its ranking with a worst-case estimate of the number and cost of rule application attempts and the cost of rule applications to obtain the desired meta-theorem. Here we generalize the approach presented in these papers and use it to analyse several non-trivial rule-based constraint solver programs. These results also hold for naive CHR implementations. We also present empirical evidence through test runs that the actual run-time of a state-of-the-art CHR implementation is much better due to optimizations like indexing.
---
paper_title: Logical rules for a lexicographic order constraint solver

paper_content:

We give an executable specification of the global constraint of lexicographic order in Constraint Handling Rules (CHR) language. In contrast to previous approaches, the implementation is short and concise without giving up on linear time worst case time complexity. It is incremental and concurrent by nature of CHR. It is provably correct and confluent. It is independent of the underlying constraint system, and therefore not restricted to finite domains. We also show completeness of constraint propagation, i.e. that all possible consequences of the constraint are generated by the implementation. Our algorithm is encoded by three pairs of rules, two corresponding to base cases, two performing the obvious traversal of the sequences to be compared and two covering a not so obvious special case when the lexicographic constraint has a unique solution.
---
paper_title: Dijkstra’s algorithm with Fibonacci heaps: An executable description

paper_content:

We construct a readable, compact and efficient implementation of Dijkstra’s shortest path algorithm and Fibonacci heaps using Constraint Handling Rules (CHR), which is increasingly used as a high-level rule-based general-purpose programming language. We measure its performance in different CHR systems, investigating both the theoretical asymptotic complexity and the constant factors realized in practice.
---
paper_title: Optimizing compilation of CHR with rule priorities

paper_content:

Constraint Handling Rules were recently extended with user-definable rule priorities. This paper shows how this extended language can be efficiently compiled into the underlying host language. It extends previous work by supporting rules with dynamic priorities and by introducing various optimizations. The effects of the optimizations are empirically evaluated and the new compiler is compared with the state-of-the-art K.U. Leuven CHR system.
---
paper_title: A prolog constraint handling rules compiler and runtime system

paper_content:

The most recent and advanced implementation of constraint handling rules (CHR) is introduced in a logic programming language. The Prolog implementation consists of a runtime system and a compiler. The runtime system utilizes attributed variables for the realization of the constraint store with efficient retrieval and update mechanisms. Rules describing the interactions between constraints are compiled into Prolog clauses by a compiler, the core of which comprises a small number of compact code generating templates in the form of definite clause grammar rules.
---
paper_title: Constraint Handling Rules and tabled execution

paper_content:

Both Constraint Handling Rules (CHR) and tabling – as implemented in XSB – are powerful enhancements of Prolog systems, based on fix point computation. Until now they have only been implemented in separate systems. This paper presents the work involved in porting a CHR system to XSB and in particular the technical issues related to the integration of CHR with tabled resolution. These issues include call abstraction, answer projection, entailment checking, answer combination and tabled constraint store representations. Different optimizations related to tabling constraints are evaluated empirically. The integration requires no changes to the tabling engine. We also show that the performance of CHR programs without tabling is not affected. Now, with the combined power of CHR and tabling, it is possible to easily introduce constraint solvers in applications using tabling, or to use tabling in constraint solvers.
---
paper_title: The K.U.Leuven CHR system: implementation and application

paper_content:

We present the K.U.Leuven CHR system: what started out as a validation of a new attributed variables implementation, has become a part of three different Prolog systems with an increasing userbase. In this paper we highlight the particular implementation aspects of the K.U.Leuven CHR system, and a few CHR applications that we have built with our system.
---
paper_title: CHR for XSB

paper_content:

XSB is a highly declarative programming system consisting of Prolog extended with tabled resolution. It is useful for many tasks, some of which require constraint solving. Thus flexible and high level support for constraint systems is required. Constraint Handling Rules is exactly such a high level language embedded in Prolog for writing application tailored constraint solvers. In this paper we present the integration of a CHR system in the XSB system and especially our findings on how to integrate CHR with tabled resolution, such as how to deal with issues as call abstraction of constraints, constraint store merging, answer store projection and constraint store representations for tabling. We illustrate the power of the XSB-CHR combination with two examples in the field of model checking. It is indeed possible to quickly write application specific constraint solvers, experiment with them and achieve a reasonable performance and high readability. The combination of XSB’s goal-driven fixpoint execution model with CHR’s committed choice bottom-up approach has proven not only feasible, but considerably useful as well.
---
paper_title: Optimizing compilation of constraint handling rules in HAL

paper_content:

In this paper we discuss the optimizing compilation of Constraint Handling Rules (CHRs). CHRs are a multi-headed committed choice constraint language, commonly applied for writing incremental constraint solvers. CHRs are usually implemented as a language extension that compiles to the underlying language. In this paper we show how we can use different kinds of information in the compilation of CHRs to obtain access efficiency, and a better translation of the CHR rules into the underlying language, which in this case is HAL. The kinds of information used include the types, modes, determinism, functional dependencies and symmetries of the CHR constraints. We also show how to analyze CHR programs to determine this information about functional dependencies, symmetries and other kinds of information supporting optimizations.
---
paper_title: Adaptive Constraint Handling with CHR in Java

paper_content:

The most advanced implementation of adaptive constraint processing with Constraint Handling Rules (CHR) is introduced in the imperative object-oriented programming language Java. The presented Java implementation consists of a compiler and a run-time system, all implemented in Java. The run-time system implements data structures like sparse bit vectors, logical variables and terms as well as an adaptive unification and an adaptive entailment algorithm. Approved technologies like attributed variables for constraint storage and retrieval as well as code generation for each head constraint are used. Also implemented are theoretically sound algorithms for adapting of rule derivations and constraint stores after arbitrary constraint deletions. The presentation is rounded off with some novel applications of CHR in constraint processing: simulated annealing for the n queens problem and intelligent backtracking for some SAT benchmark problems.
---
paper_title: Intelligent search strategies based on adaptive Constraint Handling Rules

paper_content:

The most advanced implementation of adaptive constraint processing with Constraint Handling Rules (CHR) allows the application of intelligent search strategies to solve Constraint Satisfaction Problems (CSP). This presentation compares an improved version of conflict-directed backjumping and two variants of dynamic backtracking with respect to chronological backtracking on some of the AIM instances which are a benchmark set of random 3-SAT problems. A CHR implementation of a Boolean constraint solver combined with these different search strategies in Java is thus being compared with a CHR implementation of the same Boolean constraint solver combined with chronological backtracking in SICStus Prolog. This comparison shows that the addition of “intelligence” to the search process may reduce the number of search steps dramatically. Furthermore, the runtime of their Java implementations is in most cases faster than the implementations of chronological backtracking. More specifically, conflict-directed backjumping is even faster than the SICStus Prolog implementation of chronological backtracking, although our Java implementation of CHR lacks the optimisations made in the SICStus Prolog system.
---
paper_title: CHR for imperative host languages

paper_content:

In this paper, we address the different conceptual and technical difficulties encountered when embedding CHR into an imperative host language. We argue that a tight, natural integration leads to a powerful programming language extension, intuitive to both CHR and imperative programmers. We show how to compile CHR to highly optimized imperative code. To this end, we first review the well-established CHR compilation scheme, and survey the large body of possible optimizations. We then show that this scheme, when used for compilation to imperative target languages, leads to stack overflows. We therefore introduce new optimizations that considerably improve the performance of recursive CHR programs. Rules written using tail calls are even guaranteed to run in constant space. We implemented systems for both Java and C, following the language design principles and compilation scheme presented in this paper, and show that our implementations outperform other state-of-the-art CHR compilers by several orders of magnitude.
---
paper_title: Adaptive Constraint Handling with CHR in Java

paper_content:

The most advanced implementation of adaptive constraint processing with Constraint Handling Rules (CHR) is introduced in the imperative object-oriented programming language Java. The presented Java implementation consists of a compiler and a run-time system, all implemented in Java. The run-time system implements data structures like sparse bit vectors, logical variables and terms as well as an adaptive unification and an adaptive entailment algorithm. Approved technologies like attributed variables for constraint storage and retrieval as well as code generation for each head constraint are used. Also implemented are theoretically sound algorithms for adapting of rule derivations and constraint stores after arbitrary constraint deletions. The presentation is rounded off with some novel applications of CHR in constraint processing: simulated annealing for the n queens problem and intelligent backtracking for some SAT benchmark problems.
---
paper_title: The Refined Operational Semantics of Constraint Handling Rules

paper_content:

Constraint Handling Rules (CHRs) are a high-level rule-based programming language commonly used to write constraint solvers. The theoretical operational semantics for CHRs is highly non-deterministic and relies on writing confluent programs to have a meaningful behaviour. Implementations of CHRs use an operational semantics which is considerably finer than the theoretical operational semantics, but is still non-deterministic (from the user’s perspective). This paper formally defines this refined operational semantics and proves it implements the theoretical operational semantics. It also shows how to create a (partial) confluence checker capable of detecting programs which are confluent under this semantics, but not under the theoretical operational semantics. This supports the use of new idioms in CHR programs.
---
paper_title: Projection in adaptive Constraint Handling

paper_content:

Constraint solving in dynamic environments requires an immediate adaptation of the solutions if the constraint problems are changing. Constraint solving with Constraint Handling Rules (CHR) is extended with incremental algorithms, thus supporting the solution of dynamic constraint satisfaction problems (DCSPs). Unfortunately, constraint processing with CHR introduces a lot of new variables which require additional memory space and reduce run-time performance. Most of the variables may be eliminated without any loss of information. Thus, memory may be kept rather small and run-time performance may be improved. This paper describes the use of projection with CHR in order to eliminate irrelevant variable bindings and maintain the constraint store quite small. In detail, some projection algorithms are presented to eliminate variables which are introduced during constraint processing with CHR. Projection is called early projection if it is applied together with each rule application, thus eliminating recently introduced irrelevant variable bindings while keeping the derived constraint store quite small. This kind of projection is well-suited when solving Dynamic Constraint Satisfaction Problems, especially after constraint deletion, when many superfluous variable binding have to be deleted as well. Consequently, the modifications that are required for an adaptation are reduced. This may result in an improved performance of the adaptation algorithms and a better performance for non-adaptive constraint processing with CHR is also expected.
---
paper_title: Extending arbitrary solvers with constraint handling rules

paper_content:

Constraint Handling Rules (CHRs) are a high-level committed choice programming language commonly used to write constraint solvers. While the semantic basis of CHRs allows them to extend arbitrary underlying constraint solvers, in practice, all current implementations only extend Herbrand equation solvers. In this paper we show how to define CHR programs that extend arbitrary solvers and fully interact with them. In the process, we examine how to compile such programs to perform as little recomputation as possible, and describe how to build index structures for CHR constraints that are modified automatically when variables in the underlying solver change. We report on the implementation of these techniques in the HAL compiler, and give empirical results illustrating their benefits.
---
paper_title: Compiling Constraint Handling Rules into Prolog with Attributed Variables

paper_content:

We introduce the most recent and advanced implementation of constraint handling rules (CHR) in a logic programming language, which improves both on previous implementations (in terms of completeness, flexibility and efficiency) and on the principles that should guide such a Prolog implementation consisting of a runtime system and a compiler. The runtime system utilizes attributed variables for the realization of the constraint store with efficient retrieval and update mechanisms. Rules describing the interactions between constraints are compiled into Prolog clauses by a multi-phase compiler, the core of which comprises a small number of compact code generating templates in the form of definite clause grammar rules.
---
paper_title: Translating constraint handling rules into action rules

paper_content:

CHR is a popular high-level language for implementing constraint solvers and other general purpose applications. It has a wellestablished operational semantics and quite a number of different implementations, prominently in Prolog. However, there is still much room for exploring the compilation of CHR to Prolog. Nearly all implementations rely on attributed variables. In this paper, we explore a different implementation target for CHR: B-Prolog’s Action Rules (ARs). As a rule-based language, it is a good match for particular aspects of CHR. However, the strict adherence to CHR’s refined operational semantics poses some difficulty. We report on our work in progress: a novel compilation schema, required changes to the AR language and the preliminary benchmarks and experiences.
---
paper_title: CHR for imperative host languages

paper_content:

In this paper, we address the different conceptual and technical difficulties encountered when embedding CHR into an imperative host language. We argue that a tight, natural integration leads to a powerful programming language extension, intuitive to both CHR and imperative programmers. We show how to compile CHR to highly optimized imperative code. To this end, we first review the well-established CHR compilation scheme, and survey the large body of possible optimizations. We then show that this scheme, when used for compilation to imperative target languages, leads to stack overflows. We therefore introduce new optimizations that considerably improve the performance of recursive CHR programs. Rules written using tail calls are even guaranteed to run in constant space. We implemented systems for both Java and C, following the language design principles and compilation scheme presented in this paper, and show that our implementations outperform other state-of-the-art CHR compilers by several orders of magnitude.
---
paper_title: Optimizing compilation of CHR with rule priorities

paper_content:

Constraint Handling Rules were recently extended with user-definable rule priorities. This paper shows how this extended language can be efficiently compiled into the underlying host language. It extends previous work by supporting rules with dynamic priorities and by introducing various optimizations. The effects of the optimizations are empirically evaluated and the new compiler is compared with the state-of-the-art K.U. Leuven CHR system.
---
paper_title: User-definable rule priorities for CHR

paper_content:

This paper introduces CHRrp: Constraint Handling Rules with user-definable rule priorities. CHRrp offers flexible execution control which is lacking in CHR. A formal operational semantics for the extended language is given and is shown to be an instance of the theoretical operational semantics of CHR. It is discussed how the CHR rp semantics influences confluence results. A translation scheme for CHRrp programs with static rule priorities into (regular) CHR is presented. The translation is proven correct and bench-mark results are given. CHRrp is related to priority systems in other constraint programming and rule based languages.
---
paper_title: The computational power and complexity of constraint handling rules

paper_content:

Constraint Handling Rules (CHR) is a high-level rule-based programming language which is increasingly used for general-purpose programming. We introduce the CHR machine, a model of computation based on the operational semantics of CHR. Its computational power and time complexity properties are compared to those of the well-understood Turing machine and Random Access Memory machine. This allows us to prove the interesting result that every algorithm can be implemented in CHR with the best known time and space complexity. We also investigate the practical relevance of this result and the constant factors involved. Finally we expand the scope of the discussion to other (declarative) programming languages.
---
paper_title: Memory Reuse for CHR

paper_content:

Two Constraint Handling Rules compiler optimizations that drastically reduce the memory footprint of CHR programs are introduced. The reduction is the result of reusing suspension terms, the internal CHR constraint representation, and avoiding the overhead of constraint removal followed by insertion. The optimizations are defined formally and their correctness is proved. Both optimizations were implemented in the K.U.Leuven CHR system. Significant memory savings and speedups were measured on classical and well-known benchmarks.
---
paper_title: Guard and Continuation Optimization for Occurrence Representations of CHR

paper_content:

Constraint Handling Rules (CHR) is a high-level rule-based language extension, commonly embedded in Prolog. We introduce a new occurrence representation of CHR programs, and a new operational semantics for occurrence representations, equivalent to the widely implemented refined operational semantics. The occurrence representation allows in a natural way to express guard and continuation optimizations, which remove redundant guards and eliminate redundant code for subsumed occurrences. These optimizations allow CHR programmers to write self-documented rules with a clear logical reading. We show correctness of both optimizations, present an implementation in the K.U.Leuven CHR compiler, and discuss speedup measurements.
---
paper_title: Optimizing compilation of constraint handling rules in HAL

paper_content:

In this paper we discuss the optimizing compilation of Constraint Handling Rules (CHRs). CHRs are a multi-headed committed choice constraint language, commonly applied for writing incremental constraint solvers. CHRs are usually implemented as a language extension that compiles to the underlying language. In this paper we show how we can use different kinds of information in the compilation of CHRs to obtain access efficiency, and a better translation of the CHR rules into the underlying language, which in this case is HAL. The kinds of information used include the types, modes, determinism, functional dependencies and symmetries of the CHR constraints. We also show how to analyze CHR programs to determine this information about functional dependencies, symmetries and other kinds of information supporting optimizations.
---
paper_title: CHR for imperative host languages

paper_content:

In this paper, we address the different conceptual and technical difficulties encountered when embedding CHR into an imperative host language. We argue that a tight, natural integration leads to a powerful programming language extension, intuitive to both CHR and imperative programmers. We show how to compile CHR to highly optimized imperative code. To this end, we first review the well-established CHR compilation scheme, and survey the large body of possible optimizations. We then show that this scheme, when used for compilation to imperative target languages, leads to stack overflows. We therefore introduce new optimizations that considerably improve the performance of recursive CHR programs. Rules written using tail calls are even guaranteed to run in constant space. We implemented systems for both Java and C, following the language design principles and compilation scheme presented in this paper, and show that our implementations outperform other state-of-the-art CHR compilers by several orders of magnitude.
---
paper_title: Dijkstra’s algorithm with Fibonacci heaps: An executable description

paper_content:

We construct a readable, compact and efficient implementation of Dijkstra’s shortest path algorithm and Fibonacci heaps using Constraint Handling Rules (CHR), which is increasingly used as a high-level rule-based general-purpose programming language. We measure its performance in different CHR systems, investigating both the theoretical asymptotic complexity and the constant factors realized in practice.
---
paper_title: Unfolding in CHR

paper_content:

Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption and more generally to optimize a given program. Essentially it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. One of the basic operations which is used by most program transformation systems is unfolding which consists in the replacement of a procedure call by its definition. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages and, to the best of our knowledge, no one has considered unfolding of CHR programs. This paper is a first attempt to define a correct unfolding system for CHR programs. We define an unfolding rule, show its correctness and discuss some conditions which can be used to delete an unfolded rule while preserving the program meaning.
---
paper_title: Aggregates for CHR through program transformation

paper_content:

We propose an extension of Constraint Handling Rules (CHR) with aggregates such as sum , count , findall , and min . This new feature significantly improves the conciseness and expressiveness of the language. In this paper, we describe an implementation based on source-to-source transformations to CHR (extended with some low-level compiler directives). We allow user-defined aggregates and nested aggregate expressions over arbitrary guarded conjunctions of constraints. Both an on-demand and an incremental aggregate computation strategy are supported.
---
paper_title: Specialization of Concurrent Guarded Multi-Set Transformation Rules

paper_content:

Program transformation and in particular partial evaluation are appealing techniques for declarative programs to improve not only their performance. This paper presents the first step towards developing program transformation techniques for a concurrent constraint programming language where guarded rules rewrite and augment multi-sets of atomic formulae, called Constraint Handling Rules (CHR). ::: ::: We study the specialization of rules with regard to a given goal (query). We show the correctness of this program transformation: Adding and removing specialized rules in a program does not change the program's operational semantics. Furthermore termination and confluence of the program are shown to be preserved.
---
paper_title: A type system for CHR

paper_content:

The language of Constraint Handling Rules (CHR) of T. Fruhwirth [1] is a successful rule-based language for implementing constraint solvers in a wide variety of domains. It is an extension of a host language, such as Prolog [2], Java or Haskell [3], allowing the introduction of new constraints in a declarative way. One peculiarity of CHR is that it allows multiple heads in rules. For the sake of simplicity, we consider only simpli.cation rules, since the distinction of propagation and simpagation rules [1] is not needed for typing purposes. A simpli.cation rule is of the form $H_{1},...,H_{i} \Leftrightarrow G_{1},...,G_{j}|B_{1},...,B_{k}$, where H1,...,Hi is a nonempty sequence of CHR constraints, the guard G1,...,Gj is a sequence of native constraints and the body B1,...,Bk is a sequence of CHR and native constraints.
---
paper_title: Probabilistic Constraint Handling Rules

paper_content:

Abstract Classical Constraint Handling Rules (CHR) provide a powerful tool for specifying and implementing constraint solvers and programs. The rules of CHR rewrite constraints (non-deterministically) into simpler ones until they are solved. In this paper we introduce an extension of Constraint Handling Rules (CHR), namely Probabilistic CHRs (PCHR). These allow the probabilistic “weighting” of rules, specifying the probability of their application. In this way we are able to formalise various randomised algorithms such as for example Simulated Annealing. The implementation is based on source-to-source transformation (STS). Using a recently developed prototype for STS for CHR, we could implement probabilistic CHR in a concise way with a few lines of code in less than one hour.
---
paper_title: Constraint Handling Rules and tabled execution

paper_content:

Both Constraint Handling Rules (CHR) and tabling – as implemented in XSB – are powerful enhancements of Prolog systems, based on fix point computation. Until now they have only been implemented in separate systems. This paper presents the work involved in porting a CHR system to XSB and in particular the technical issues related to the integration of CHR with tabled resolution. These issues include call abstraction, answer projection, entailment checking, answer combination and tabled constraint store representations. Different optimizations related to tabling constraints are evaluated empirically. The integration requires no changes to the tabling engine. We also show that the performance of CHR programs without tabling is not affected. Now, with the combined power of CHR and tabling, it is possible to easily introduce constraint solvers in applications using tabling, or to use tabling in constraint solvers.
---
paper_title: Adaptive Constraint Handling with CHR in Java

paper_content:

The most advanced implementation of adaptive constraint processing with Constraint Handling Rules (CHR) is introduced in the imperative object-oriented programming language Java. The presented Java implementation consists of a compiler and a run-time system, all implemented in Java. The run-time system implements data structures like sparse bit vectors, logical variables and terms as well as an adaptive unification and an adaptive entailment algorithm. Approved technologies like attributed variables for constraint storage and retrieval as well as code generation for each head constraint are used. Also implemented are theoretically sound algorithms for adapting of rule derivations and constraint stores after arbitrary constraint deletions. The presentation is rounded off with some novel applications of CHR in constraint processing: simulated annealing for the n queens problem and intelligent backtracking for some SAT benchmark problems.
---
paper_title: Projection in adaptive Constraint Handling

paper_content:

Constraint solving in dynamic environments requires an immediate adaptation of the solutions if the constraint problems are changing. Constraint solving with Constraint Handling Rules (CHR) is extended with incremental algorithms, thus supporting the solution of dynamic constraint satisfaction problems (DCSPs). Unfortunately, constraint processing with CHR introduces a lot of new variables which require additional memory space and reduce run-time performance. Most of the variables may be eliminated without any loss of information. Thus, memory may be kept rather small and run-time performance may be improved. This paper describes the use of projection with CHR in order to eliminate irrelevant variable bindings and maintain the constraint store quite small. In detail, some projection algorithms are presented to eliminate variables which are introduced during constraint processing with CHR. Projection is called early projection if it is applied together with each rule application, thus eliminating recently introduced irrelevant variable bindings while keeping the derived constraint store quite small. This kind of projection is well-suited when solving Dynamic Constraint Satisfaction Problems, especially after constraint deletion, when many superfluous variable binding have to be deleted as well. Consequently, the modifications that are required for an adaptation are reduced. This may result in an improved performance of the adaptation algorithms and a better performance for non-adaptive constraint processing with CHR is also expected.
---
paper_title: CHR: A Flexible Query Language

paper_content:

We show how the language Constraint Handling Rules (CHR), a high-level logic language for the implementation of constraint solvers, can be slightly extended to become a general-purpose logic programming language with an expressive power subsuming the expressive ower of Horn clause programs with SLD resolution. The extended language, called “CHR∀”, retains however the extra features of CHR, e.g., committed choice and matching, which axe important for other purposes, especially for efficiently solving constraints. CHR∀ turns out to be a very flexible query language in the sense that it supports several (constraint) logic programming paradigms and allows to mix them in a single program. In particular, it supports top-down query evaluation and also bottom-up evaluation as it is frequently used in (disjunctive) deductive databases.
---
paper_title: Constraint Programming Architectures : Review and a New Proposal

paper_content:

Most automated reasoning tasks with practical applications can be automatically reformulated into a constraint solving task. A constraint programming platform can thus act as a unique, underlying engine to be reused for multiple automated reasoning tasks in intelligent agents and systems. We identify six key requirements for such platform: expressive task modeling language, rapid solving method customization and combination, adaptive solving method, user-friendly solution explanation, efficient execution, and seamless integration within larger systems and practical applications. We then propose a novel, model-driven, component and rule-based architecture for such a platform that better satisfies as a whole this set of requirements than those of currently available platforms.
---
paper_title: Intelligent search strategies based on adaptive Constraint Handling Rules

paper_content:

The most advanced implementation of adaptive constraint processing with Constraint Handling Rules (CHR) allows the application of intelligent search strategies to solve Constraint Satisfaction Problems (CSP). This presentation compares an improved version of conflict-directed backjumping and two variants of dynamic backtracking with respect to chronological backtracking on some of the AIM instances which are a benchmark set of random 3-SAT problems. A CHR implementation of a Boolean constraint solver combined with these different search strategies in Java is thus being compared with a CHR implementation of the same Boolean constraint solver combined with chronological backtracking in SICStus Prolog. This comparison shows that the addition of “intelligence” to the search process may reduce the number of search steps dramatically. Furthermore, the runtime of their Java implementations is in most cases faster than the implementations of chronological backtracking. More specifically, conflict-directed backjumping is even faster than the SICStus Prolog implementation of chronological backtracking, although our Java implementation of CHR lacks the optimisations made in the SICStus Prolog system.
---
paper_title: Adaptive CHR meets CHR ∨ : An extended refined operational semantics for CHR ∨ based on justifications

paper_content:

A system and method for electronically exchanging information related to telecommunication services includes separating data representing the information to be exchanged into predefined segments corresponding to telecommunication services, associating a segment identification code with each segment, and grouping each segment identification code with corresponding data. The system and method also include concatenating the segment identification codes and associated data according to a predefined sequence to form an electronic transaction and transmitting the electronic message to a telecommunications wholesaler or reseller. Preferably, the information is exchanged over a TCP/IP connection in an interactive, transaction-based exchange.
---
paper_title: Aggregates for CHR through program transformation

paper_content:

We propose an extension of Constraint Handling Rules (CHR) with aggregates such as sum , count , findall , and min . This new feature significantly improves the conciseness and expressiveness of the language. In this paper, we describe an implementation based on source-to-source transformations to CHR (extended with some low-level compiler directives). We allow user-defined aggregates and nested aggregate expressions over arbitrary guarded conjunctions of constraints. Both an on-demand and an incremental aggregate computation strategy are supported.
---
paper_title: Aggregates for Constraint Handling Rules

paper_content:

Constraint Handling Rules (CHR) [2,3,4] is a general-purpose programming language based on committed-choice, multi-headed, guarded multiset rewrite rules. As the head of each CHR rule only considers a fixed number of constraints, any form of aggregation over unbounded parts of the constraint store necessarily requires explicit encoding, using auxiliary constraints and rules.
---
paper_title: Extending arbitrary solvers with constraint handling rules

paper_content:

Constraint Handling Rules (CHRs) are a high-level committed choice programming language commonly used to write constraint solvers. While the semantic basis of CHRs allows them to extend arbitrary underlying constraint solvers, in practice, all current implementations only extend Herbrand equation solvers. In this paper we show how to define CHR programs that extend arbitrary solvers and fully interact with them. In the process, we examine how to compile such programs to perform as little recomputation as possible, and describe how to build index structures for CHR constraints that are modified automatically when variables in the underlying solver change. We report on the implementation of these techniques in the HAL compiler, and give empirical results illustrating their benefits.
---
paper_title: A Unified Semantics for Constraint Handling Rules in Transaction Logic

paper_content:

Reasoning on Constraint Handling Rules (CHR) programs and their executional behaviour is often ad-hoc and outside of a formal system. This is a pity, because CHR subsumes a wide range of important automated reasoning services. Mapping CHR to Transaction Logic (τ R) combines CHR rule specification, CHR rule application, and reasoning on CHR programs and CHR derivations inside one formal system which is executable. This new τ R semantics obviates the need for disjoint declarative and operational semantics.
---
paper_title: A linear-logic semantics for constraint handling rules

paper_content:

One of the attractive features of the Constraint Handling Rules (CHR) programming language is its declarative semantics where rules are read as formulae in first-order predicate logic. However, the more CHR is used as a general-purpose programming language, the more the limitations of that kind of declarative semantics in modelling change become apparent. We propose an alternative declarative semantics based on (intuitionistic) linear logic, establishing strong theorems on both soundness and completeness of the new declarative semantics w.r.t. operational semantics.
---
paper_title: ACD Term Rewriting

paper_content:

In this paper we introduce Associative Commutative Distributive Term Rewriting (ACDTR), a rewriting language for rewriting logical formulae. ACDTR extends AC term rewriting by adding distribution of conjunction over other operators. Conjunction is vital for expressive term rewriting systems since it allows us to require that multiple conditions hold for a term rewriting rule to be used. ACDTR uses the notion of a conjunctive context, which is the conjunction of constraints that must hold in the context of a term, to enable the programmer to write very expressive and targeted rewriting rules. ACDTR can be seen as a general logic programming language that extends Constraint Handling Rules and AC term rewriting. In this paper we define the semantics of ACDTR and describe our prototype implementation.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: Logical Algorithms

paper_content:

Bottom-up logic programming can be used to declaratively specify many algorithms in a succinct and natural way, and McAllester and Ganzinger have shown that it is possible to define a cost semantics that enables reasoning about the running time of algorithms written as inference rules. Previous work with the programming language Lollimon demonstrates the expressive power of logic programming with linear logic in describing algorithms that have imperative elements or that must repeatedly make mutually exclusive choices. In this paper, we identify a bottom-up logic programming language based on linear logic that is amenable to efficient execution and describe a novel cost semantics that can be used for complexity analysis of algorithms expressed in linear logic.
---
paper_title: Observable confluence for constraint handling rules

paper_content:

Constraint Handling Rules (CHR) are a powerful rule based language for specifying constraint solvers. Critical for any rule based language is the notion of confluence, and for terminating CHR programs there is a decidable test for confluence. But many CHR programs that are in practice confluent fail this confluence test. The problem is that the states that illustrate non-confluence are not observable from the initial goals of interest. In this paper we introduce the notion of observable confluence, a more general notion of confluence which takes into account whether states are observable. We devise a test for observable confluence which allows us to verify observable confluence for a range of CHR programs dealing with agents, type systems, and the union-find algorithm.
---
paper_title: Optimal placement of base stations in wireless indoor telecommunication

paper_content:

Planning of local wireless communication networks is about installing base stations (small radio transmitters) to provide wireless devices with strong enough signals. POPULAR is an advanced industrial prototype that allows to compute the minimal number of base stations and their location given a blue-print of the installation site and information about the materials used for walls and ceilings. It does so by simulating the propagation of radio-waves using ray tracing and by subsequent optimization of the number of base stations needed to cover the whole building. Taking advantage of state-of-the-art techniques for programmable application-oriented constraint solving, POPULAR is among the first practical tools that can optimally plan wireless communication networks.
---
paper_title: The Munich Rent Advisor: A Success for Logic Programming on the Internet

paper_content:

Most cities in Germany regularly publish a booklet called the Mietspiegel. It basically contains a verbal description of an expert system. It allows the calculation of the estimated fair rent for a flat. By hand, one may need a weekend to do this task. With our computerized version, the Munich Rent Advisor, the user just fills in a form in a few minutes, and the rent is calculated immediately. We also extended the functionality and applicability of the Mietspiegel so that the user need not answer all questions on the form. The key to computing with partial information using high-level programming was to use constraint logic programming. We rely on the Internet, and more specifically the World Wide Web, to provide this service to a broad user group, the citizens of Munich and the people who are planning to move to Munich. To process the answers from the questionnaire and return its result, we wrote a small simple stable special-purpose web server directly in ECLiPSe. More than 10,000 people have used our service in the last three years. This article describes the experiences in implementing and using the Munich Rent Advisor. Our results suggest that logic programming with constraints can be an important ingredient in intelligent internet systems.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: A constraint solver for sequences and its applications

paper_content:

Constraint programming techniques are successfully used in various areas of software engineering for industry, commerce, transport, finance etc. Constraint solvers for different data types are applied in validation and verification of programs containing data elements of these types. A general constraint solver for sequences is necessary to take into account this data type in the existing validation and verification tools. In this work, we present an original constraint solver for sequences implemented in CHR and based on T. Fruhwirth's solver for lists with the propagation of two constraints: generalized concatenation and size. The applications of the solver (with the validation and verification tool BZTT) to different software engineering problems are illustrated by the example of a waiting room model.
---
paper_title: Toward a first-order extension of Prolog's unification using CHR: a CHR first-order constraint solver over finite or infinite trees

paper_content:

Prolog, which stands for PROgramming in LOGic, is the most widely used language in the logic programming paradigm. One of its main concepts is unification. It represents the mechanism of binding the contents of variables and can be seen as solving conjunctions of equations over finite or infinite trees. We present in this paper an idea of a first-order extension of Prolog's unification by giving a general algorithm for solving any first-order constraint in the theory T of finite or infinite trees, extended by a relation which allows to distinguish between finite and infinite trees. The algorithm is given in the form of 16 rewriting rules which transform any first-order formula ' into an equivalent disjunction D of simple formulas in which the solutions of the free variables are expressed in a clear and explicit way. We end this paper describing a CHR implementation of our algorithm. CHR (Constraint Handling Rules) has originally been developed for writing constraint solvers, but the constraints here go much beyond implicitly quantified conjunctions of atomic constraints and are considered as arbitrary first-order formulas built on the signature of T. We discuss how we implement nested local constraint stores and what programming patterns and language features we found useful in the CHR implementation of our algorithm.
---
paper_title: Complexity of a CHR solver for existentially quantified conjunctions of equations over trees

paper_content:

Constraint Handling Rules (CHR) is a concurrent, committed- choice, rule-based language. One of the first CHR programs is the classic constraint solver for syntactic equality of rational trees that performs unification. We first prove its exponential complexity in time and space for non-flat equations and deduce from this proof a quadratic complexity for flat equations. We then present an extended CHR solver for solving existentially quantified conjunctions of non-flat equations in the theory of finite or infinite trees. We reach a quadratic complexity by first flattening the equations and introducing new existentially quantified variables, then using the classic solver, and finally eliminating particular equations and quantified variables.
---
paper_title: Adaptive Constraint Handling with CHR in Java

paper_content:

The most advanced implementation of adaptive constraint processing with Constraint Handling Rules (CHR) is introduced in the imperative object-oriented programming language Java. The presented Java implementation consists of a compiler and a run-time system, all implemented in Java. The run-time system implements data structures like sparse bit vectors, logical variables and terms as well as an adaptive unification and an adaptive entailment algorithm. Approved technologies like attributed variables for constraint storage and retrieval as well as code generation for each head constraint are used. Also implemented are theoretically sound algorithms for adapting of rule derivations and constraint stores after arbitrary constraint deletions. The presentation is rounded off with some novel applications of CHR in constraint processing: simulated annealing for the n queens problem and intelligent backtracking for some SAT benchmark problems.
---
paper_title: On Incremental Adaptation of CHR Derivations

paper_content:

Constraint-solving in dynamic environments requires the immediate adaptation of solutions of constraint satisfaction problems if these problems are changing. After any change, an adapted solution is preferred which is stable, i.e., as close as possible to the original solution. A wide range of incremental constraint-solving methods for dynamic, especially finite-domain, constraint satisfaction problems (DCSPs) are known, which more or less satisfy this additional requirement. Adaptation of DCSPs after constraint additions is generally simple and successfully solved, but adaptation after arbitrary constraint deletions is not. How constraint handling rules (CHRs), a high level language extension for implementing constraint solvers, can be improved in this respect is investigated. A new incremental algorithm is presented, which adapts an arbitrary CHR derivation after eliminations of constraints in the processed DCSPs. Thus, the existing solvers - there are several dozens of them - for various kinds of const...
---
paper_title: Soft Constraint Propagation and Solving in Constraint Handling Rules

paper_content:

Soft constraints are a generalization of classical constraints, which allow for the description of preferences rather than strict requirements. In soft constraints, constraints and partial assignments are given preference or importance levels, and constraints are combined according to combinators which express the desired optimization criteria. On the other hand, constraint handling rules (CHR) constitute a high-level natural formalism to specify constraint solvers and propagation algorithms. We present a framework to design and specify soft constraint solvers by using CHR. In this way, we extend the range of applicability of CHR to soft constraints rather than just classical ones, and we provide a straightforward implementation for soft constraint solvers.
---
paper_title: Qualitative Spatial Reasoning: Theory and Practice: Application to Robot Navigation

paper_content:

With the aim of automatically reasoning with spatial aspects in a cognitive way, several qualitative models have been developed recently in the field of qualitative spatial reasoning. However, most of these models simplify spatial objects to points, and, to date, there is no model to reason with several spatial aspects in a uniform way. This work provides an approach for integrating the qualitative concepts of orientation, distance, and cardinal directions, using points as well as extended objects as primitive of reasoning, based on Constraint Logic Programming. The resulting model has been applied to build a qualitative Navigation Simulator on the structured environment of the city of Castellon.
---
paper_title: A Framework Based on CLP Extended with CHRs for Reasoning with Qualitative Orientation and Positional Information

paper_content:

Several qualitative models have been developed in the last years with the aim of simulating the spatial reasoning process used by humans. However, up to now no model has been developed to represent and reason with several aspects of space (such as orientation, distance and cardinal directions, for instance) in a uniform way, i.e. by referring to the same spatial objects. An approach for the integration of several aspects of space into the same model, based on constraint logic programming extended with constraint handling rules, is proposed in this article. As an example of this approach, the integration of orientation and positional information in the same model is explained.
---
paper_title: Modeling Motion by the Integration of Topology and Time

paper_content:

A qualitative representational model and the corresponding reasoning process for integrating time and topological information is developed in this paper. In the calculus presented, topological information in function of the point of the time in which it is true is represented as an instance of the Constraint Satisfaction Problem. The resulting method can be applied to qualitative navigation of autonomous agents. The model presented in this paper will help us during the path planning task by describing the sequence of topological situations that the agent should find during its way to the target objective. A preliminary result of that application has been obtained by using qualitative representation of such spatial aspects for the autonomous simulated navigation of a Nomad-200 robot, on a structured environment of an easy corridor in a building.
---
paper_title: Reasoning about Actions with CHRs and Finite Domain Constraints

paper_content:

We present a CLP-based approach to reasoning about actions in the presence of incomplete states. Constraints expressing negative and disjunctive state knowledge are processed by a set of special Constraint Handling Rules. In turn, these rules reduce to standard finite domain constraints when handling variable arguments of single state components. Correctness of the approach is proved against the general action theory of the Fluent Calculus. The constraint solver is used as the kernel of a high-level programming language for agents that reason and plan. Experiments have shown that the constraint solver exhibits excellent computational behavior and scales up well.
---
paper_title: M.: Fluxplayer: A successful general game player

paper_content:

General Game Playing (GGP) is the art of designing programs that are capable of playing previously unknown games of a wide variety by being told nothing but the rules of the game. This is in contrast to traditional computer game players like Deep Blue, which are designed for a particular game and can't adapt automatically to modifications of the rules, let alone play completely different games. General Game Playing is intended to foster the development of integrated cognitive information processing technology. In this article we present an approach to General Game Playing using a novel way of automatically constructing a position evaluation function from a formal game description. Our system is being tested with a wide range of different games. Most notably, it is the winner of the AAAI GGP Competition 2006.
---
paper_title: Observable confluence for constraint handling rules

paper_content:

Constraint Handling Rules (CHR) are a powerful rule based language for specifying constraint solvers. Critical for any rule based language is the notion of confluence, and for terminating CHR programs there is a decidable test for confluence. But many CHR programs that are in practice confluent fail this confluence test. The problem is that the states that illustrate non-confluence are not observable from the initial goals of interest. In this paper we introduce the notion of observable confluence, a more general notion of confluence which takes into account whether states are observable. We devise a test for observable confluence which allows us to verify observable confluence for a range of CHR programs dealing with agents, type systems, and the union-find algorithm.
---
paper_title: Semantic Web Reasoning for Ontology-Based Integration of Resources

paper_content:

The Semantic Web should enhance the current World Wide Web with reasoning capabilities for enabling automated processing of possibly distributed information. In this paper we describe an architecture for Semantic Web reasoning and query answering in a very general setting involving several heterogeneous information sources, as well as domain ontologies needed for offering a uniform and source-independent view on the data. Since querying a Web source is very costly in terms of response time, we focus mainly on the query planner of such a system, as it may allow avoiding the access to query-irrelevant sources or combinations of sources based on knowledge about the domain and the sources.
---
paper_title: Information Integration Using Contextual Knowledge and Ontology Merging

paper_content:

With the advances in telecommunications, and the introduction of the Internet, information systems achieved physical connectivity, but have yet to establish logical connectivity. Lack of logical connectivity is often inviting disaster as in the case of Mars Orbiter, which was lost because one team used metric units, the other English while exchanging a critical maneuver data. In this Thesis, we focus on the two intertwined sub problems of logical connectivity, namely data extraction and data interpretation in the domain of heterogeneous information systems. ::: The first challenge, data extraction, is about making it possible to easily exchange data among semi-structured and structured information systems. We describe the design and implementation of a general purpose, regular expression based Cameleon wrapper engine with an integrated capabilities-aware planner/optimizer/executioner. ::: The second challenge, data interpretation, deals with the existence of heterogeneous contexts, whereby each source of information and potential receiver of that information may operate with a different context, leading to large-scale semantic heterogeneity. We extend the existing formalization of the COIN framework with new logical formalisms and features to handle larger set of heterogeneities between data sources. This extension, named Extended Context Interchange (ECOIN), is motivated by our analysis of financial information systems that indicates that there are three fundamental types of heterogeneities in data sources: contextual, ontological, and temporal. ::: While COIN framework was able to deal with the contextual heterogeneities, ECOIN framework expands the scope to include ontological heterogeneities as well. In particular, we are able to deal with equational ontological conflicts (EOC), which refer to the heterogeneity in the way data items are calculated from other data items in terms of definitional equations. ECOIN provides a context-based solution to the EOC problem based on a novel approach that integrates abductive reasoning and symbolic equation solving techniques in a unified framework. ::: Furthermore, we address the merging of independently built ECOIN applications, which involves merging disparate ontologies and contextual knowledge. The relationship between ECOIN and the Semantic Web is also discussed. ::: Finally, we demonstrate the feasibility and features of our integration approach with a prototype implementation that provides mediated access to heterogeneous information systems. (Copies available exclusively from MIT Libraries, Rm. 14-0551, Cambridge, MA 02139-4307. Ph. 617-253-5668; Fax 617-253-1690.)
---
paper_title: APPLICATION-SPECIFIC CONSTRAINTS FOR MULTIMEDIA PRESENTATION GENERATION

paper_content:

A multimedia presentation can be viewed as a collection of multimedia items (such as image, text, video and audio), along with detailed information that describes the spatial and temporal placement of the items as part of the presentation. Manual multimedia authoring involves explicitly stating the placement of each media item in the spatial and temporal dimensions. The drawback of this approach is that resulting presentations are hard to adapt to different target platforms, network resources, and user preferences. An approach to solving this problem is to abstract from the low-level presentation details, for example by specifying the high-level semantic relations between the media items. The presentation itself can then be generated from the semantic relations along with a generic set of transformation rules, specifying how each semantic relation can be conveyed using multimedia constructs. These constructs may differ depending on the target platform, current network conditions or user preferences. We are thus able to automatically adapt the presentation to a wide variety of different circumstances while ensuring that the underlying message of the presentation remains the same. This approach requires an execution environment in which transformation rules, resulting in a set of constraints, are derived from a given semantic description. The resulting set of constraints can then be solved to create a final multimedia presentation. The paper describes the design and implementation of such a system. It explains the advantages of using constraint logic programming to realize the implementation of both the transformation rules and the constraints system. It also demonstrates the need for two different types of constraints. Quantitative constraints are needed to verify whether the final form presentation meets all the numeric constraints that are required by the environment. Qualitative constraints are needed to facilitate high-level reasoning and presentation encoding. While the quantitative constraints can be handled by off-the-shelf constraint solvers, the qualitative constraints needed are specific to the multimedia domain and need to be defined explicitly.
---
paper_title: Answering Queries in Context

paper_content:

The emergence of the Internet as the de facto Global Information Infrastructure enables the construction of decision support systems that leverage on the panoply of on-line information sources. This highly dynamic environment presents a critical need for a flexible and scalable strategy for integrating the disparate information sources while respecting their autonomy.
---
paper_title: ARM: Automatic Rule Miner

paper_content:

Rule-based formalisms are ubiquitous in computer science. However, a difficulty that arises frequently when specifying or programming the rules is 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 functionality 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 rule-based constraint solvers. Thus, it is suitable for users from different fields.
---
paper_title: Automatic generation of rule-based constraint solvers over finite domains

paper_content:

A general approach to implement propagation and simplification of constraints consists of applying rules over these constraints. However, a difficulty that arises frequently when writing a constraint solver is to determine the constraint propagation algorithm. In this article, we propose a method for generating propagation and simplification rules for constraints over finite domains defined extensionally by, for example, a truth table or their tuples. The generation of rules is performed in two steps. First, propagation rules are generated. Propagation rules do not rewrite constraints but add new ones. Thus, the constraint store may contain superfluous constraints. Removing these constraints not only allows saving of space but also decreases the cost of constraint solving. Constraints can be removed using simplification rules. Thus, in a second step, some propagation rules are transformed into simplification rules.Furthermore, we show that our approach performs well on various examples, including Boolean constraints, multivalued logic, and Allen's qualitative approach to temporal logic. Moreover, an application taken from the field of digital circuit design shows that our approach is of practical use.
---
paper_title: Constraint Programming viewed as Rule-based Programming

paper_content:

We study here a natural situation when constraint programming can be entirely reduced to rule-based programming. To this end we explain first how one can compute on constraint satisfaction problems using rules represented by simple first-order formulas. Then we consider constraint satisfaction problems that are based on predefined, explicitly given constraints. To solve them we first derive rules from these explicitly given constraints and limit the computation process to a repeated application of these rules, combined with labeling. We consider two types of rule here. The first type, that we call equality rules, leads to a new notion of local consistency, called rule consistency that turns out to be weaker than arc consistency for constraints of arbitrary arity (called hyper-arc consistency in Marriott & Stuckey (1998)). For Boolean constraints rule consistency coincides with the closure under the well-known propagation rules for Boolean constraints. The second type of rules, that we call membership rules, yields a rule-based characterization of arc consistency. To show feasibility of this rule-based approach to constraint programming, we show how both types of rules can be automatically generated, as CHR rules of Fruhwirth (1995). This yields an implementation of this approach to programming by means of constraint logic programming. We illustrate the usefulness of this approach to constraint programming by discussing various examples, including Boolean constraints, two typical examples of many valued logics, constraints dealing with Waltz's language for describing polyhedral scenes, and Allen's qualitative approach to temporal logic.
---
paper_title: The computational power and complexity of constraint handling rules

paper_content:

Constraint Handling Rules (CHR) is a high-level rule-based programming language which is increasingly used for general-purpose programming. We introduce the CHR machine, a model of computation based on the operational semantics of CHR. Its computational power and time complexity properties are compared to those of the well-understood Turing machine and Random Access Memory machine. This allows us to prove the interesting result that every algorithm can be implemented in CHR with the best known time and space complexity. We also investigate the practical relevance of this result and the constant factors involved. Finally we expand the scope of the discussion to other (declarative) programming languages.
---
paper_title: Dijkstra’s algorithm with Fibonacci heaps: An executable description

paper_content:

We construct a readable, compact and efficient implementation of Dijkstra’s shortest path algorithm and Fibonacci heaps using Constraint Handling Rules (CHR), which is increasingly used as a high-level rule-based general-purpose programming language. We measure its performance in different CHR systems, investigating both the theoretical asymptotic complexity and the constant factors realized in practice.
---
paper_title: Principal type inference for GHCstyle multi-parameter type classes

paper_content:

We observe that the combination of multi-parameter type classes with existential types and type annotations leads to a loss of principal types and undecidability of type inference. This may be a surprising fact for users of these popular features. We conduct a concise investigation of the problem and are able to give a type inference procedure which, if successful, computes principal types under the conditions imposed by the Glasgow Haskell Compiler (GHC). Our results provide new insights on how to perform type inference for advanced type extensions.
---
paper_title: Polymorphic algebraic data type reconstruction

paper_content:

One of the disadvantages of statically typed languages is the programming overhead caused by writing all the necessary type information: Both type declarations and type definitions are typically required. Traditional type inference aims at relieving the programmer from the former.We present a rule-based constraint rewriting algorithm that reconstructs both type declarations and type definitions, allowing the programmer to effectively program type-less in a strictly typed language. This effectively combines strong points of dynamically typed languages (rapid prototyping) and statically typed ones (documentation, optimized compilation). Moreover it allows to quickly port code from a statically untyped to a statically typed setting.Our constraint-based algorithm reconstructs uniform polymorphic definitions of algebraic data types and simultaneously infers the types of all expressions and functions (supporting polymorphic recursion) in the program. The declarative nature of the algorithm allows us to easily show that it has a number of highly desirable properties such as soundness, completeness and various optimality properties. Moreover, we show how to easily extend and adapt it to suit a number of different language constructs and type system features
---
paper_title: A flow-based approach for variant parametric types

paper_content:

A promising approach for type-safe generic codes in the object-oriented paradigm is variant parametric type, which allows covariant and contravariant subtyping on fields where appropriate. Previous approaches formalise variant type as a special case of the existential type system. In this paper, we present a new framework based on flow analysis and modular type checking to provide a simple but accurate model for capturing generic types. Our scheme stands to benefit from past (and future) advances in flow analysis and subtyping constraints. Furthermore, it fully supports casting for variant types with a special reflection mechanism, called cast capture, to handle objects with unknown types. We have built a constraint-based type checker and have proven its soundness. We have also successfully annotated a suite of Java libraries and client code with our flow-based variant type system.
---
paper_title: Type inference and type error diagnosis for Hind-ley/Milner with extensions

paper_content:

An improved tool in the form of a tooth forming rack for cold working a cylindrical workpiece to form teeth thereon to produce, for example, a toothed gear is provided. The rack comprises a plurality of releasable inserts mounted on a tool holder. The inserts are of the throw-away type which enables replacement of only that portion of the rack that is worn or broken, thus extending the ueful life of the entire rack. In a first embodiment the inserts are releasably attached to the tool holder by threaded capscrews. In an alternate embodiment a milled slot within the inserts permits retention by means of tapered retainers attached to the tool holder by threaded capscrews.
---
paper_title: Interpreting Abduction in CLP

paper_content:

Constraint Logic Programming (CLP) and Abductive Logic Programming (ALP) share the important concept of conditional answer. We exploit their deep similarities to implement an ecient abductive solver where abducibles are treated as constraints. We propose two pos- sible implementations, in which integrity constraints are exploited either (i) as the definition of a CLP solver on an abductive domain, or (ii) as constraintsla CLP. Both the solvers are implemented on top of CLP(Bool), that typically have impressively ecient propagation en- gines.
---
paper_title: An Experimental CLP Platform for Integrity Constraints and Abduction

paper_content:

Integrity constraint and abduction are important in query-answering systems for enhanced query processing and for expressing knowledge in databases. A straightforward characterization of the two is given in a subset of the language CHRv, originally intended for writing constraint solvers to be applied for CLP languages. This subset has a strikingly simple computational model that can be executed using existing, Prolog-based technology. Together with earlier results, this confirms CHRv as a multiparadigm platform for experimenting with combinations of top-down and bottom-up evaluation, disjunctive databases and, as shown here, integrity constraint and abduction
---
paper_title: HYPROLOG: A New Logic Programming Language with Assumptions and Abduction

paper_content:

We present HYPROLOG, a novel integration of Prolog with assumptions and abduction which is implemented in and partly borrows syntax from Constraint Handling Rules (CHR) for integrity constraints. Assumptions are a mechanism inspired by linear logic and taken over from Assumption Grammars. The language shows a novel flexibility in the interaction between the different paradigms, including all additional built-in predicates and constraints solvers that may be available. Assumptions and abduction are especially useful for language processing, and we can show how HYPROLOG works seamlessly together with the grammar notation provided by the underlying Prolog system. An operational semantics is given which complies with standard declarative semantics for the “pure” sublanguages, while for the full HYPROLOG language, it must be taken as definition. The implementation is straightforward and seems to provide for abduction, the most efficient of known implementations; the price, however, is a limited use of negations. The main difference wrt. previous implementations of abduction is that we avoid any level of metainterpretation by having Prolog execute the deductive steps directly and by treating abducibles (and assumptions as well) as CHR constraints.
---
paper_title: Balanced parentheses in NL texts : a useful cue in the syntax/semantics interface

paper_content:

Balanced parentheses on text sentences can be obtained from information on particular morphemes -- the introducers -- and on inflected verbal forms. From balanced parentheses, a partial graph of the sentence in the semantics interface can be deduced, along with other information. The hypothesis and its expression with CHR constraints are presented.
---
paper_title: Coordination Revisited – A Constraint Handling Rule Approach

paper_content:

Coordination in natural language (as in “Tom and Jerry”, “John built but Mary painted the cupboard”, “publish or perish”) is one of the most difficult computational linguistic problems. Not only can it affect any type of constituent, but it often involves “guessing” material left implicit. We introduce a CHR methodology for extending a user’s grammar not including coordination with a metagrammatical treatment of same category coordination. Our methodology relies on the input grammar describing its semantics compositionally. It involves reifying grammar symbols into arguments of a generic symbol constituent, and adding three more rules to the user’s grammar. These three rules can coordinate practically any kind of constituent while reconstructing any missing material at the appropriate point. With respect to previous work, this is powerfully laconic as well as surprisingly minimal in the transformations and overhead required.
---
paper_title: Semantic Property Grammars for Knowledge Extraction from Biomedical Text

paper_content:

We present Semantic Property Grammars, designed to extract concepts and relations from biomedical texts. The implementation adapts a CHRG parser we designed for Property Grammars [1], which views linguistic constraints as properties between sets of categories and solves them by constraint satisfaction, can handle incomplete or erroneous text, and extract phrases of interest selectively. We endow it with concept and relation extraction abilities as well.
---
paper_title: Meaning in Context

paper_content:

A model for context-dependent natural language semantics is proposed and formalized in terms of possible worlds. The meaning of a sentence depends on context and at the same time affects that context representing the knowledge about the world collected from a discourse. The model fits well with a “flat” semantic representation as first proposed by Hobbs (1985), consisting basically of a conjunction of atomic predications in which all variables are existentially quantified with the widest possible scope; in our framework, this provides very concise semantic terms as compared with other representations. There is a natural correspondence between the possible worlds semantics and a constraint solver, and it is shown how such a semantics can be defined using the programming language of Constraint Handling Rules (Fruhwirth, 1995). Discourse analysis is clearly a process of abduction in this framework, and it is shown that the mentioned constraint solvers serve as effective and efficient abductive engines for the purpose.
---
paper_title: Chart Parsing And Constraint Programming

paper_content:

In this paper, parsing-as-deduction and constraint programming are brought together to outline a procedure for the specification of constraint-based chart parsers. Following the proposal in Shieber et al. (1995), we show how to directly realize the inference rules for deductive parsers as Constraint Handling Rules (Fruhwirth, 1998) by viewing the items of a chart parser as constraints and the constraint base as a chart. This allows the direct use of constraint resolution to parse sentences.
---
paper_title: A constraint parser for contextual rules

paper_content:

In this paper we describe a constraint analyser for contextual rules. Contextual rules constitute a rule-based formalism that allows rewriting of terminals and/or non terminal sequences taking in account their context. The formalism allows also to refer to portions of text by means of exclusion zones, that is, patterns that are only specified by a maximum length and a set of not allowed categories. The constraint approach reveals particularly useful for this type of rules, as decisions can be taken under the hypothesis of non existence of the excluded categories. If these categories are finally deduced, all other categories inferred upon the non existence of the former ones are automatically eliminated. The parser has been implemented using Constraint, Handling Rules. Some results with a set of rules oriented to the segmentation of texts in propositions are shown.
---
paper_title: CHR: A Flexible Query Language

paper_content:

We show how the language Constraint Handling Rules (CHR), a high-level logic language for the implementation of constraint solvers, can be slightly extended to become a general-purpose logic programming language with an expressive power subsuming the expressive ower of Horn clause programs with SLD resolution. The extended language, called “CHR∀”, retains however the extra features of CHR, e.g., committed choice and matching, which axe important for other purposes, especially for efficiently solving constraints. CHR∀ turns out to be a very flexible query language in the sense that it supports several (constraint) logic programming paradigms and allows to mix them in a single program. In particular, it supports top-down query evaluation and also bottom-up evaluation as it is frequently used in (disjunctive) deductive databases.
---
paper_title: Constraint Based Methods for Biological Sequence Analysis

paper_content:

The need for processing biological information is rapidly growing, owing to the masses of new information in digital form being produced at this time. Old method- ologies for processing it can no longer keep up with this rate of growth. The methods of Artificial Intelligence (AI) in general and of language processing in particular can offer much towards solving this problem. However, interdisciplinary research between language processing and molecular biology is not yet widespread, partly because of the effort needed for each specialist to understand the other one's jargon. We argue that by looking at the problems of molecular biology from a language processing perspec- tive, and using constraint based logic methodologies we can shorten the gap and make interdisciplinary collaborations more effective. We shall discuss several sequence anal- ysis problems in terms of constraint based formalisms such Concept Formation Rules, Constraint Handling Rules (CHR) and their grammatical counterpart, CHRG. We pos- tulate that genetic structure analysis can also benefit from these methods, for instance to reconstruct from a given RNA secondary structure, a nucleotide sequence that folds into it. Our proposed methodologies lend direct executability to high level descriptions of the problems at hand and thus contribute to rapid while efficient prototyping.
---
paper_title: An abductive treatment of long distance dependencies in CHR

paper_content:

We propose a CHR treatment for long distance dependencies which abduces the missing elements while relating the constituents that must be related. We discuss our ideas both from a classical analysis point of view, and from a property-grammar based perspective. We exemplify them through relative clauses first, and next through the more challenging case of natural language coordination. We present an abductive rule schema for conjunction from which appropriate rule instances materialize through the normal process of unification in a given sentence's parse, and which fills in (abduces) any information that may be missing in one conjunct through semantic and syntactic information found in the other. Thus semantic criteria, which in most previous approaches was understressed in favour of syntactic criteria, regains its due importance, within our encompassing while retaining economic abductive formulation.
---
paper_title: Extracting Selected Phrases through Constraint Satisfaction

paper_content:

We present in this paper a CHR based parsing methodology for parsing Property Grammars. This approach constitutes a flexible parsing technology in which the notions of derivation and hierarchy give way to the more flexible notion of constraint satisfaction between categories. It becomes then possible to describe the syntactic characteristics of a category in terms of satisfied and violated constraints.Different applications can take advantage of such flexibility, in particular in the case where information comes from part of the input and requires the identification of selected phrases such as NP, PP, etc. Our method presents two main advantages: first, there is no need to build an entire syntactic structure, only the selected phrases can be extracted. Moreover, such extraction can be done even from incomplete or erroneous text: indication of possible kinds of error or incompleteness can be given together with the proposed analysis for the phrases being sought.
---
paper_title: Logic Grammars for Diagnosis and Repair

paper_content:

We propose an abductive model based on Constraint Handling Rule Grammars (CHRGs) for detecting and correcting errors in problem domains that can be described in terms of strings of words accepted by a logic grammar. We provide a proof of concept for the specific problem of detecting and repairing natural language errors, in particular, those concerning feature agreement. Our methodology relies on grammar and string transformation in accordance with a user-defined dictionary of possible repairs. This transformation also serves as top-down guidance for our essentially bottom-up parser. With respect to previous approaches to error detection and repair, including those that also use constraints and/or abduction, our methodology is surprisingly simple while far-reaching and efficient.
---
paper_title: JmmSolve: A Generative Java Memory Model Implemented in Prolog and CHR

paper_content:

The memory model of a programming language specifies the interaction between multiple threads and main memory. Basically, the model says for every value obtained by a read operation in a program by what write operation it has been produced. In a multi-threaded unsynchronized program this need not be a deterministic linking from reads to writes. For a multi-platform language such as Java, a memory model is essential to guarantee portability of programs.
---
paper_title: Model-based testing for real

paper_content:

Model-based testing relies on abstract behavior models for test case generation. These models are abstractions, i.e., simplifications. For deterministic reactive systems, test cases are sequences of input and expected output. To bridge the different levels of abstraction, input must be concretized before being applied to the system under test. The system’s output must then be abstracted before being compared to the output of the model.The concepts are discussed along the lines of a feasibility study, an inhouse smart card case study. We describe the modeling concepts of the CASE tool AutoFocus and an approach to model-based test case generation that is based on symbolic execution with Constraint Logic Programming.Different search strategies and algorithms for test case generation are discussed. Besides validating the model itself, generated test cases were used to verify the actual hardware with respect to these traces.
---
paper_title: Using CHRs to generate functional test cases for the Java Card Virtual Machine

paper_content:

Automated functional testing consists in deriving test cases from the specification model of a program to detect faults within an implementation. In our work, we investigate using Constraint Handling Rules (CHRs) to automate the test cases generation process of functional testing. Our case study is a formal model of the Java Card Virtual Machine (JCVM) written in a sub-language of the Coq proof assistant. In this paper we define an automated translation from this formal model into CHRs and propose to generate test cases for each bytecode definition of the JCVM. The originality of our approach resides in the use of CHRs to faithfully model the formally specified operational semantics of the JCVM. The approach has been implemented in Eclipse Prolog and a full set of test cases have been generated for testing the JCVM.
---
paper_title: Security Policy Consistency

paper_content:

With the advent of wide security platforms able to express simultaneously all the policies comprising an organization's global security policy, the problem of inconsistencies within security policies become harder and more relevant. ::: We have defined a tool based on the CHR language which is able to detect several types of inconsistencies within and between security policies and other specifications, namely workflow specifications. ::: Although the problem of security conflicts has been addressed by several authors, to our knowledge none has addressed the general problem of security inconsistencies, on its several definitions and target specifications.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: Proving termination of CHR in Prolog : A transformational approach

paper_content:

Constraint Handling Rules (CHR) is a concurrent, comitted-choice, logic programming language. It is constraint-based and has guarded rules that rewrite multisets of atomic formulas [1]. Its simple syntax and semantics make it wellsuited for implementing custom constraint solvers. Despite the amount of work directed to CHR, not much has been done on termination analysis. To the best of our knowledge, there were no attempts made to automate termination proofs. The first and, until now, only contribution to termination analysis of CHR is reported in [2] and shows termination of CHR programs under the theoretical semantics [1] of CHR. Termination is shown, using a ranking function, mapping sets of constraints to a well-founded order. A ranking condition, on the level of the rules, implies termination. Although termination conditions in CHR take a different form than in Logic Programs (LP) and Term-Rewrite Systems (TRS), [2] shows that achievements from the work on termination of LP and TRS are relevant and adaptable to the CHR context. In this paper, we present a termination preserving transformation of CHR to Prolog. This allows the direct reuse of termination proof methods from LP and TRS for CHR, yielding the first fully automatic termination proving for CHR. We implemented the transformation and used existing termination tools for LP and TRS on a set of CHR programs to demonstrate the usefulness of our approach. In [3], we formalize the transformation and prove soundness w.r.t. termination.
---
paper_title: Adaptive Constraint Handling with CHR in Java

paper_content:

The most advanced implementation of adaptive constraint processing with Constraint Handling Rules (CHR) is introduced in the imperative object-oriented programming language Java. The presented Java implementation consists of a compiler and a run-time system, all implemented in Java. The run-time system implements data structures like sparse bit vectors, logical variables and terms as well as an adaptive unification and an adaptive entailment algorithm. Approved technologies like attributed variables for constraint storage and retrieval as well as code generation for each head constraint are used. Also implemented are theoretically sound algorithms for adapting of rule derivations and constraint stores after arbitrary constraint deletions. The presentation is rounded off with some novel applications of CHR in constraint processing: simulated annealing for the n queens problem and intelligent backtracking for some SAT benchmark problems.
---
paper_title: Unfolding in CHR

paper_content:

Program transformation is an appealing technique which allows to improve run-time efficiency, space-consumption and more generally to optimize a given program. Essentially it consists of a sequence of syntactic program manipulations which preserves some kind of semantic equivalence. One of the basic operations which is used by most program transformation systems is unfolding which consists in the replacement of a procedure call by its definition. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages and, to the best of our knowledge, no one has considered unfolding of CHR programs. This paper is a first attempt to define a correct unfolding system for CHR programs. We define an unfolding rule, show its correctness and discuss some conditions which can be used to delete an unfolded rule while preserving the program meaning.
---
paper_title: Abstract interpretation for constraint handling rules

paper_content:

Program analysis is essential for the optimized compilation of Constraint Handling Rules (CHRs) as well as the inference of behavioral properties such as confluence and termination. Up to now all program analyses for CHRs have been developed in an ad hoc fashion.In this work we bring the general program analysis methodology of abstract interpretation to CHRs: we formulate an abstract interpretation framework over the call-based operational semantics of CHRs. The abstract interpretation framework is non-obvious since it needs to handle the highly non-deterministic execution of CHRs. The use of the framework is illustrated with two instantiations: the CHR-specific late storage analysis and the more generally known groundness analysis. In addition, we discuss optimizations based on these analyses and present experimental results.
---
paper_title: On Incremental Adaptation of CHR Derivations

paper_content:

Constraint-solving in dynamic environments requires the immediate adaptation of solutions of constraint satisfaction problems if these problems are changing. After any change, an adapted solution is preferred which is stable, i.e., as close as possible to the original solution. A wide range of incremental constraint-solving methods for dynamic, especially finite-domain, constraint satisfaction problems (DCSPs) are known, which more or less satisfy this additional requirement. Adaptation of DCSPs after constraint additions is generally simple and successfully solved, but adaptation after arbitrary constraint deletions is not. How constraint handling rules (CHRs), a high level language extension for implementing constraint solvers, can be improved in this respect is investigated. A new incremental algorithm is presented, which adapts an arbitrary CHR derivation after eliminations of constraints in the processed DCSPs. Thus, the existing solvers - there are several dozens of them - for various kinds of const...
---
paper_title: Extending arbitrary solvers with constraint handling rules

paper_content:

Constraint Handling Rules (CHRs) are a high-level committed choice programming language commonly used to write constraint solvers. While the semantic basis of CHRs allows them to extend arbitrary underlying constraint solvers, in practice, all current implementations only extend Herbrand equation solvers. In this paper we show how to define CHR programs that extend arbitrary solvers and fully interact with them. In the process, we examine how to compile such programs to perform as little recomputation as possible, and describe how to build index structures for CHR constraints that are modified automatically when variables in the underlying solver change. We report on the implementation of these techniques in the HAL compiler, and give empirical results illustrating their benefits.
---
paper_title: Integration and Optimization of Rule-based Constraint Solvers

paper_content:

One lesson learned from practical constraint solving applications is that constraints are often heterogeneous. Solving such constraints requires a collaboration of constraint solvers. In this paper, we introduce a methodology for the tight integration of CHR constraint programs into one such program. CHR is a high-level rule-based language for writing constraint solvers and reasoning systems. A constraint solver is well-behaved if it is terminating and confluent. When merging constraint solvers, this property may be lost. Based on previous results on CHR program analysis and transformation we show how to utilize completion to regain well-behavedness. We identify a class of solvers whose union is always confluent and we show that for preserving termination such a class is hard to find. The merged and completed constraint solvers may contain redundant rules. Utilizing the notion of operational equivalence, which is decidable for well-behaved CHR programs, we present a method to detect redundant rules in a CHR program.
---
paper_title: Theory and Practice of Constraint Handling Rules

paper_content:

Abstract Constraint Handling Rules (CHR) are our proposal to allow more flexibility and application-oriented customization of constraint systems. CHR are a declarative language extension especially designed for writing user-defined constraints. CHR are essentially a committed-choice language consisting of multi-headed guarded rules that rewrite constraints into simpler ones until they are solved. In this broad survey we aim at covering all aspects of CHR as they currently present themselves. Going from theory to practice, we will define syntax and semantics for CHR, introduce an important decidable property, confluence, of CHR programs and define a tight integration of CHR with constraint logic programming languages. This survey then describes implementations of the language before we review several constraint solvers – both traditional and nonstandard ones – written in the CHR language. Finally we introduce two innovative applications that benefited from using CHR.
---
paper_title: A new approach to termination analysis of Constraint Handling Rules

paper_content:

Constraint Handling Rules (CHR) is a concurrent, committed-choice constraint programming language (see [2]). It is a rule-based language, in which multisets of atomic constraints are rewritten using guarded rules. It has a simple syntax and declarative semantics, and is very suitable for implementing constraint solvers. Although the language is strongly related to Logic Programming (LP) and to lesser extent also to Term-Rewrite Systems (TRS), termination analysis of CHR has received little attention. To the best of our knowledge, the only contribution so far is reported in [3]. This study is limited to CHR programs with only one type of rules: the so called ’simplification rules’. The work shows that, for this class of programs, termination analysis techniques developed for LP (see [1]) can be adapted to CHR. In this paper, we present a new approach to termination analysis of CHR which is applicable to a much larger class of CHR programs. We propose a new termination condition and show its applicability to CHR programs with rules that are not only of the simplification type. We have successfully tested the condition on a benchmark of programs, using a prototype analyser.
---
paper_title: Specialization of Concurrent Guarded Multi-Set Transformation Rules

paper_content:

Program transformation and in particular partial evaluation are appealing techniques for declarative programs to improve not only their performance. This paper presents the first step towards developing program transformation techniques for a concurrent constraint programming language where guarded rules rewrite and augment multi-sets of atomic formulae, called Constraint Handling Rules (CHR). ::: ::: We study the specialization of rules with regard to a given goal (query). We show the correctness of this program transformation: Adding and removing specialized rules in a program does not change the program's operational semantics. Furthermore termination and confluence of the program are shown to be preserved.
---
paper_title: A compositional semantics for CHR

paper_content:

Constraint Handling Rules (CHR) are a committed-choice declarative language which has been designed for writing constraint solvers. A CHR program consists of multi-headed guarded rules which allow one to rewrite constraints into simpler ones until a solved form is reached.CHR has received a considerable attention, both from the practical and from the theoretical side. Nevertheless, due the use of multi-headed clauses, there are several aspects of the CHR semantics which have not been clarified yet. In particular, no compositional semantics for CHR has been defined so far.In this paper we introduce a fix-point semantics which characterizes the input/output behavior of a CHR program and which is and-compositional, that is, which allows to retrieve the semantics of a conjunctive query from the semantics of its components. Such a semantics can be used as a basis to define incremental and modular analysis and verification tools.
---
paper_title: Observable confluence for constraint handling rules

paper_content:

Constraint Handling Rules (CHR) are a powerful rule based language for specifying constraint solvers. Critical for any rule based language is the notion of confluence, and for terminating CHR programs there is a decidable test for confluence. But many CHR programs that are in practice confluent fail this confluence test. The problem is that the states that illustrate non-confluence are not observable from the initial goals of interest. In this paper we introduce the notion of observable confluence, a more general notion of confluence which takes into account whether states are observable. We devise a test for observable confluence which allows us to verify observable confluence for a range of CHR programs dealing with agents, type systems, and the union-find algorithm.
---

Title: As time goes by: Constraint Handling Rules - A survey of CHR research from 1998 to 2007

Section 1: Introduction
Description 1: Provide an introduction to the survey, detailing the foundation and evolution of Constraint Handling Rules (CHR) over the specified period.

Section 2: Historical Overview
Description 2: Outline the development and important milestones of CHR research from its early stages to 2007.

Section 3: Constraint Handling Rules
Description 3: Introduce the syntax and informal semantics of CHR to make the survey self-contained for readers who may not be familiar with CHR.

Section 4: Semantics
Description 4: Discuss both the logical (declarative) semantics and the operational semantics of CHR, including classical, linear, and transaction logic semantics.

Section 5: Program Analysis
Description 5: Explore the important properties and analyses of CHR programs such as confluence, termination, and complexity.

Section 6: Systems and Implementation
Description 6: Provide an overview of the numerous CHR systems, their implementation, and the compilation techniques, including important optimizations to enhance performance.

Section 7: Extensions and Variants
Description 7: Discuss various extensions and variants of CHR that address identified weaknesses and limitations, including probabilistic CHR, adaptive CHR, and CHR with disjunctions.

Section 8: Relation to Other Formalisms
Description 8: Draw connections between CHR and other formalisms, comparing capabilities and commonalities with different logic and term rewriting systems, production rules, and graph-based formalisms.

Section 9: Applications
Description 9: Review significant applications of CHR across various domains such as constraint solvers, spatio-temporal reasoning, multi-agent systems, and programming language development.

Section 10: Conclusions
Description 10: Summarize the survey findings, assess the coverage of CHR research, reflect on past research topics from earlier surveys, and identify grand challenges for future CHR research.