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

Terminierung von CHR

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

Mehr Information

GLOB-CON: Regelbasierte Propagation von Globalen Constraints

DFG-Projekt FR 1390/1-1, März 2006-2008.
Projektpartner ist Dr. Sebastian Brand, Melbourne University, Australien.


Plattformunabhängige Analyse und Implementierung von Constraint Handling Rules

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

Ziel des Projekts ist die Untersuchung und Entwicklung von neuen Analyse- und Implementierungstechniken für die Sprache CHR. Der spezielle Fokus liegt auf dem Entwurf einer abstrakten Maschine für CHR, der optimierenden Übersetzung von CHR durch abstrakte Interpretation, der Untersuchung der (Zeit- und Platz-)Komplexität von CHR und der Untersuchung von Techniken für Speicherplatzwiederverwendung zur Übersetzungszeit.

Mehr Information

ROARS: Reuse-Oriented Automated Reasoning Software

DAAD Probral und CAPES Projekt 415-br-probral/po/D05/30354, März 2006-2008.
Projektpartner sind Prof. Dr. Jacques Robin, Universidade Federal do Pernambuco (CInUFPE), Recife, Brasilien und Prof. Dr. Colin Atkinson, Universität Mannheim und Dr. Armin Wolf, Fraunhofer FIRST, Berlin.