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.

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