A complete and terminating execution model for constraint handling rules

DOI10.1017/S147106841000030XzbMATH Open1205.68215arXiv1007.3829MaRDI QIDQ3585170FDOQ3585170

Authors: Hariolf Betz, Frank Raiser, Thom Frühwirth 

Publication date: 19 August 2010

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1007.3829

Recommendations

• A Compositional Semantics for CHR with Propagation Rules
• Logic Programming
• Concurrent goal-based execution of constraint handling rules
• A Unified Semantics for Constraint Handling Rules in Transaction Logic
• A compositional semantics for CHR

zbMATH Keywords

operational semanticsconstraint handling rulespersistent constraintsexecution model

Mathematics Subject Classification ID

Logic programming (68N17) Semantics in the theory of computing (68Q55)

Cites Work

• Confluence and semantics of constraint simplification rules
• As time goes by: constraint handling rules
• Constraint Handling Rules
• A Linear-Logic Semantics for Constraint Handling Rules
• Linear Logical Algorithms
• Logical Algorithms meets CHR: A meta-complexity result for Constraint Handling Rules with rule priorities

Cited In (8)

• A Unified Semantics for Constraint Handling Rules in Transaction Logic
• Exhaustive Execution of CHR Through Source-to-Source Transformation
• An operational semantics for the cognitive architecture ACT-R and its translation to constraint handling rules
• Parallelism, concurrency and distribution in constraint handling rules: a survey
• Title not available (Why is that?)
• Containment in Rule-Based Models
• On proving confluence modulo equivalence for Constraint Handling Rules
• The expressive power of CHR with priorities

This page was built for publication: A complete and terminating execution model for constraint handling rules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3585170)