ABSTRACT. CeTA was originally developed as a tool for certifying termination proofs which have to be provided as certificates in the CPF-format. Its soundness is proven as part of IsaFoR, the Isabelle Formalization of Rewriting. By now, CeTA can also be used for certifying confluence and non-confluence proofs. In this system description, we give a short overview on what kind of proofs are supported, and what information has to be given in the certificates. As we will see, only a small amount of information is required and so we hope that CSI will not stay the only confluence tool which can produce certificates.

ABSTRACT. In this note we introduce critical-pair-closing systems which are aimed at analyzing confluence of term rewriting systems. Based on the notion two new confluence criteria are presented. One is a generalization of weak orthogonality based on relative termination, and another is a partial solution to the RTA Open Problem #13.

ABSTRACT. This extended abstract breifly introduces rewriting of networks (directed acyclic graphs with the extra structure needed to serve as expressions for PROducts and Permutations categories) and describes the critical pairs aspects of this theory.

ABSTRACT. This paper improves the existing criterion for proving confluence of a normal conditional term rewriting system (CTRS) via the Serbanuta-Rosu transformation, a computationally equivalent transformation of CTRSs into unconditional term rewriting systems (TRS), showing that a weakly left-linear normal CTRS is confluent if the transformed TRS is confluent. Then, we discuss usefulness of the optimization of the Serbanuta-Rosu  transformation, which has informally been proposed in the literature. 

ABSTRACT. We introduce the notion of higher dimensional linear rewriting system for presentations of algebras generalizing the notion of noncommutative Gröbner bases. We show how to use this notion to compute homological invariants of associative algebras, related to confluence properties of presentations of these algebras. Our method constitutes a new application of confluence in algebra.

ABSTRACT. Métivier (1983) proved that every confluent and terminating rewrite system can be transformed into an equivalent canonical rewrite system. He also proved that equivalent canonical rewrite systems which are compatible with the same reduction order are unique up to variable renaming. In this note we present simple and formalized proofs of these results. The latter result is generalized to the uniqueness of normalization equivalent reduced rewrite systems.

ABSTRACT. This paper briefly sketches that "non-E"-overlapping and weakly-shallow TRSs are confluent" by extending reduction graph in our previous work (M.Sakai and M.Ogawa. Weakly-non-overlapping non-collapsing shallow term rewriting systems are confluent. Information Processing Letters vol.110, 2010) by introducing constructor expansion. A term is weakly shallow if each defined function symbol appears either at the root or in the ground subterms, and a TRS is weakly shallow if the both sides of rules are weakly shallow. The non-E-overlapping property is undecidable for weakly shallow TRSs and a decidable sufficient condition is the strongly non-overlapping condition. A Turing machine can be simulated by a weakly shallow TRS (p.27 in J.W.Klop, Term Rewriting Systems, 1993); thus the word problem is undecidable,in contrast to shallow TRSs.

ABSTRACT. The 3rd Confluence Competition (CoCo 2014) runs live. The competition is part of the FLoC'14 Olympic Games.