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.