Proving termination of CHR in Prolog: A transformational approach
Paolo Pilozzi, Tom Schrijvers, Danny De Schreye · Lirias (KU Leuven) · 2007
In this paper, we present a termination preserving transformation of CHR to Prolog. This allows the direct reuse of termination proof methods from LP and TRS for CHR, yielding the first fully automatic termination proving for CHR. We implemented the transformation and used existing termination tools for LP and TRS on a set of CHR programs to demonstrate the usefulness of our approach.