View: session overviewtalk overviewside by side with other conferences

09:00 | PRESENTER: Aart Middeldorp ABSTRACT. Having development closed critical pairs is a well-known sufficient condition for confluence of left-linear term rewrite systems. We present formalized results involving proof terms and unification that play an important role in the proof. |

09:30 | On Confluence of Parallel-Innermost Term Rewriting PRESENTER: Carsten Fuhs ABSTRACT. We revisit parallel-innermost term rewriting as a model of parallel computation on inductive data structures. We propose a simple sufficient criterion for confluence of parallel-innermost rewriting based on non-overlappingness. Our experiments on a large benchmark set indicate the practical usefulness of our criterion. We close with a challenge to the community to develop more powerful dedicated techniques for this problem. |

10:00 | Uniform Completeness ABSTRACT. We introduce uniform completeness and give a local characterisation of it. We show it yields a complete method for showing completeness of rewrite systems. |

11:00 | Seven Confluence Criteria for Solving COPS #20 ABSTRACT. COPS #20 is a thought-provoking confluence problem for term rewriting, posed by Gramlich and Lucas (2006). Although the term rewrite system of the problem is confluent, it is beyond the realm of classical confluence criteria such as Knuth and Bendix' criterion (1970) and Huet's parallel closedness (1980). In this talk we will discuss various solutions to the problem, recalling powerful confluence methods developed in the last decade and a half. |

12:00 | PRESENTER: Fabian Mitterwallner ABSTRACT. Conversion equivalence and normalization equivalence are important properties of two rewrite systems. We investigate how many constants are needed to reduce these properties to their ground versions for linear variable-separated rewrite systems. Our results are implemented in the decision tool FORT-h and formalized in Isabelle/HOL. The latter enables the validation of the proofs produced by the former in the certifier FORTify. |

Lunches will be held in Taub hall and in The Grand Water Research Institute.

14:00 | ABSTRACT. We characterize local confluence of *conditional rewrite systems* à la Huet, i.e., as the joinability of a set of conditional pairs including the usual conditional critical pairs and a new kind of pairs we call *conditional variable pairs*. |

14:30 | A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems PRESENTER: Takahito Aoto ABSTRACT. We introduce level-commutation of conditional term rewriting systems (CTRSs) that extends the notion of level-confluence, in a way similar to extending confluence to commutation. We show a criterion for level-commutation of oriented CTRSs, which generalizes the one for commutation of term rewriting systems in (Toyama, 1987). As a corollary, we obtain a criterion of level-confluence of oriented CTRSs which extends the one in (Suzuki et al., 1995). |

15:00 | Proving Confluence with CONFident PRESENTER: Raúl Gutiérrez ABSTRACT. This paper describes the proof framework used in CONFident, a framework to deal with different types of systems (term rewriting systems, context-sensitive term rewriting systems and conditional term rewriting systems) and different types of tasks (checking joinability of critical pairs, termination of systems, feasibility of reachibility problems or deducibility) and different techniques for proving confluence (including modular decompositions, transformations, etc.). |