Termination analysis of CHR revisited

Today, there exist two distinct direct approaches to prove termination of CHR programs. Both are applicable on separate classes of CHR programs. One approach, by T. Frühwirth, proves termination of CHR programs without propagation rules. A second approach deals with CHR programs with propagation rules. Due to its extended scope to such programs, it fails to prove termination for a class of CHR programs without propagation that are in the scope of Frühwirth's approach. In this paper, we introduce a termination condition for CHR which is strictly more powerful than both of these and deals with a new class of programs.status: publishe