Projekter pr. år
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 nonlogical builtin 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 firstorder logic, that we show is not sufficient in the present case. We have introduced a formal metalanguage that allows reasoning about abstract states and derivations with metalevel restrictions that reflect the nonlogical 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.
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 firstorder logic, that we show is not sufficient in the present case. We have introduced a formal metalanguage that allows reasoning about abstract states and derivations with metalevel restrictions that reflect the nonlogical 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.
Originalsprog  Engelsk 

Tidsskrift  Formal Aspects of Computing 
Vol/bind  29 
Udgave nummer  1 
Sider (fratil)  5795 
Antal sider  39 
ISSN  09345043 
DOI  
Status  Udgivet  2017 
Projekter
 1 Afsluttet

Automatic Support for Proving Confluence Modulo Equivalence for Constraint Handling Rules
Christiansen, H. & Kirkeby, M. H.
Det Frie Forskningsråd  Natur og Univers
01/11/2015 → 31/12/2018
Projekter: Projekt › Forskning