A New Proof-theoretical Linear Semantics for CHR
Résumé
Constraint handling rules are a committed-choice language consisting of multiple-heads guarded rules that rewrite constraints into simpler ones until they are solved. We propose a new proof theoretical declarative linear semantics for Constraint Handling Rules. We demonstrate completeness and soundness of our semantics w.r.t. operational ωt semantics. We propose also a translation from this semantics to linear logic.