Constraint Handling Rules (CHR) is a simple, but elegant declarative rule-based programming language. It combines elements of Constraint Programming and Rewrite Systems. Typical applications are constraint solving, natural language processing, type checking, and reasoning capabilities for multi-agent systems. Various implementations of CHR exist for Prolog, Java and other languages.
In recent years, the Declarative Languages and Artificial Intelligence group (DTAI) of the K.U.Leuven has been actively contributing to the research on the Constraint Handling Rules language. This research has been conducted in cooperation with the research group of the University of Ulm headed by Thom Frühwirth, the creator of the CHR language.
A seminar day is organized to bring together these two active groups in the field of CHR, and to present, under the auspices of the WOG research network on Declarative Methods in Computer Science, to all interested parties the latest developments of the CHR language and future research topics.
Program14:00: Using CHR to extend the union-find algorithm,
Thom Fruehwirth, University of Ulm
14:30: Overview of the K.U.Leuven CHR Research,
Tom Schrijvers, K.U.Leuven
15:00 Coffee break
15:30: Transaction Logic Semantics for CHR,
Marc Meister, University of Ulm
16:00: Memory reuse for CHR,
Jon Sneyers, K.U.Leuven
Celestijnenlaan 200, building S, room 00.03, 3001 Heverlee (Leuven), Belgium
This building is on the same campus site as the department of computer science.Participation is free and open. Registration is not required, but appreciated.
Contact: Tom Schrijvers
Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium
tel: +32 16 327544
e-mail: tom.schrijvers@cs.kuleuven.be
Using CHR to extend the union-find algorithm, Thom Fruehwirth, University of Ulm
Abstract:
After a gentle introduction to the rule-based constraint programming
language CHR (constraint handling rules) we show the compact and
efficient implementation of Tarjan's classical almost linear-time
union-find algorithm in CHR of Tom Schrijvers and myself.
The union-find algorithm can be seen as solving simple equalities
between pairs of variables or constants. In our ongoing work we extend
the implementation so that other types of simple (in)equations in two
variables can be efficiently solved. With a few lines of code, we
rediscover (variations of) fast algorithms for solving certain
propostional logic (SAT) problems as well as certain polynomial
inequations. We would like to extend our work to other types of
problems.
An Overview of the K.U.Leuven CHR Research, Tom Schrijvers, K.U.Leuven
Abstract:
In this presentation we provide an overview of the past, present and
future work of the K.U.Leuven CHR team on Constraint Handling Rules.
Our work is driven by the development of the K.U.Leuven CHR system,
currently available for Prolog (7 systems) and Java and with quite a
number of academic and industrial users. We focus in particular on
language features & integration, program analysis &
verification, and optimized compilation.
In the past we have already achieved a number of important
contributions in each of these domains, e.g. the integration of CHR
with tabled execution, an abstract interpretation framework for CHR,
and equivalent time and space complexity of our CHR system and RAM
machines. Many general and important challenges still lie ahead of us
in the future. We give an overview of issues concerning the subsumption
of other rule-based languages (production rule systems, TRS), feasible
yet accurate program analysis and closing the performance gap with
hand-optimized constraint propagators.
A Transaction Logic Semantics for CHR, Marc Meister, University of Ulm
Abstract:
When using Constraint Handling Rules (CHR) as a general purpose
programming language, we often exploit its refined semantics. Programs
for refined semantics, which rely on the order rules are tried, often
have no classical declarative semantics and reasoning over such
programs is awkward. Proving that, e.g., an invariant holds during a
CHR computation for such a program is often done in an ad-hoc manner.
Transaction logic (TR) is an extension of first-order logic (FOL)
capable of modelling updates in logic programs. An executable
Horn-fragment of TR
allows to program in TR and we can reason over such TR-programs in TR
as we reason over (pure) Prolog programs in FOL.
We propose to use TR as a specification, execution, and verification
language for CHR by transforming the CHR program and the CHR run-time
system into TR. To this end, we formalise the state transition system
of CHR as Horn-TR-program and link the application of CHR rules with
establishing the truth of TR-predicates: The TR-model theory of the
transformed program gives the new declarative TR semantics for CHR.
Executional entailment integrates CHR's operational semantics into a
formal logic and TR's sound and complete inference engine actually runs
the program. Using (full) TR we can reason over the transformed
program, e.g, prove that an invariant holds during a CHR computation
inside the formal TR system.
Memory reuse for CHR, Jon Sneyers, K.U.Leuven
Abstract: This is a presentation on recent work on the K.U.Leuven CHR (Constraint Handling Rules) implementation. We introduce two compiler optimizations that drastically reduce the memory footprint of CHR programs. The core idea is to reuse the internal CHR constraint representation, and avoid the overhead of constraint removal followed by insertion. Both optimizations were implemented in the K.U.Leuven CHR system. They result in significant memory savings and speedups.
My work consists in investigating the possible sinergies of recent techniques in software enginneering with emphasys in reuse (i.e. MDA, AOD and Components) for building a very abstract/executable engine for CHR with disjunction possibily extended with justification mechanisms proposed by Armin Wolf in his Doctor´s thesis. The codename for the engine is CHREK (short for CHRv engine using the KobrA method). CHREK is the starting step towards the ORCAS project (Ontology-driven Reasoning Components for Agent-based Simulations), a reusable automated reasoning component framework. ORCAS aims at integrating most services for automated reasoning in reusable stand-alone components based on a CHRv engine.
Interests: software reuse, components, automated reasoning, constraint solving, constraint handling rules
My short talk is about implementing a powerful but concise F-logic handler for CHR. We give an overview of F-logic, a rule-based object-oriented formalism that supports non-monotonic inheritance. The implementation creates a model by repeatedly applying F-rules and inheritance on the F-facts and provides answers for F-queries. As the current implementation based on Kifer's original work leads to several anomalies when inheritance and inference by rules interact, we plan to improve the handler based on Yang's rectification with three-valued semantics.
Interests: object-orientation, standard semantics, modularisation, automatic proving
Declarative semantics presents a powerful tool for the analysis and verification of CHR programs, a property inherited from its logical and constraint-logical predecessors. My talk is about the linear logic semantics for CHRv, i.e. CHRs with disjunction. At first, a short introduction to linear logic will be given and the already established linear logic semantics for classic CHR will be presented. Subsequently, we will discuss my approach how to extend this result to CHRv.
Interests: CHR with disjunction; probabilistic CHR and their mathematical analysis; CHR for embedded systems.