NDLI: On proving confluence modulo equivalence for Constraint Handling Rules

Content Provider	Springer Nature Link
Author	Christiansen, Henning Kirkeby, Maja H.
Copyright Year	2016
Abstract	Previous results on proving confluence for Constraint Handling Rules are extended in two ways in order to allow a larger and more realistic class of CHR programs to be considered confluent. Firstly, we introduce the relaxed notion of confluence modulo equivalence into the context of CHR: while confluence for a terminating program means that all alternative derivations for a query lead to the exact same final state, confluence modulo equivalence only requires the final states to be equivalent with respect to an equivalence relation tailored for the given program. Secondly, we allow non-logical built-in predicates such as var/1 and incomplete ones such as is/2, that are ignored in previous work on confluence.To this end, a new operational semantics for CHR is developed which includes such predicates. In addition, this semantics differs from earlier approaches by its simplicity without loss of generality, and it may also be recommended for future studies of CHR.For the purely logical subset of CHR, proofs can be expressed in first-order logic, that we show is not sufficient in the present case. We have introduced a formal meta-language that allows reasoning about abstract states and derivations with meta-level restrictions that reflect the non-logical and incomplete predicates. This language represents subproofs as diagrams, which facilitates a systematic enumeration of proof cases, pointing forward to a mechanical support for such proofs.The Project is supported by The DanishCouncil for IndependentResearch, Natural Sciences, Grant No. DFF4181-00442. The second author’s contribution received funding from the European Union Seventh Framework Programme (FP7/2007-2013) under Grant Agreement No. 318337, ENTRA—Whole-Systems Energy Transparency.
Starting Page	57
Ending Page	95
Page Count	39
File Format	PDF
ISSN	09345043
Journal	Formal Aspects of Computing
Volume Number	29
Issue Number	1
e-ISSN	1433299X
Language	English
Publisher	Springer London
Publisher Date	2016-11-16
Publisher Place	London
Access Restriction	Subscribed
Subject Keyword	Math Applications in Computer Science Theory of Computation Computational Mathematics and Numerical Analysis
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

On Proving Confluence Modulo Equivalence for Constraint Handling Rules

A framework for Satisfiability Modulo Theories

Shape Neutral Analysis of Graph-based Data-structures

Program equivalence by circular reasoning

Unifying theories in ProofPower-Z

A UTP semantics for Circus

Constraint-based correctness proofs for logic program transformations

Exploring probabilistic bisimulations, part I

Deciding orthogonal bisimulation

On proving confluence modulo equivalence for Constraint Handling Rules

Similar Documents

On Proving Confluence Modulo Equivalence for Constraint Handling Rules

A framework for Satisfiability Modulo Theories

Shape Neutral Analysis of Graph-based Data-structures

Program equivalence by circular reasoning

Unifying theories in ProofPower-Z

A UTP semantics for Circus

Constraint-based correctness proofs for logic program transformations

Exploring probabilistic bisimulations, part I

Deciding orthogonal bisimulation

On proving confluence modulo equivalence for Constraint Handling Rules