ABSTRACT. Higher categories are a generalization of standard categories where there are not only $1$-cells between $0$-cells but more generally $n{+}1$-cells between $n$-cells. They are more and more used in mathematics, physics and computer science. They can notably be used to represent algebraic structures. There are several variants going from weak categories, that are the most general formalism but also the hardest to manipulate, to strict categories, simpler but less general. One usually wants both the expressive power of weak categories and the simplicity of strict categories. Semi-strict categories, such as Gray categories in dimension $3$, are an in-between formalism that it used in this work. Here, we are interested in proving \emph{coherence} of certain algebraic structures in dimension $3$ using rewriting, where ``coherence'' is the property that there is at most one $3$-cell between two $2$-cells. It amounts to compute critical pairs of a rewriting system and use a variant of Newmann's lemma. In this setting, an algorithm exists to compute these critical pairs.

ABSTRACT. We introduce string data structures as combinatorial descriptions of structured words on totally ordered alphabets. The data can be described by words through a reading map and can be constructed by using an insertion algorithm. The insertion map defines a product on datum. We show that the associativity of this product, the cross section property of the data structure, and the confluence of the rewriting system defined by the insertion map are equivalent properties. We explicit a coherent presentation of the monoid presented by the data structure, made of generators, rewriting rules describing the insertion of letters in words and relations among the insertion algorithms.

ABSTRACT. The computation of minimal convergent presentations for monoids, categories or higher-dimensional categories appear in low-dimensional combinatorial problems on these structures, such as coherence problems. A method to compute coherent presentations using convergent string rewriting systems was developed following works of Squier. In this approach, coherence results are formulated in terms of confluence diagrams of critical pairs. This work proposes an extension of these methods to string rewriting systems modulo.

ABSTRACT. We are studying rewriting systems over free modules, that is linear combinations of free generators with noninvertible coefficients. We provide a sufficient condition in terms of local confluence restricted to generators for the global rewrite relation to be confluent: this condition is formulated in terms of syzygies. When the coefficients belong to a domain, we equip the set of syzygies with a module structure, which provides a finer criterion: the local confluence has to be checked over a subset of syzygies, namely a generating set for the module structure.

ABSTRACT. On the one hand, ordered completion is a fundamental technique in equational theorem proving that is employed by automated tools. On the other hand, their complexity makes such tools inherently error prone. As a remedy to this situation we give an Isabelle/HOL formalization of ordered rewriting and completion that comes with a formally verified certifier for ordered completion proofs. By validating generated proof certificates, our certifier increases the reliability of ordered completion tools.

ABSTRACT. Confluence is a decidable property of ground rewrite systems. We present a formalization effort in Isabelle/HOL of the decision procedure based on ground tree transducers.

ABSTRACT. Unravelings are transformations of a conditional term rewriting system (CTRS, for short) into an unconditional term rewriting system (a TRS, for short) that is an overapproximation of the CTRS w.r.t. reduction. Unravelings are useful to prove confluence and operational termination of some CTRSs - we unravel a CTRSs to a TRS and try to prove termination and confluence using techniques for TRSs. A simultaneous unraveling has been proposed for normal 1-CTRSs and then a sequential one has been proposed for deterministic 3-CTRSs. Both the simultaneous and sequential unravelings are applicable to normal 1-CTRSs which are deterministic 3-CTRSs. In this paper, we first show that for a normal 1-CTRS, the simultaneously unraveled TRS is orthogonal iff so is the sequentially unraveled one. Then, we show that for a normal 1-CTRS, if the simultaneously unraveled TRS is terminating, then so is the sequentially unraveled one. Finally, we show that for a normal 1-CTRS with termination of the unraveled TRS, the simultaneously unraveled TRS is locally confluent iff so is the sequentially unraveled one.

ABSTRACT. Top trees with DAG representation can be used to compress huge ordered-tree data such as XML documents. However, one ordered tree can be represented by several top trees, so it is necessary to efficiently decide which top trees represent the same tree for higher compression rate. In this paper, we give a complete axiom system for the equational theory of top trees, called the cluster algebra. In order to prove the completeness, we introduce a reduction system on cluster algebra, and show the strong normalization and the unique normal form property.