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 omega_t. semantics. We propose also a translation from this semantics to linear logic.
@InProceedings{stephan:OASIcs.ICLP.2018.4, author = {St\'{e}phan, Igor}, title = {{A New Proof-Theoretical Linear Semantics for CHR}}, booktitle = {Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)}, pages = {4:1--4:17}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-090-3}, ISSN = {2190-6807}, year = {2018}, volume = {64}, editor = {Dal Palu', Alessandro and Tarau, Paul and Saeedloei, Neda and Fodor, Paul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2018.4}, URN = {urn:nbn:de:0030-drops-98707}, doi = {10.4230/OASIcs.ICLP.2018.4}, annote = {Keywords: Constraint Handling Rules, Linear Logic} }
Feedback for Dagstuhl Publishing