| Home > Publications > Reports > Informatics (CW) |
CW 487
Paolo Pilozzi, Tom Schrijvers, and Danny De Schreye
Proving termination of CHR in Prolog: A transformational approach
Abstract
In this paper we present a termination preserving transformation from Constraint Handling Rules to Prolog. The transformation is sound w.r.t. termination under the theoretical semantics of Constraint Handling Rules. It does not consider the presence of a propagation history. The transformation allows for the direct reuse of termination proof methods from Logic Programs and Term-Rewrite Systems, yielding the first fully automatic termination proving for Constraint Handling Rules. We formalize the transformation and show usefulness of the approach. We transform a set of CHR programs, by an implementation of the transformation and show termination by using existing termination tools for Logic Programs and Term-Rewrite Systems.
report.pdf (174K) / mailto: P. Pilozzi