### Resumé

Originalsprog | Engelsk |
---|---|

Titel | Functional and Constraint Logic Programming : 26th International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers |

Antal sider | 130 |

Vol/bind | 11285 |

Forlag | Springer |

Publikationsdato | 2019 |

Sider | 112 |

ISBN (Trykt) | 978-3-030-16201-6 |

DOI | |

Status | Udgivet - 2019 |

Navn | Lecture Notes in Computer Science |
---|---|

Vol/bind | 11285 |

ISSN | 0302-9743 |

### Citer dette

*Functional and Constraint Logic Programming : 26th International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers*(Bind 11285, s. 112). Springer . Lecture Notes in Computer Science, Bind. 11285 https://doi.org/10.1007/978-3-030-16202-3_7

}

*Functional and Constraint Logic Programming : 26th International Workshop, WFLP 2018, Frankfurt/Main, Germany, September 6, 2018, Revised Selected Papers.*bind 11285, Springer , Lecture Notes in Computer Science, bind 11285, s. 112. https://doi.org/10.1007/978-3-030-16202-3_7

**Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs.** / Christiansen, Henning; Kirkeby, Maja Hanne.

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

TY - GEN

T1 - Towards a Constraint Solver for Proving Confluence with Invariant and Equivalence of Realistic CHR Programs

AU - Christiansen, Henning

AU - Kirkeby, Maja Hanne

PY - 2019

Y1 - 2019

N2 - Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general property of confluence modulo equivalence ensures that equivalent inputs are related to equivalent outputs, that need not be identical. Confluence under invariants is also considered. Constraint Handling Rules (CHR) is an important example of a rewrite based logic programming language, and we aim at a mechanizable method for proving confluence modulo equivalence of terminating CHR programs. While earlier approaches to confluence for CHR programs concern an idealized logic subset, we refer to a semantics compatible with standard Prolog-based implementations. We specify a meta-level constraint language in which invariants and equivalences can be expressed and manipulated as is needed for confluence proofs, thus extending our previous theoretical results towards a practical implementation.

AB - Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general property of confluence modulo equivalence ensures that equivalent inputs are related to equivalent outputs, that need not be identical. Confluence under invariants is also considered. Constraint Handling Rules (CHR) is an important example of a rewrite based logic programming language, and we aim at a mechanizable method for proving confluence modulo equivalence of terminating CHR programs. While earlier approaches to confluence for CHR programs concern an idealized logic subset, we refer to a semantics compatible with standard Prolog-based implementations. We specify a meta-level constraint language in which invariants and equivalences can be expressed and manipulated as is needed for confluence proofs, thus extending our previous theoretical results towards a practical implementation.

U2 - 10.1007/978-3-030-16202-3_7

DO - 10.1007/978-3-030-16202-3_7

M3 - Article in proceedings

SN - 978-3-030-16201-6

VL - 11285

SP - 112

BT - Functional and Constraint Logic Programming

PB - Springer

ER -