Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Automating Termination Proofs for CHR
verfasst von : Paolo Pilozzi, Danny De Schreye
Erschienen in: Logic Programming
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We propose a constraint-based approach towards automated termination analysis of Constraint Handling Rules (CHR). Similar to such approaches for Logic Programming (LP), we define a symbolic level mapping on atoms of the program and express termination conditions using these. Then, we search for an assignment to the symbolic coefficients, validating the termination conditions. However, different from the approaches developed for LP, termination of CHR programs is concerned with multi-headed rules, while the existing constraint-based approaches in LP are developed for definite programs. These cannot be adapted directly to a multi-headed context. In the following we discuss a constraint-based approach for CHR programs and show how such an approach can be obtained by an elegant reuse of existing techniques in LP. We evaluate the approach, using our implementation, CHRisTA.