Article contents
A complete and terminating execution model for Constraint Handling Rules
Published online by Cambridge University Press: 09 July 2010
Abstract
We observe that the various formulations of the operational semantics of Constraint Handling Rules proposed over the years fall into a spectrum ranging from the analytical to the pragmatic. While existing analytical formulations facilitate program analysis and formal proofs of program properties, they cannot be implemented as is. We propose a novel operational semantics ω!, which has a strong analytical foundation, while featuring a terminating execution model. We prove its soundness and completeness with respect to existing analytical formulations and we provide an implementation in the form of a source-to-source transformation to CHR with rule priorities.
- Type
- Regular Papers
- Information
- Theory and Practice of Logic Programming , Volume 10 , Special Issue 4-6: 26th International Conference on Logic Programming , July 2010 , pp. 597 - 610
- Copyright
- Copyright © Cambridge University Press 2010
References
- 12
- Cited by