A Unified Analytical Foundation for Constraint Handling Rules
The non-deterministic rule-based programming language of Constraint Handling Rules (CHR) features a remarkable combination of desirable properties: a foundation in classical logic, powerful analysis methods for deciding program properties – especially confluence – and an efficient execution model. Upon a closer look, we observe several limitations to this asset. In this thesis, we introduce several concepts to amend for these short- comings. Firstly, we propose an unusually concise formulation of the two most important semantic interpretations of CHR. Secondly, we analyse the relationship between the major diverging interpretations of CHR. Finally, we found CHR on intuitionistic linear logic.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
a s b abstract analytic gap answer stability answer-stable Ap(S axiomatic axiomatic semantics built-in constraint CHR program CHR rule CHR_ classical declarative semantics classical logic congruence consider Constraint Handling Rules constraint identifiers Constraint Programming constraint theory CT CP(S criterion critical peak data-sufficient answers defined Definition denote di↵erent empty encoding entailment equivalence classes equivalence relation equivalence-based exists formulation furthermore global variables goal equivalence Hence Horn program implementation implies interpretation of CHR intuitionistic linear logic intuitionistic logic judgement Lemma leq(x,y linear-logic semantics Logic Programming logical equivalence logical reading multiset natural number normal form notion observe operational semantics partial-order phase semantics phase space proof tree propagation rule proper axioms pure CHR renamed respect S-equivalence Section semantic compliance semantics of CHR sequent calculus singular configurations SP(S st(S straint subset substructural logic syntax Theorem Thom Fr¨uhwirth tion token-store transition system well-behavedness