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.
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.
Termination of CHR
FWO, 1/1/2008 to 1/1/2012.
K.U. Leuven (Tom Schrijvers, Paolo Pilozzi, Danny De Schreye, Dean Voets).
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.
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.
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.