Constraint Handling Rules (CHRs) are a high-level rule-based programming language commonly used to write constraint solvers. The theoretical operational semantics for CHRs is highly non-deterministic and relies on writing confluent programs to have a meaningful behaviour. Implementations of CHRs use an operational semantics which is considerably finer than the theoretical operational semantics, but is still non-deterministic (from the user's perspective). This paper formally defines this refined operational semantics and proves it implements the theoretical operational semantics. It also shows how to create a (partial) confluence checker capable of detecting programs which are confluent under this semantics, but not under the theoretical operational semantics. This supports the use of new idioms in CHR programs. © Springer-Verlag 2004.
CITATION STYLE
Duck, G. J., Stuckey, P. J., García De La Banda, M., & Holzbaur, C. (2004). The Refined Operational Semantics of Constraint Handling Rules. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3132, 90–101. https://doi.org/10.1007/978-3-540-27775-0_7
Mendeley helps you to discover research relevant for your work.