Recent Research Activities of Thom Frühwirth

Only a few examplary research papers are shown. Rechent Bachelor theses are not included. See Thom Fruehwirth's list of publications for a complete list of research. Links to theses and papers on this page may contain preliminary versions.
See also about the programming language CHR.

Research Topics, Applications and Supervised Theses since 2012

CHR - The Constraint Handling Rules Language

Constraint Handling Rules (CHR) is a concurrent committed-choice constraint logic programming language consisting of guarded rules that transform multi-sets of atomic formulas (constraints) until exhaustion. It was designed by Thom Fruehwirth in 1991. CHR can embed many rule-based formalisms and systems, and it can describe algorithms in a compact declarative way without compromising efficiency. The clean semantics of CHR ensures that several desirable properties hold for CHR programs and also facilitates sophisticated program analysis. CHR libraries exist for Prolog, Haskell, Java, Javascript, Python and C. CHR is also available online for experimentation with many example programs. More than 250 academic and industrial projects worldwide use CHR, and about 2500 research papers reference it.

Constraint Handling Rules - What Else?, Thom Frühwirth, Invited Survey Paper, RuleML 2015. Slides of associated Keynote Talk.

Online Interactive Constraint Handling Rules Demo Tool and JavaScript JIT CHR Compiler, Master Thesis Falco Nogatz, 2015.

CHR Book Home Page with many links.


Constraint Handling Rules - Compilation, Execution, and Analysis. Thom Frühwirth and Frank Raiser (editors). ISBN 9783746069050, BOD, 2018.

Parallelism, Concurrency and Distribution in Constraint Handling Rules: A Survey, Thom Fruehwirth, TPLP Journal, 2018.

Implementing parallel CHR on special hardware: On FPGA, PhD. Andrea Triossi, CERN, 2012; On GPU Nvidia, Amira Zaki, Ilvar Geller, 2012.

Constraint Reasoning: CDF-intervals: a probabilistic interval constraint framework to reason about data with uncertainty, PhD. Aya Saad, 2016.

Program Analysis and Verification
A Unified Analytical Foundation for Constraint Handling Rules, PhD. Hariolf Betz, BOD, ISBN 9783734732508, 2014.

A Devil's Advocate against Termination of Direct Recursion, Thom Frühwirth, PPDP 2015.

Why Can't You Behave? Non-Termination Analysis of Direct Recursive Rules with Constraints (Full Version), Thom Frühwirth, RuleML 2016.

Confluence Modulo Equivalence with Invariants in Constraint Handling Rules, Daniel Gall, FLOPS 2018.

Analysis of Cognitive Models in Constraint Handling Rules, PhD. thesis, Daniel Gall, Ulm University, 2021.

Programm Transformation
Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms, Thom Fruehwirth, LNCS 10855, 2018.
Combining Forward and Backward Propagation, Amira Zaki,2015.
Source-to-source transformation for rule-based approaches and extensions in CHR (book slides), Thom Fruehwirth, 2013.

Programming Environment
A Confluence Checker for Constraint Handling Rules with Persistent Constraints, INAP 2017, Master Thesis Frank Richter, 2017.
Online Interactive Constraint Handling Rules Demo Tool and JavaScript JIT CHR Compiler, CHR.js: A CHR Implementation in JavaScript, Falco Nogatz, RuleML+RR 2018.
Extension of the Confluence Checker for CHR Programs, B.Sc. Daniel Bebber, 2015.
A Confluence and Operational Equivalence Checker for CHR Programs, (tool download), B.Sc. Frank Richter, 2014.
Eclipse Plugin for CHR, (tool download link), B.Sc. Matthias Rau, 2013.


See also research projects below.

Translator from XML Schema to JSON Schema
From XML Schema to JSON Schema - Comparison and Translation with Constraint Handling Rules, (tool download link), B.Sc. Falco Nogatz, Uni Ulm, 2014.

Algorithm Visualisation
CHRvis: an animation extension for animating constraint handling rules, PhD. Nada Sharaf, GUC and Uni Ulm, 2019.
Visualization of Grid-based and Fundamental CHR Algorithms, B.Sc. thesis Arwa Ismail GUC, 2012.
Animation of Mathematical and Graph-based Algorithms expressed in CHR, B.Sc. thesis Mostafa Ali Said GUC, 2012.

More Applications
Security Policies in Constraint Handling Rules, Thom Fruehwirth, LPOP 2018.
Automatic Poetry Generation Using CHR, Master Thesis, Alia El Bolock, GUC, 2014.
Probabilistic Legal Reasoning in CHRiSM, TPLP Journal, Jon Sneyers, K.U. Leuven, 2013.
CHR Solver for Binomial Bivariate Polynomial Equation Systems, B.Sc. Alia El Bolock, GUC, 2012.
A Clustering-based Approach to Summarizing Google Search Results using CHR, B.Sc. thesis Sharif Ayman, GUC, 2012.
CHR-based Text Mining and Classification of Google Search Results, B.Sc. thesis Aly Saleh, GUC, 2012.
Longterm Routing for autonomous sailboats, Johannes Langbein Uni Ulm, Roland Stelzer INNOC Vienna, Jon Sneyers, K.U. Leuven, 2011.

Video of talk on CHR applications (German with English slides):
Computer knacken harte Nüsse - Von Sudoku über den Aktienhandel zum Robotersegeln,
also at TIB, Thom Frühwirth, 2013.

Online Tools and Demos
- chrjs: Online Interactive Constraint Handling Rules (CHR) Demo Tool and JavaScript JIT CHR Compiler
- Online Interactive Constraint Handling Rules Prolog Programming Demo Tool (replacing WebCHR)
- Constraint Handling Rules (CHR) bibliography and blog

Research Projects, Funding, Grants of Thom Frühwirth since 1984

See also our current projects. See also the list of publications for material related to the projects.

Super-Linear Speedup by Program Transformation

Thom Fruehwirth, since 2019.
We investigate the use of repeated unfolding and simplification to achieve super-linear speedup in sequential programs. Our technique of repeated recursion unfolding repeatedly unfolds a recursion with itself and simplifies it while keeping all unfolded rules. Each unfolding doubles the number of recursive steps covered. This reduces the number of recursive steps to its logarithm at the expense of introducing a logarithmic number of unfolded recursive cases to the program. Our optimization can lower the time complexity class of a program if enough simplification in the recursions is possible. The actual runtime improvement quickly reaches several orders of magnitude.

Repeated Recursion Unfolding for Super-Linear Speedup within Bounds, LOPSTR 2020.

Mason's Mark Database and Design with the Graph Tool VanDeGraphGenerator

Thom Fruehwirth, 2018-2021.
We are developing a rule-based implementation of a tool to analyse and generate graphs. It is used in the domain of mason's marks. For thousands of years, stonemasons have been inscribing these symbolic signs on dressed stone. Geometrically, mason's marks are line drawings. They consist of a pattern of straight lines, sometimes circles and arcs. We represent mason's marks by connected planar graphs. Our tool for analysis and generation of graphs is written in the rule-based declarative language Constraint Handling Rules. We also apply the tool to generate Digital Art.

The Computer Art of Mason's Mark Design with VanDeGraphGenerator, Thom Fruehwirth, ISBN 9783752842975, BOD, 2018.
Rule-Based Drawing, Analysis and Generation of Graphs for Mason's Mark Designs, Thom Fruehwirth, RuleML+RR 2018.
Digital Artificial Intelligence Abstract Art, 2019.
Official contribution to the German Science Year 2019 on Artificial Intelligence of the Federal Ministry of Education and Research.

Automatic Support for Proving Confluence Modulo Equivalence for Constraint Handling Rules

External project partner of Prof. Henning Christiansen, Roskilde University, Denmark, 2015-2019.
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.

FormalCog: Formal Semantics and Analysis of Cognitive Architectures

With Daniel Gall, Ulm University, 2013-2020.
The aim of this project is to develop a formal basis for analysis of a cognitive modeling architecture and its sound implementation as a proof-of-concept. Computational cognitive modeling explores human cognition by building models that are executable by computers. Such computational models can serve as process-based theories that support classic behavioral studies to better understand human cognition. Currently, computational cognitive modeling architectures as well as the implementations of cognitive models are typically ad-hoc constructs. They lack a formalization from the computer science point of view. This impedes analysis of the underlying languages and the programmed models. It makes it hard to compare different implementation variants of the languages. It makes it hard to verify properties of the models. These issues call for a formal semantics of cognitive modeling languages together with proper analysis techniques. The main objective of this project is to connect the psychological methods from computational cognitive modeling with results from computer science to eliminate ad-hoc cognitive modeling. We will develop a formal operational semantics for a popular cognitive modeling language and build an analysis framework upon it. In short, the possibility of analyzing models on a sound semantical basis will enable the formally founded validation of cognitive models. Last but not least, our endeavor will foster the interplay between Computational Psychology and Computer Science.
Analysis of Cognitive Models in Constraint Handling Rules, PhD. thesis, Daniel Gall, Ulm University, 2021.
An Operational Semantics for the Cognitive Architecture ACT-R and its Translation to Constraint Handling Rules, Daniel Gall, ACM TOCL Journal, 2018.
A Decidable Confluence Test for Cognitive Models in ACT-R, Daniel Gall, LNCS 10364, 2017.
ACT-R cognitive modeling language in CHR, M.Sc. thesis, Daniel Gall, 2013.

Longterm Routing for Autonomous Robot Sailboats with Constraint Handling Rules

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

Click on image downloads paper.
Events like the devastating tsunamis in Asia, the Deep-water Horizon oil spill in Gulf of Mexico, accidents involving refugee boats in the Mediterranean Sea and pirate activities in the Gulf of Aden have impressively emphasized the importance of a fully integrated ocean observation system. Robotic sailing boats offer the possibility of sampling an area of interest with high temporal and spatial resolution at low cost. The ASV Roboat from INNOC Vienna won several international competitions in robotic sailing in recent years. It has also completed a several-day oceanographic research mission in the Baltic Sea.
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.

Click on image shows roboat video.

(news article in German), July 2012, Eckernfoerde, Germany. Collaboration with Jon Sneyers and Jochen Deferme, K.U. Leuven, and with Roboat sailing team of Roland Stelzer, INNOC Vienna, using CHR for autonomous robotic sailboat routing. Video: The Roboat in Action (from INNOC Vienna).

Longterm Routing for autonomous sailboats, research paper with Johannes Langbein Uni Ulm, Roland Stelzer INNOC Vienna, Jon Sneyers K.U. Leuven.
We implemented our algorithm in the declarative rule-based programing language Constraint Handling Rules (CHR). Our method is based on the A*-algorithm and incorporates changing weather conditions by dynamically adapting the underlying routing graph. A comparison with existing commercial applications yields considerably shorter computation times for our implementation. It works with real-life wind and currents forecasts, high-resolution map data, and provides a graphical user interface. The implementation was used for the long-term robot sailing world record attempt in 2012.

FWO-Project Termination Analysis for Constraint Handling Rules

External project partner of Prof. Danny De Schreye, K.U. Leuven, Belgium, 2008-2011.
In this project, we aim to develop several new, powerful techniques for termination analysis of CHR. Our main target is to develop techniques that are able to deal with a much large class of programs than what is currently the case. In particular, programs with propagation and simpagation rules should be in the scope of the new approach.
We will port a number of recent techniques, developed in the context of Term Rewrite Systems, such as dependency pairs, and apply them to obtain powerful termination analyzers for CHR. We will also adapt abstract interpretation for CHR to better support termination analysis. Finally, we will develop prototype systems for the most promising techniques developed in the project. We will set up a benchmark of CHR programs that form a challenge for termination analysis and we will test the implemented prototypes on this benchmark.

GLOB-CON - Rule-Based Propagation of Global Constraints

DFG Project FR 1390/1-1, 2006-2011.
External project partner is Dr. Sebastian Brand, Melbourne University, Australia.
The project is concerned with the formally correct and efficiently executable specification of constraint propagation for complex, global constraints by means of rules. A constraint satisfaction problem consists of a set of constraints which must be satisfied by every solution. Problems of this type, including NP-complete ones, can be solved well by problem simplification methods -- constraint propagation -- combined with search. Notably constraint-specific propagation methods can cause huge reductions of the search space at low cost, drastically reducing the solving time in turn. Specification as well as correct implementation of such methods requires substantial expertise, however. Rules have proved to be a useful formalism for the description of the propagation of primitive, simple constraints. Appropriate rule-based languages, notably Constraint Handling Rules, and corresponding implementations exist in which constraint propagation procedures can immediately be executed. Several methods for generating propagation rules automatically from declarative definitions of primitive constraints have been developed in the last years. The purpose of this project is to investigate the specification of the propagation of global constraints by rules, and the automatic generation of rule-based constraint propagation mechanisms for such constraints. This project proposal pursues the classical ideal of generating practical programs from formal specifications.

MTSeq: Multi-touch-enabled CHR-based Music Generation and Manipulation

With Jon Sneyers, K.U. Leuven, 2009-2010.

Click on image shows video demo
MTSeq combines GUI-driven multi-touch input technology with the CHR-based music generation system APOPCALEAPS and an advanced audio engine. APOPCALEAPS (Automatic POP Composer And LEArner of ParameterS) is an artificial intelligence application that can compose music and learn music styles from samples. It is written in an probabilistic extension of CHR called CHRiSM. MTSeq leads to an extended user experience and an intuitive, playful access to the music generation system, and thus introduces the capabilities of the programming language CHR to musicians and other non-computer-scientists in an appropriate way.
Video CHR-powered TTable MTSeq Multitouch Music Generation System Demo, Ulm University 2010.
Florian Geiselhart, Frank Raiser, Jon Sneyers, Thom Frühwirth. MTSeq - multi-touch-enabled music generation and manipulation based on CHR. CHR Workshop 2010.

FWO-Project Platform-independent Analysis and Implementation of Constraint Handling Rules

External project partner of Prof. Maurice Bruynooghe, Prof. Gerda Janssens, Prof. Bart Demoen, K.U. Leuven, Belgium, 2007-2010.
This 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, 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.
The project aims to create the first inter-institutional research group worldwide to investigate the cross-fertilization between reuse-oriented software engineering and application-embedded automated reasoning based on constraints and rules. Main issues are the meta-model and formal logic semantics of a hybrid object-oriented, rule-based constraint language to mediate between UML models and Java or C implementations to create reusable and extensible rule-based AR components for deduction, abduction, belief revision, inheritance, finite domain constraint solving and their seamless integration.
More about ROARS.

Projects at the University of Munich 1996-2002

JCK - Java Constraint Kit

IB-BMBF/SCyT Project ARG 030/98 INF: Java Constraint Kit, 1999-2002.
The main goal of the joint project is to develop a Java-based software tool for solving combinatorial, optimization and planning problems using constraint technology. Towards this end, we will implement a constraint logic programming kit in the internet programming language Java. Our choice of Java will allow easy implementation and wide-spread use of the tool. The concrete target of the JCK project is to embed the Constraint Handling Rules (CHR) into the JavaLog programming language. CHR is a special language for the description of constraint systems whereas JavaLog is an implementation of Prolog in Java.
JCK Java Constraint Kit

FLPC - Functional Programming with Constraints

DFG project Wi 841/4-1: Funktional-logische Programmierung mit Constraints, 1996-2002.
The goal of the project is the semantically well-founded integration of functional, logic and constraint-based programming, the implementation of a prototype language, the use and validation of the language in application studies and finally the development of a programming methodology.

DExVal - Simulating and Analyzing Hybrid Systems

IB-BMBF/CNPQ project: Formal Derivation of Meaningful Validation Experiments, 1998-2000.
We work on a tool to derive validation and testing tasks of software derived from formal specifications. The basis of our approach is the abstract execution of hybrid systems (including statecharts) in a constraint logic programming language. It is possible to run the hybrid system abstractly, i.e. without giving values to initial variables at all. Moreover, any variable in any state can be constrained. The programm then produces all valid runs possible that satisfy the given constraints on the variables. The result of a run are time-dependent constraints that must be satisfied by the variables of the hybrid system at different instances of time.
A. E. M. Ciarlini and T. Frühwirth, Automatic Derivation of Meaningful Experiments for Hybrid Systems, ACM SIGSIM Conference on AI, Simulation and Planning (AIS'2000), Tucson, Arizona, USA, March 2000. Paper, Slides.

ZEITRAUM - Spatio-temporal Reasoning for GIS

DAAD Project 314-VIGONI-DR: Spatio-temporal Reasoning for GIS, 2000-2001.
Together with the University of Pisa we aim at the development of new techniques to support spatio-temporal reasoning in databases, in particular geographic information systems (GIS), on the basis of constraint logics and constraint databases. The TACLP approach of Dr. Frühwirth shall be extended by spatial aspects and shall be integrated in deductive data models. In this way, we expect an improvement in the application-oriented representation of spatio-temporal relationships and the user-friendly integration and interaction of heterogeneous data models and information sources for problem solving.

TACLP - Temporal Annotated Constraint Logic Programming

A family of logics and associated programming languages for representing and reasoning about time is introduced. The family is conceptually simple while allowing for different models of time. Formulas can be labeled with temporal information using annotations. Both qualitative and quantitative (metric) temporal reasoning about definite and indefinite information with time points (instants) and time periods (temporal intervals) in different models of time are supported. The important property of the logics is that there is a systematic way to make their clausal fragment executable as a constraint logic program.
Temporal Annotated Constraint Logic Programming, Journal of Symbolic Computation, Special issue on Executable Temporal Logics (M. Fisher, M. Orgun and S. Kono, Eds.), Vol. 22, pp. 555-583, Academic Press, 1996, Paper (ps.Z).

POPULAR - Planning Cordless Communication

The versatility of CHR has been shown in a real-life application for SIEMENS involving geometric reasoning to find the optimal placement of senders for wireless portable devices (e.g. phones). Given a blue-print of the building and information about the materials used for walls and ceilings, POPULAR computes the minimal number of transmitters and their location by simulation and subsequent constraint-based optimization. This tool was regarded as one of the most innovative applications in telecommunications by IEEE Expert Magazine. POPULAR won the Telecom application contest of Telecom Italia at CP'98, the annual conference on constraint programming, in October 1998.

MRA - The Munich Rent Advisor

This real-life application brings constraints to the internet. It is a small expert system that allows one to calculate the typical rent of a flat in Munich based on your input to a questionnaire. The Munich Rent Advisor (MRA) won the prize for best application at JFPLC, Clermont Ferrand, France, June 1996. The MRA was shown at the SYSTEMS 96 and SYSTEMS 97 Computer Shows in Munich, Germany, and featured in several newspaper articles and AI Watch, UK. 10000's of requests have been served.

Project Participation 1984-1995


EU ESPRIT project #5291, Constraint Handling in Industry and Commerce, 1991-95. Development of a programming methodology for constraint languages and its application in industry.


EU ESPRIT project #7035, Logic and Change, 1994-96. Research in non-monotonicity and temporal change in logics and its application in programming languages.


EU ESPRIT project #6333, Intelligent Database Environment for Advanced Applications, 1995. Development of an object-oriented deductive database system.


EU ESPRIT project #2409, Environment for Qualitative Temporal Reasoning, 1992-93. Development and application of temporal reasoning to air traffic control and urban traffic control.

Ph.D. Grants

Fulbright grant and Austrian chamber of commerce grant, 1989-1990 for research stay with Prof. Dr. D. S. Warren, Computer Science Department, State University of New York at Stony Brook, USA.


Austrian National Bank Grant #2791, A Deductive Database Management System (in German), 1984-86. Development of a deductive database system at the Technical University of Vienna.

Thom Frühwirth, updated April 22, 2022