Automatic Support for Proving Confluence Modulo Equivalence for Constraint Handling Rules

External project partner of Prof. Henning Christiansen, Roskilde University, Denmark, 2015-2018.

This project will develop foundations and methods for automatic and semi-automatic proofs of a program property called Confluence Modulo Equivalence (CME) for CHR, that generalizes the classical confluence notion (CC) studied so far for CHR. A program being confluent means that the final result, i.e., the final constraint store, for a query is independent of the order in which the program rules are applied. CME involves an equivalence relation specified by the programmer, so that alternative program traces do not need to lead to identical states (as for CC), but only to states equivalent modulo the equivalence relation. CME allows a much larger class of programs to be considered confluent, e.g., with redundant data representations (sets as lists or trees) and dynamic programming algorithms with pruning, that were not covered by earlier work.

more information

FormalCog: Formal Semantics and Analysis of Cognitive Architectures

The aim is to develop a formal basis for analysis of a cognitive modeling
architecture and its sound implementation as a proof-of-concept.

more information

Long-term Routing for Autonomous Robot Sailboats with Constraint Handling Rules

With Roland Stelzer, INNOC, Vienna, Austria and Jon Sneyers, K.U.Leuven, Belgium, 2009-2013.

Robotic sailing boats execute complex sailing processes completely autonomously and without human interaction. Starting with finding a route based on weather data, to the autonomous execution of manoeuvres, robotic boats are able to reach any desired destination. We developed a rule-based algorithm for long-term routing of robotic sailboats. It computes optimal routes based on wind conditions, ocean currents, and shorelines, while taking the boats individual characteristics into account.

more information

Termination of CHR

FWO, 1/1/2008 to 1/1/2012.
K.U. Leuven (Tom Schrijvers, Paolo Pilozzi, Danny De Schreye, Dean Voets).

more information

GLOB-CON - Rule-Based Propagation of Global Constraints

DFG Project FR 1390/1-1, March 2006-2008.
Project partner is Dr. Sebastian Brand, Melbourne University, Australia.

project description

Platform independent analysis and implementation of Constraint Handling Rules

FWO, 3E060075, 01-01-2007 to 31-12-2010.
K.U. Leuven (Bart Demoen, Maurice Bruynooghe, Gerda Janssens)
University of Melbourne (Peter Stuckey)

The project intends to study and develop new analysis and implementation techniques for the language CHR. The project will focus in particular on the design of an abstract machine for CHR, the optimizing compilation of CHR by means of abstract interpretation, the study of complexity (space and time) properties of CHR and the study of techniques for compile time memory reuse.

more information

ROARS: Reuse-Oriented Automated Reasoning Software

DAAD Probral and CAPES Project 415-br-probral/po/D05/30354, March 2006-2008.
Project partners are Prof. Dr. Jacques Robin, Universidade Federal do Pernambuco (CInUFPE), Recife, Brazil and Prof. Dr. Colin Atkinson, University of Mannheim, Germany and Dr. Armin Wolf, Fraunhofer FIRST, Berlin, Germany.

project description