# Certifying the Decidability of the Word Problem in Monoids at Large

Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James

D Mitchell, Finn Smith

► To cite this version:

Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D Mitchell, et al. Certifying the Decidability of the Word Problem in Monoids at Large. CPP 2026 - 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2026, Rennes, France. pp.128-142, 10.1145/3779031.3779101 . hal-05448783

HAL Id: hal-05448783

https://hal.science/hal-05448783v1

Submitted on 8 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Certifying the Decidability of the Word Problem in Monoids at Large

Reinis Cirpons

Nantes Université, École Centrale
Nantes, CNRS, Inria, LS2N, UMR 6004
France
rc234@st-andrews.ac.uk

Florent Hivert

Université Paris-Saclay, CNRS, ENS
Paris Saclay, Inria, LMF
Gif-sur-Yvette, France
florent.hivert@lisn.fr

Assia Mahboubi

Nantes Université, École Centrale
Nantes, CNRS, Inria, LS2N, UMR 6004
France
Vrije Universiteit Amsterdam
The Netherlands
assia.mahboubi@inria.fr

Guillaume Melquiond

Université Paris-Saclay, CNRS, ENS
Paris Saclay, Inria, LMF
Gif-sur-Yvette, France
guillaume.melquiond@inria.fr

James D. Mitchell

University of St Andrews
United Kingdom
jdm3@st-andrews.ac.uk

Finn Smith

University of St Andrews
United Kingdom
fls3@st-andrews.ac.uk

## Abstract

While the word problem for monoids is undecidable in general, having a decision procedure for some finitely presented monoid of interest has numerous applications. This paper presents a toolbox for the Rocq proof assistant that can be used to verify the decidability of the word problem for a given monoid and, in some cases, to produce the corresponding decision procedure. As this verification can be computationally intensive, the toolbox heavily relies on proofs by reflection guided by an external oracle. This approach has been successfully used on several large presentations from the literature, as well as on a database of one million 1-relation monoids. The huge size of this database forced some unusual considerations onto the Rocq formalization, so that the formal proofs could be checked in a reasonable amount of time.

**CCS Concepts:** • Theory of computation → Logic and verification; Rewrite systems; Automated reasoning; • Mathematics of computing → Combinatorics on words.

**Keywords:** Word problem, Monoids, Decision procedure, Formal proof

## ACM Reference Format:

Reinis Cirpons, Florent Hivert, Assia Mahboubi, Guillaume Melquiond, James D. Mitchell, and Finn Smith. 2026. Certifying the Decidability of the Word Problem in Monoids at Large. In *Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP '26), January 12–13, 2026, Rennes, France*. ACM, New York, NY, USA, 15 pages. https://doi.org/10.1145/3779031.3779101

<figure><img src="image_2.png" /></figure>

This work is licensed under a Creative Commons Attribution 4.0 International License.

CPP '26, Rennes, France

© 2026 Copyright held by the owner/author(s).

ACM ISBN 979-8-4007-2341-4/2026/01

https://doi.org/10.1145/3779031.3779101

## 1 Introduction

The algebraic structures of monoids and semigroups generalise those of groups for describing collections of composable actions, respectively with or without an identity. Originating from abstract group theory, today these structures and their relationship with formal languages and automata theory underpin the foundations of theoretical computer science. They connect to a variety of other areas such as computational complexity theory and category theory, as well as partial differential equations and dynamical systems.

Presentations provide a convenient way of describing a monoid, consisting of a set of generators of the monoid (formally, symbols chosen in a given alphabet) and a set of relations (equalities among words over the generators). Here is an example with two generators and one relation:

$$ \langle \underbrace{a, b}_{\text{generators}} | \underbrace{baaba = a}_{\text{relations}} \rangle. \qquad (1) $$

In this monoid, the words *baabaabbaaba* and *a* are equal, because

$$ baabaab(baaba) = (b(baaba)ab = baaba = a. \qquad (2) $$

Monoids are sometimes also introduced more explicitly, e.g., as collections of functions from a set to itself that are closed under composition or as collections of not necessarily invertible matrices that are closed under product. The mathematical literature is replete with examples of presentations for specific semigroups and monoids defined by other means, or defined by presentations with a particular property. As expected, conducting proofs based on equational reasoning in concrete presentations by hand is error-prone, and some of these published papers contain mistakes, of varying magnitude, especially those not resorting to computer-aided calculations; see for example [17, 20].

Designing useful computer tools for making equational reasoning in monoids more reliable is not an easy task either,
in particular because a number of simple questions related to monoids are undecidable, or even open. For instance, the word problem for a monoid M defined by a presentation $\langle A | R \rangle$ is the decision problem asking whether or not two words with letters in A represent the same element of M. In the monoid defined by (1), Equation (2) shows that the words bbaabaabbaaba and a actually represent the same element.

The word problem is decidable for every finite monoid over any generating set. It is also decidable when the presentation is convergent, that is, when the rewriting system given by orienting its relations is locally confluent and terminating. In this case indeed, applying the rewriting system (whatever the strategy) to a word will compute a normal form. But in general, the word problem for monoids (and semigroups) is only semidecidable. There is indeed an algorithm showing that two words u and v represent the same element: by simply exploring every possible sequence of rewrites starting at u, one will eventually find v. Yet proving that u and v do not represent the same element is harder, and is in general undecidable. This means that there exists a monoid M defined by a presentation $\langle A | R \rangle$ such that no algorithm can show that u and v represent distinct elements of M.

It is known that, for groups, having only one relation makes the word problem decidable [29]. However, at the time of writing, the word problem for 1-relation monoids is still open. It has been one of the most prominent open questions in combinatorial algebra for at least the past 100 years; see for example Nyberg-Brodda's survey [35, 36] and the references therein. The current work actually originates in a talk given by Nyberg-Brodda in 2021 about his survey work. At this occasion, one of the authors of the present paper asked him the following question:

> "What is the smallest example of a 1-relation monoid where it is not known whether or not the word problem is decidable?"

The example provided in answer was the monoid given in (1). Yet, by using the Knuth-Bendix algorithm [28], as implemented in, for example, KBMAG [25] or libsemigroups [33], it is possible to show, in a matter of microseconds, that the following presentation defines a monoid isomorphic to that defined by (1):

$$ \langle a, b \mid baaa = aaba, baaba = a \rangle. \qquad (3) $$

It is then possible to show that the presentation in (3) is locally confluent and terminating, with respect to the lenlex ordering,<fnref n="1" /> meaning that the word problem is actually decidable for (1). Another presentation, from Nyberg-Brodda's survey [35, Section 6.1], where a confluent terminating rewriting system was seemingly not previously known was:

$$ \langle a, b \mid bababbbabba = a \rangle. \qquad (4) $$

With only slightly more effort, some of the authors of the present paper determined a confluent terminating rewriting system for the monoid defined by (4). First, introduce two new generators c = bababbbabb and d = bababbba, and replace all occurrences of bababbbabb and bababbba by c and d, respectively. Doing this results in a different way of presenting the monoid:

$$ \langle a, b, c, d \mid ca = a, c = dbb, d = bababbba \rangle. \qquad (5) $$

From this new presentation, the Knuth-Bendix algorithm produces a confluent terminating rewriting system with 64 rules involving words of length at most 604.

These early successes suggested further exploration to determine to what extent, and by what means, the word problem for 1-relation monoids can be solved using existing computational tools, combined with known mathematical results. An array of tools were efficiently implemented in Python and C++ and used to perform a large scale exploration, resulting in a database of proofs of the solvability of the word problem for many 1-relation monoids. It contains decidability proofs for more than one million 1-relation monoids, including all but 260 left-cycle free presentations $\langle a, b \mid u = v \rangle$ where $|u|, |v| \le 10$.

Each of these proofs consists of a certificate which provides enough information to reconstruct a decidability proof for a certain presentation in a mechanical way. Yet as illustrated by the monoid defined by (4), even a single one of these proofs may far exceed what a human being can manually verify. Therefore, one can only hope to achieve some confidence in the whole database by machine-checking all the certificates it contains. A time-tested way for achieving a high level of confidence is to turn such certificates into formal proofs that are then checked by some generic proof assistant. Some representative examples of formally verifying large computer-generated certificates are the four-colour theorem using the Rocq prover [18], the Kepler conjecture on dense sphere packing using the HOL Light and Isabelle systems [21], or the value of Schur Number Five using ACL2 [22].

The present paper presents three main contributions. The first is a large database of decidability proof certificates, for the word problem in 1-relation monoids. The second is a Rocq library of results and formally verified algorithms related to the word problem in monoids. The third is a methodology for conducting the computation-intensive formal verification of the database of proof certificates. In particular, this methodology was successfully employed to produce an axiom-free formal proof for all of the Knuth-Bendix-based proofs in the database, more than 200 000 in total.

The artefact submitted along with this paper contains the database of proof certificates [8] together with several proof checkers, including a Rocq-based one [23]. The corresponding Rocq development is conducted on top of the Mathematical Components library [30]. A 🤫 icon indicates a hyperlink

<footnote n="1">¹Comparing lengths of words first before applying the lexicographic order.</footnote>
to the original Rocq code developed for this project, here to the definition of the structure of commutative monoid.

The paper is organised as follows. Section 2 fixes some standard vocabulary and notation used through the paper, and provides some more details about the word problem for finitely presented monoids. Section 3 provides a high-level description of the array of techniques deployed to search for proofs of decidability, as well as the certificates produced for these proofs. Section 4 then describes the systematic procedure for turning each certificate in the database into a Rocq counterpart. At this stage, such a certificate is still an untrusted oracle, albeit in Rocq syntax, so Section 5 presents the available toolbox of formalised algorithms and theorems for obtaining a Rocq-checked proof that the word problem for a given presentation is decidable. The sheer size of the database means that Rocq would never succeed in formally checking all of it, short of the carefully optimised implementation described in Section 6. Section 7 gives some quantitative figures about the database and the resources needed for its verification. It also describes applications of the same methodology to examples from the literature but outside the database, illustrating how verified computational tools shall increase the reliability of proofs in semigroup theory.

## 2 Preliminaries

A semigroup is a set equipped with an associative binary operation. It is a monoid when this operation admits a two-sided identity element. Formally, a presentation $\mathcal{P}$ of a monoid is a pair $(A|R)$ consisting of a collection $A$ of distinct symbols and a set $R \subseteq A^* \times A^*$ of pairs of words over the alphabet $A$. We call $A$ the set of generators of $\mathcal{P}$ and $R$ the set of relations of $\mathcal{P}$. A pair $(u,v) \in R$ is sometimes written as $u = v$, when $R$ is clear from the context. In this paper, we only consider finite monoid presentations, that is, monoid presentations with finite sets of generators and finite sets of relations. The length of $\mathcal{P}$ is given by $|\mathcal{P}| = |A| + \sum_{(u,v) \in R} |u| + |v|$.

Let $x, y \in A^*$ be words. An elementary $R$-sequence (or just elementary sequence when $R$ is clear from the context) starting at $x$ and ending at $y$ is a sequence of words $w_1, \dots, w_n \in A^*$ such that $x = w_1, y = w_n$ and for each $i \in \{1, \dots, n-1\}$ there exist words $s, t, u, v \in A^*$ such that $w_i = sut, w_{i+1} = svt$ and either $(u, v) \in R$ or $(v, u) \in R$. If there exists an elementary sequence starting at $x$ and ending at $y$, we say that $x$ and $y$ are equal modulo $R$ and we write $R^\# \subseteq A^* \times A^*$ for the set of all pairs of words that are equal modulo $R$. A monoid is defined by $\mathcal{P}$ if it is isomorphic to the quotient $M_\mathcal{P} = A^*/R^\#$ of the free monoid $A^*$ by $R^\#$.

For instance, the symmetric group $S_n$, whose elements are the bijections from the set $\{1, \dots, n\}$ to itself, admits the following presentation [34], where $\sigma_i$ represents the adjacent transposition $(i, i+1)$, i.e., the bijection swapping element $i$ with element $i+1$, and $\varepsilon$ is the identity:

$$ \langle \sigma_1, \dots, \sigma_n \mid \sigma_i^2 = 1, \sigma_i \sigma_j = \sigma_j \sigma_i \text{ for } |i-j| > 1, (\sigma_i \sigma_{i+1})^3 = \varepsilon \rangle. $$

The following transformations of a monoid presentation $(A|R)$ are collectively known as *Tietze transformations*:

T1. add a relation $u = v$ to $R$ if $u = v$ is a consequence of $R$;

T2. remove a relation $u = v$ from $R$ if $u = v$ is a consequence of $R \setminus \{u = v\}$;

T3. add a generator $b \notin A$ and a new relation $b = w$ for some word $w \in A^*$;

T4. remove a generator $b \in A$ if there is a relation of the form $b = w$ in $R$ where $w$ does not contain $b$, in which case the transformation removes the relation $b = w$, and replaces every occurrence of $b$ in $R$ by $w$.

Two presentations $\mathcal{P}$ and $\mathcal{P}'$ are equivalent if $\mathcal{P}'$ can be obtained from $\mathcal{P}$ by a sequence of Tietze transformations. By [40, Proposition 2.5], $\mathcal{P}$ and $\mathcal{P}'$ are equivalent if and only if the corresponding monoids $M_\mathcal{P}$ and $M_\mathcal{P}'$ are isomorphic.

Arguably the most important decision problem for finitely presented monoids is the *word problem*. The word problem for a monoid $M$ defined by $(A|R)$ is the problem of deciding if two words over the alphabet $A$ are equal modulo $R$. Decidability of the word problem is preserved under monoid isomorphism and so it does not depend on the particular presentation used to present the underlying monoid. The smallest (in terms of number of relations) known example of a presentation with undecidable word problem has 3 relations [31]. We now turn our attention to the word problem in 1-relation monoids.

Let $(A|R)$ be a 1-relation presentation. In a 1-relation presentation, the number of relations is restricted, but what about the number of generators? It is possible via Evans [11] to encode an arbitrary finite set of generators into words over a 2-letter alphabet, while preserving the decidability of the word problem. But this encoding can make the relation words much longer and less structured. Fortunately, Adian and Oganesian [1] proved the following stronger reduction, which does not suffer from a size blow-up issue and is central to our purpose here:

**Theorem 2.1** ([35], Theorem 3.13). Let $M$ be the monoid defined by the presentation $\mathcal{P} = (A | u = v)$. Then there exists a monoid $M'$ defined by a presentation $\mathcal{P}'$ of one of the following forms

$$ \langle a, b | bu'a = av'a \rangle \quad \text{or} \quad \langle a, b | bu'a = a \rangle \qquad (6) $$

for some $u', v' \in \{a, b\}^*$, such that

(i) if the word problem is decidable in $M'$, then the word problem is decidable in $M$ also;

(ii) if $|A| \ge 2$ and $|u| + |v| \ge 3$, then $|\mathcal{P}'| \le |\mathcal{P}|$.

One-relation monoids defined by a presentation of one of the forms in (6) are called *left-cycle free*. The proof of Theorem 2.1 is constructive, and it is straightforward to find a presentation of the form given in (6) from the original 1-relation presentation using a combination of alphabet isomorphisms, reversals of relation words, *strong compression*,
and reduction to 2 generators, see [35, Sections 3.2 and 3.3] for details. Motivated by this reduction, in Section 3 we primarily consider 2-generated 1-relation monoids with a particular focus on left-cycle free monoids, for which various criteria establishing decidability of the word problem are known, for example Theorem 2.2; see also [35, Section 4.3].

**Theorem 2.2** (Theorem 4.9 [35], Oganesian 1978). Let $\mathcal{P} = \langle a, b \mid \text{bua} = \text{ava} \rangle$ for some $u, v \in \{a, b\}^*$. If the numbers of occurrences of a in bua and ava are equal, then the word problem is decidable for the monoid defined by $\mathcal{P}$. The analogous statement holds when the number of occurrences of b is used instead.

However, many 1-relation presentations exist for which existing criteria from the literature do not apply, and the decidability of the word problem for 1-relation monoids therefore remains open at the time of writing. A very important tool we use to resolve the decidability of the word problem in these cases is the Knuth-Bendix algorithm [28]. The rest of this section is dedicated to introducing the necessary background for this method.

Let $\langle A | R \rangle$ be a presentation. The set of relations $R$ also defines a *string rewriting system*, sometimes called a *semi-Thue system*, in the following manner. A word $w \in A^*$ *rewrites* to $w'$ by $R$, written $w \to_R w'$ when $w'$ is obtained by substituting a sub-word $u$ of $w$ by $v$ with $(u, v) \in R$. We simply write $w \to w'$ if $R$ is clear from the context. We write $\to_R^*$ for the reflexive and transitive closure of $\to_R$ and $\leftrightarrow_R^*$ for the reflexive, symmetric, and transitive closure of $\to_R$. It is not hard to show that $\leftrightarrow_R^* = R^\#$. Hence the decidability of the word problem in a monoid defined by $\langle A | R \rangle$ may follow from the study of $\to_R$, using techniques from abstract rewriting.

We say that $R$ is *terminating* if there is no infinite chain of words $w_1 \to_R w_2 \to_R w_3 \to_R \dots$. We say that $R$ is *locally confluent* when for any word $u \in A^*$ that can be rewritten by $R$ to two distinct words $v_1$ and $v_2$, there is a word $v$ such that $v_1 \to_R^* v$ and $v_2 \to_R^* v$. Finally $R$ is *convergent*, also called *complete*, if it is both terminating and locally confluent. If $R$ is convergent, then every word $w \in A^*$ admits a unique *normal form* $\bar{w}$ obtained by repeatedly rewriting $w$ via $R$ until no left-hand side of a relation in $R$ occurs as a subword in $w$. If a monoid is defined by $\langle A | R \rangle$ where $R$ is convergent, then the word problem is decidable. Indeed, to decide if $w_1$ equals $w_2$ modulo $R$, simply check if their normal forms are equal as words $\bar{w}_1 = \bar{w}_2$.

The Knuth-Bendix algorithm is a semidecision procedure which, given an input presentation $\mathcal{P} = \langle A | R \rangle$ attempts to compute a convergent set of relations $R'$ such that the presentations $\mathcal{P}$ and $\mathcal{P}' = \langle A | R' \rangle$ are equivalent. Consequently, if the Knuth-Bendix algorithm terminates, then the word problem is decidable in the monoid defined by $\mathcal{P}$. Roughly speaking, the algorithm proceeds by computing a set of critical pairs — pairs of distinct words $(v_1, v_2)$ such that $v \to_R v_1$,

$v \to_R v_2$ for some $v \in A^*$ which is in some sense minimal. For each such pair, the algorithm computes normal forms $\bar{v}_1$ and $\bar{v}_2$ using the current rewriting system $\to_R$. If $\bar{v}_1$ and $\bar{v}_2$ differ, then one of the relations $(\bar{v}_1, \bar{v}_2)$ and $(\bar{v}_2, \bar{v}_1)$ is added to $R$ in a process called orientation. To determine which, a user supplied *reduction order* on words, i.e., a well order which is stable under concatenation, is used. A commonly used reduction order is the *length-lexicographic* or *lenlex* ordering. Once a relation is added to $R$, the process is repeated until all normal forms of critical pairs coincide. All transformations applied to the set of relations $R$ by a Knuth-Bendix procedure can be justified using T1 and T2 Tietze transformations. It is sometimes possible to make the Knuth-Bendix procedure terminate, when it would otherwise not, by using a T3 Tietze transformation to add a new generator. We will use this strategy extensively in Section 3.

## 3 Searching and Crafting SA Certificates

A detailed description of the array of techniques employed to generate the database of certificates provided in the artifact is outside the scope of the present paper. However, we provide here some high-level comments on the resources put in its generation, so as to explain the need for formal proofs.

Various criteria on presentations have been devised that imply the decidability of the word problem, some specialised for 1-relation monoids and others that can be applied to any finitely presented monoid. Many of these criteria were already implemented in the libsemigroups C++ library [33]. The other criteria were not hard to implement given the framework for working with presentations available in libsemigroups. We provide below the list of criteria implemented, in roughly ascending order of time complexity, and providing references for the technical details that fall outside the scope of the present paper:

1. a presentation $\langle a, b | u = v \rangle$ is special [35, Section 2.3], i.e., $v = \varepsilon$;

2. a presentation $\langle a, b | u = v \rangle$ is length preserving, i.e., $|u| = |v|$;

3. a presentation $\langle a, b | u = v \rangle$ is cycle-free [35, Section 2.2], i.e., the initial (respectively terminal) letters of $u$ and $v$ differ;

4. a presentation is the *free product* of monogenic monoids, i.e., both sides of each relation are powers of the same generator;

5. any combination of reversing the relation words and exchanging the letters in the alphabet followed by *strong compression* [35, Section 3] (when strong compression is applicable) produces a left-cycle free presentation with decidable word problem;

6. a presentation satisfies the *first Watier condition* [35, Theorem 4.10];

7. a presentation is left-cycle free and *stabilizes a generator* [35, Theorem 4.9], i.e., the initial letters of $u$
and $v$ differ and there is a letter which occurs an equal number of times in $u$ and $v$;

8. a presentation satisfies the C(3) small overlap criterion [39], see also [32] for a description of the linear-time procedure implemented in libsemigroups;

9. the Knuth-Bendix algorithm terminates with respect to some lenlex ordering, with a timeout of 10 milliseconds per Knuth-Bendix instance;

10. after recursively replacing a subword with a generator (using the T3 Tietze transformation) up to depth 5, the Knuth-Bendix algorithm terminates with respect to some lenlex ordering, with a timeout of 10 milliseconds per Knuth-Bendix instance;

11. a backtracking version of Knuth-Bendix, similar to [45, 46], terminates, with a timeout of 20 minutes per instance;

12. a rewriting system derived from Adian's algorithm [9] terminates according to the termination provers match-box [44] and MultumNonMulta [24].

Note that criterion 5 produces a conditional proof of decidability of the word problem, i.e., after strong compression is performed, the decidability of the word problem in the compressed monoid still needs to be decided.

Time complexity here refers to the cost of checking that a given presentation falls under a specific criterion. Using checkers for these criteria as oracles, we were able to verify computationally, but without formal proofs, that the word problem is decidable for a large portion of 2-generated 1-relation monoids. This was done by enumerating all monoids defined by $\langle a, b | u = v \rangle$ with $|u|, |v| \le 10$ and applying each applicable decidability oracle in order of estimated time complexity. Oracles of higher complexity were only run if no oracle of lesser complexity could prove decidability of the word problem. Of the 4,190,209 presentations considered, 4,015,958 presentations were resolved by oracles checking criteria 1 through 5, leaving 174,251 left-cycle free presentations which were checked via oracles for criteria 6 through 12. Oracles for criteria 6, 7, and 8 were able to decide a further 135,405 instances. Oracles for criteria 9 and 10 resolved 37,624 instances and oracles for criteria 11 and 12 could establish decidability of the word problem in a further 962 instances. This left us with 260 left-cycle free monoid presentations $\langle a, b | u = v \rangle$ with $|u|, |v| \le 10$ for which the decidability of the word problem is unknown with current computational methods. The vast majority of the time was spent running the oracles for the Knuth-Bendix based oracles (implementing criteria 9, 10, and 11), with individual runs taking upwards of 4 hours per presentation and the total time taken across the whole corpus being about 6 days and 14 hours. This is a significant computational effort with practical benefits to the field of semigroup and monoid theory, as the small examples with unknown decidability can be used to tailor new decidability criteria for the word problem. However, the

large amount of time necessary to apply the oracles provides a significant barrier to reproducibility of the results.

At the same time, the results of these computations are hard to trust as the C++ implementations are not formally verified, and due to their size and complexity it seems unrealistic at the present moment to do so. For example, the libsemigroups implementation of the Knuth-Bendix algorithm consists of over 1600 lines of C++ code, which depends on correctness of many different associated data structures and implements various optimisations on top of the base algorithm. Despite numerous tests present in the libsemigroups test suite to catch bugs, it is not unreasonable to expect that there are still some errors present.

In order to increase our confidence in the claims of these oracles, we instrumented them so that they produce more useful output than a boolean answer. The SA certificate format<fnref n="2" /> was devised so as to facilitate the verification that the output of the oracle is correct, by storing enough information to reconstruct a complete proof in an independent, mechanical, exploration-free way. For example, to certify that the output of the Knuth-Bendix algorithm is correct, the SA format stores two pieces of data: a sequence of Tietze transformations taking the initial presentation to the final rewriting system and a termination ordering that is preserved by the final rewriting system $R$, i.e., a well-order $>_{R}$ on words that is compatible with concatenation and such that $l >_{R} r$ holds for all $(l, r) \in R$. From this information, an independent tool can verify the decidability claim by checking the following points:

1. the termination ordering is preserved;

2. every Tietze transformation is valid;

3. the final rewriting system is locally confluent.

Condition 1 can be immediately checked provided that an implementation of the termination ordering is given. This is the case for the lenlex ordering used by libsemigroups. Condition 2 is more involved since, e.g., verifying that a particular relation can be added by a Tietze transformation requires solving an instance of the word problem. Therefore, we additionally store a witness, in the form of a pair of rewrite sequences, verifying that the word problem instance is positive. It is not hard to check that the witness itself is well formed and correct. Finally, condition 3 can be checked using a similar approach to what is done in the Knuth-Bendix algorithm itself.

As a secondary benefit, producing certificates dramatically cuts the cost of reproducing the results. For example, checking if a presentation is equivalent to a presentation given by a convergent string rewriting system is undecidable, so the runtime of the Knuth-Bendix algorithm cannot be bounded above by any computable function. Therefore, the results of running the Knuth-Bendix algorithm are not

<footnote n="2">²SA is an abbreviation for St Andrews.</footnote>
easy to replicate, lowering their trustworthiness. To alleviate this, the SA certificates record additional information about the execution of the proof methods, such as the Knuth-Bendix algorithm. Enough information is recorded so that the validity of a stored result can be verified in polynomial time (in the total length of all relation words) without the need to re-run the original computational exploration. To give concrete numbers, verifying the whole proof database using a custom Python-based checker can be done in about 3 to 8 minutes, whereas re-running the Knuth-Bendix oracle with our search parameters can take up to 4 hours for just a single instance.

An SA certificate is structured as a tuple of *proof steps*, where each proof step is itself a tuple consisting of an index, a step type, the input presentation, and various step-specific parameters. More precisely, the tuple is as follows.

1. The proof step in the certificate is 0-indexed.

2. We distinguish two kinds of steps: transformations of the input presentation and decidability criteria. For example, the step type `tietze_add_relation` indicates that the step transforms the input presentation by applying a Tietze transformation. The step type `is_complete_rws` indicates that the step applies the convergent presentation criterion to establish decidability of the word problem.

3. The input presentation is a tuple of strings encoding the presentation before applying the transformation or criterion of the proof step.

4. The remaining parameters are proof step type specific, and they encode witnesses for the transformations and criteria applied.

Note that several decidability criteria may apply to a given monoid, and several convergent rewrite systems could be obtained from a same initial presentation. In particular, it remains useful to compute a convergent rewriting system for a monoid whose decidability follows from criteria 1 to 4, because such a rewriting system provides a normalisation algorithm for words.

An SA certificate enables the generation of various na-
tures of proofs. For instance, it can be converted to a hu-
man readable proof, in natural language. As noted earlier,
a human-readable format is however of little use in many
cases, as the proofs are too long to be checked by hand.
Two independent Python-based checkers, one utilising the
libsemigroups Pybind11 [7] package and a standalone one,
without any dependencies, are available to computationally
check the well-formedness of the SA certificates. These gave
some assurance of the correctness of the given certificates
and computation. However, minor bugs could still affect the
implementation of the checkers, which also do not prevent
from errors in the specification of the proof certificate for-
mat itself. The highest possible level of guarantee can only
be provided by a checker producing formal proofs. We thus

implemented a script that turns an SA certificate into the
formal definition in Rocq of a monoid presentation, i.e., a
Gallina term, and a template proof script of a decidability
proof for this monoid, to be machine-checked by Rocq's
kernel. Interestingly, designing this checker allowed us to
catch some minor bugs in the database, that other checkers
did not reveal. For instance, an early bug in the enumer-
ation code, combined with a defective implementation of
Condition 7, caused Condition 7 to be incorrectly applied to
some non-left-cycle free presentations in the database, e.g.,
⟨a, b | bbbbbbaaab = bababbbab⟩. Formalising Condition 7
in Rocq was instrumental in catching this bug.

Figure 1 gives a schematic overview of the pipeline taking
oracle-produced output and converting it to a Rocq certifi-
cate.

4 Rocq Certificates

The formal vocabulary used in Rocq certificates is provided
by a novel Rocq library about the word problem in monoids.
This library is abstracted over a fixed type Alph that is suf-
ficiently large to contain all the generators that might be
needed (e.g., the natural numbers). This parameter consider-
ably eases formal reasoning about selecting a fresh character,
distinct from an existing list of generators as required for
instance by Tietze transformations T3. The word type is then
defined as a list of elements of type Alph. A presentation
is described by the following ⤦ record which contains the
list pgen of generators, the list prelat of relations, as well as
proofs that the generators are distinct and that the relations
only use the given generators.

```h
Structure pres := Pres {
    pgen : seq Alph; (* generators *)
    prelat :> seq (word * word); (* relations *)
    uniq_pgen : uniq pgen; (* distinct generators *)
    wf_relat : all_relwords prelat (mem pgen) (* only use pgen *)
}.
```

A certificate for a presentation P is a term belonging to
one of the 15 cases of the prescertificate ⤦ variant type:

Variant prescertificate :=
  (* requires: rewriting certificate + termination ordering *)
  CompleteRewritingSystem of pres_cert & seq Alph
  (* requires: the repeated letter a in < a b | a^k = a^l > *)
  EqualNumberOfOccurrences of Alph
  Monogenic
  [ ... ten more cases ... ]
  (* Recursive certificates: reduction proofs to another presentation *)
  (* apply rev to all relation words keeping the gens and relation order *)
  Reverse of recursive_certificate
  (* requires: the word which is retained and the letter it is sent to *)
  StronglyCompressAndReduce of recursive_certificate &
    word & Alph.

Those 15 kinds of certificates fall into 3 broad categories:

* Complete rewriting system: Such a certificate indicates that the presentation *P* is equivalent to a convergent
<figure><img src="image_3.png" /><figcaption>Figure 1. A schematic representation of the pipeline taking an oracle computation trace to a full Rocq certificate.</figcaption></figure>

rewriting system. The certificate contains a large payload (see below) describing the sequence of Tietze transformations from P to the rewriting system.

*   **Simple criteria:** Those certificates usually only require a short computation to check and they provide some sufficient data to do so. For example, the certificate `EqualNumberOfOccurrences 1` corresponds to the criteria of Theorem 2.2, where the parameter 1 indicates which letter has the same number of occurrences.

*   **Recursive certificates:** They use some rather simple criteria to reduce the word problem for P to the one of another presentation Q, whose proof of decidability is given by some parameter r (see Section 6 for the type of r). A typical example is `Reverse r`, which claims that Q (as given by r) is the dual presentation of P obtained by reversing all the words in the relations. A much more involved reduction, which we will not detail, is strong compression.

We now describe in detail the most complicated case, which is the complete rewriting system. Its ▷ certificate consists of a sequence of Tietze transformations which modify the presentation until its relations can be trivially used as a convergent rewriting system.

Definition `pres_cert := seq transfo.`

A Tietze transformation either adds or removes a generator, or adds or removes a relation, while preserving the decidability of the word problem. To ensure this property, transformations come with a certificate. For instance, when adding a relation, the certificate of type `rew_cert` guarantees that both sides of the new relation are already equal, according to the relations of the current presentation. Tietze ▷ transformations are described by the following type:

Variant `transfo : Type :=`
| `add_gen` of Alph & word
| `add_rel` of word & word & `rew_cert`
| `rm_rel` of N & `rew_cert`.

Note that we do not represent Tietze T4 transformations, which remove generators. There are two reasons for that: this case is not needed to check the database, but more importantly, not having it implies that the identity is a morphism from the monoid defined by the presentation to the one described by the rewriting system. This greatly simplifies and speeds up the algorithm to decide the word problem, especially when there is a long sequence of Tietze transformations.

A certificate of type `rew_cert` guarantees the equality of two words by using a sequence of elementary rewriting steps. Suppose that P is a presentation with the following three relations.

$$ \mathit{babaabaa} = \mathit{abaaabaaa}, \mathit{baaa} = c, \mathit{babaac} = \mathit{acca}. $$

The following elementary sequence proves that these relations imply $babaac = abaaabaaaa$:

$$ \mathit{babaa}(c) = \mathit{babaa}(baaa) = (\mathit{babaabaa})a = (\mathit{abaaabaaa})a $$

The necessary information is given to Rocq by a sequence of ▷ rew_triple which instruct Rocq to apply relation number nrel at position pos in direction dirrel:

Record rew_triple : Type := RTriple {
  nrel : int;
  pos : N;
  dirrel : bool;
}.

Definition `rew_cert := seq rew_triple.`

Hence, the first step $babaa(c) = babaa(baaa)$ which consists in applying the reverse relation number 1 starting at position 5 (recall that sequences start at 0) is encoded by the left term below, whereas the second step $(babaaabaa)a = (abaaabaaa)a$ is described by the right term:

RTriple 1 5 false; RTriple 0 0 true;
# 5 Certification Toolbox

Our Rocq formalisation provides various ingredients needed to verify a Rocq certificate. More precisely, it provides implementations of all the algorithms checking that the various criteria involved in an SA certificate apply to a given presentation, and the formal statement of their correctness. It also provides complete formal proofs of correctness for the most computational intensive verification, those based on instances of the Knuth-Bendix algorithm.

## 5.1 Stating the Decidability of the Word Problem

In order to mechanise the decidability of the word problem for a given presentation P, we implement an effective method which evaluates to true on inputs u and v if and only if the two corresponding words are equal in the monoid defined by P. More precisely, we use the functional programming language provided by Rocq's type-theoretic foundations to actually implement this effective comparison test, which can in principle be executed by Rocq's reduction machine.<fnref n="3" /> Actually, these programs do not even rely on the dependent types featured by Rocq but rather on a limited, pure fragment of the OCaml programming language.

The resulting mechanised proof of decidability thus pairs a function, with boolean values, and a correctness proof. The correctness property states that if this function evaluates to true for two words u and v in the monoid defined by P, then u = v %[mod P] holds, and that otherwise u <> v %[mod P] holds. Observe that since the equality test is provided separately, resorting to non-constructive steps, or even axioms, in the correctness proof does not compromise the essence of the decidability result. We actually resort to Rocq's standard definition of ▷ decidability (which uses a sum type in sort Type) to express the decidability of the word problem for a presentation P:

Definition words_of P ::= [pred w | all (mem (pgen P)) w].

Definition WPdecidable P ::=
  ∀ u v, u ∈ words_of P → v ∈ words_of P →
  decidable (u = v %[mod P]).

Each Rocq certificate thus features a decidability statement of the form WPdecidable P, for P the presentation related to this certificate. Most of the time, this decidability is obtained by proving that the presentation P is ▷ isomorphic to some other presentation Q for which the word problem is decidable:<fnref n="4" />

Record isopres (P: pres) (Q: pres) := IsoPres {
  mor: {presmorph P → Q};
  inv: {presmorph Q → P};
  canmor: ∀ a: word,
    a ∈ words_of P → inv (mor a) = a %[mod P];
  caninv: ∀ b: word,

b ∈ words_of Q → mor (inv b) = b %[mod Q]
}.

Theorem isopres_dec P Q:
isopres P Q → WPdecidable Q → WPdecidable P.

Even minor changes in the presentation, like permuting the order of relations or renaming generators, require an isomorphism proof. Proving that two presentations are isomorphic is usually done through a sequence of Tietze transformations.

The function ▷ wfpres_cert: pres → pres_cert → bool is responsible for checking that a certificate c is well-formed with respect to a given presentation. Its correctness is expressed by the following ▷ theorem:

Theorem iso_final_pres:
  ∀ P c (wfc : wfpres_cert P c), isopres P (final_pres wfc)

which states that, if wfpres_cert P c returns true, there is an isomorphism from P to Q = final_pres wfc.

## 5.2 Proofs Based on Complete Rewriting Systems

No matter how many relations Q has, it suffices to prove that they define a terminating confluent system to establish the decidability of the word problem. These properties are characterised as follows, with R the rewriting system built from the relations of Q:

Definition terminating R :=
  well_founded (fun v u ⇒ v ∈ rewrites R u).
Definition confluent R := ∀ u v1 v2,
  rewrites_to R u v1 → rewrites_to R u v2 →
  exists2 w, rewrites_to R v1 w & rewrites_to R v2 w.

Theorem convergentrel_dec R:
  confluent R ∧ terminating R →
  ∀ u v, decidable (u = v %[mod R]).

To prove that R is terminating, the toolbox offers an algorithm that checks that all the relations are decreasing for some termination order. This order is given by the last argument of the CompleteRewritingSystem certificate.

To prove that R is locally confluent (and hence confluent), the toolbox computes all the critical pairs of R and then rewrites them into normal form. The relevant part of the algorithm is essentially

all (fun p ⇒ normal R p.1 == normal R p.2) (all_spairs R)

where normal is the normalisation function for the rewriting system and all_spairs R enumerates all its critical pairs.

## 5.3 Example of Mechanised Proof via a Rewriting System Certificate

To illustrate the way presentations and certificates are represented in Rocq and how they can be used, let us consider the following monoid presentation.

$$ \langle a, b | babaabaa = abaaabaaa \rangle \quad (7) $$

Its Rocq definition is as follows.

Definition present_entry := make_pres [:::0;1]
  [::: ([:::1;0;1;0;0;1;0;0], [:::0;1;0;0;0;1;0;0;0])].

<footnote n="3">³Mechanising undecidability requires more care; see for instance Forster's synthetic approach [12].</footnote>

<footnote n="4">⁴For conciseness, the Rocq definitions shown here use a single alphabet Alph. Our formalisation, however, is more generic, as the presentations P and Q have each their own alphabet.</footnote>
To show that the word problem is decidable for it, we will first relate it to the following presentation, with more generators and relations.

**Definition** present_final := make_pres [:::0;1;2]
[:: ([::1;0;0;0], [::2]);
([::1;0;1;0;0;2], [::0;2;2;0]);
([::1;0;1;0;0;1;0;0], [::0;2;2;0])].

Using the following SA certificate, we can prove that the
monoids respectively described by these two presentations
are isomorphic:

**Definition** cert : pres_cert := [:: add_gen 2 [:::1;0;0;0];
add_rel [:::1;0;1;0;0;2] [:::0;2;2;0]
[:: RTriple 1 5 false;
RTriple 0 0 true;
RTriple 1 1 true;
RTriple 1 2 true];
add_rel [:::1;0;1;0;0;1;0;0] [:::0;2;2]
[:: RTriple 0 0 true;
RTriple 1 1 true;
RTriple 1 2 true];
rm_rel 0
[:: RTriple 2 0 true;
RTriple 0 1 false;
RTriple 0 5 false]].

**Theorem** isopres_final : isopres present_entry present_final.
**Proof.**
have cert0k : wfpres_cert present_entry cert by [].
suff → : present_final = final_pres cert0k by apply:
iso_final_pres.
by apply/eqP; rewrite -eqpresE pgen_final_pres
prelat_final_pres.
**Qed.**

Finally, we can mechanise a proof that the corresponding
rewriting system for this new presentation is convergent,
based on an appropriate order on generators.

**Definition** final_order := [::1;0;2].
**Theorem** final_ok : convergent present_final.
**Proof.**
apply: (rgen_convergent
(reorderK (l := final_order) is_true_true) erefl).
**exact**: (check_convergenceP (rewrites1P _)
lt_sizelexi_stable sizelexi_natwf (fuel := 5)).
**Qed.**

A proof showing how the same property can be directly
extracted from the database is described in Section 6.

5.4 Other Formally Proved Criteria

While the combination of rewriting systems with Tietze
transformations covers a large set of presentations, there are
a few other special cases that have been formalised.

In particular, we provide a formal proof that the mono-
genic 1-relation case, ⟨a | a^k = a^l⟩, is decidable. We also
address the case of the free product of a decidable monoid
by a free monoid. Said otherwise, removing a free generator

from a presentation does not change its decidability. The
combination of both cases leads to the following ⤦ theorem:

**Theorem** free_product_monogenic_free_1rel_dec P:
size (prelat P) = 1 →
size (undup (flatten (relwords P))) = 1 →
WPdecidable P.

Another interesting case is when no relation of the pre-
sentation can change the ⤦ size of a word:

**Definition** is_homogeneous (R: relat) :=
all (fun r ⇒ size r.1 == size r.2) R.
**Theorem** homog_dec P:
is_homogeneous P → WPdecidable P.

Finally, we have also formalized all the simple transformations used in recursive certificates: changing the generators, reversing the presentation, and so on.

5.5 The Axiomatized Fragment

In the current state of our library, some of the theorems
used to guarantee the verification of SA certificates are not
formally proved. More precisely, for some algorithms, the
corresponding formal statement of correctness is made ex-
plicit, carefully transposing the statements of the literature,
but admitted. The exhaustive list of admitted results is as
follows:

1. special monoids ⟨A | u = ε⟩ [35, Corollary 2.8];

2. the correctness of strong compression, which removes
the left cycles from a 1-relation presentation (or from
its reverse) [35, Lemma 3.7];

3. the reduction of left-cycle free presentations to 2 gen-
erators only [35, Theorem 3.11];

4. cycle-free presentations [35, Theorem 2.6];

5. the case of Theorem 2.2;

6. the case of small overlaps [27, Theorem 1] and [39];

7. Watier presentations [35, Theorem 4.10].

We would like to emphasise that these theorems are widely
considered as correct by the community, but that their formal
verification would be a significant formalisation endeavour.

Finally, we acknowledge that in some cases our toolbox
does contain a fully verified algorithm, but it is specialised to
the checking of the database. For example, in the monogenic
case, only 1-relation presentations are supported, while the
approach can be generalised to larger presentations. Another
example is the free product; while our toolbox only handles
the case where one of the monoids is free, the approach can
be generalised to arbitrary monoids.

5.6 Number of Presentations

Table 1 shows the number of proofs by certificate type in the
extracted Rocq database as well as those of which are fully
certified (i.e., without the use of any admitted result). Note
that the database currently does not include any instance
of the Monogenic or Special cases, although both our Rocq
and Python/C++ checkers do implement the corresponding
<table><caption>**Table 1.** Number of proofs by certificate type in the extracted Rocq database as well as those of which are fully certified.</caption><thead><tr><th>Type</th><th>number</th><th>certified</th></tr></thead><tbody><tr><td>AlphabetIsom</td><td>484925</td><td>103882</td></tr><tr><td>AlphabetReorder</td><td>168226</td><td>827</td></tr><tr><td>CompleteRewritingSystem</td><td>55330</td><td>55330</td></tr><tr><td>CycleFree</td><td>70547</td><td>0</td></tr><tr><td>EqualNumberOfOccurences</td><td>56465</td><td>0</td></tr><tr><td>FlipAllRelations</td><td>385762</td><td>39813</td></tr><tr><td>FreeProductMonogenicAndFree</td><td>45</td><td>45</td></tr><tr><td>Monogenic</td><td>0</td><td>0</td></tr><tr><td>Reverse</td><td>259065</td><td>633</td></tr><tr><td>SmallOverlap</td><td>31204</td><td>0</td></tr><tr><td>Special</td><td>0</td><td>0</td></tr><tr><td>StronglyCompressAndReduce</td><td>502843</td><td>0</td></tr><tr><td>StronglyCompressToSpecial</td><td>555</td><td>0</td></tr><tr><td>Watier</td><td>44394</td><td>0</td></tr><tr><td>Total</td><td>2059361</td><td>200530</td></tr></tbody></table>

criteria. These criteria are actually straightforward to verify on a given presentation, but the correctness proof of the special case is fairly non-trivial.

## 6 Optimisations

When using an oracle to inform a proof checker, it might be tempting to produce very detailed certificates which fully guide the proof process, as the cost of producing a certificate is usually negligible. But the larger a certificate is, the longer it will take for the formal system to parse and type it, before it can be effectively used. At some point, the deserializa- tion cost might even exceed the verification cost, in which case it would be better to let the formal system perform an actual proof search, even if it duplicates the work already performed by the oracle. The generation of (yet untrusted) Rocq certificates from the database of SA certificates hits this limitation, and more than half of the time taken by this generation is actually spent reading the database.

In our case, we thus chose to give almost no information to the formal system regarding the confluence of the rewriting systems found by the oracle. Therefore, it is up to the decidability proofs to recompute all the critical pairs and to check that they have the same normal form. In our library, this computation is performed by executing an algorithm implemented as a Gallina term, and executed by a reduc- tion machine part of the kernel of the Rocq prover. We have nonetheless deployed various optimisation ingredients to make the computation tractable.

When computing a normal form, finding which rewriting rule applies at which position of a word is an operation worth optimising. That is why we have implemented a trie datastructure and formally verified the algorithms that manipulate it. A trie is a n-ary tree whose edges are labeled

by letters from Alph. If a sequence of letters along a path from the root of the tree matches the left-hand side of a rewriting rule, then the corresponding node stores the right-hand side of the rule.

Inductive trie :=
| Empty
| Trie : option word → array trie → trie.

Notice how the children of a node are stored using Rocq's primitive type array instead of, say, a generic list. This small optimisation makes it possible to offer O(1) access to the sub-tree corresponding to a given letter. It also reduces the memory footprint of the data structure. This concern about time and space efficiency applies more generally. For instance, when running the algorithms, we instantiate the abstract type Alph with Rocq's primitive type int. This means that a generator fits in a single memory word, and that comparing two generators is an O(1) operation.

Using a trie to find a matching rewriting rule instead of trying all of the rewriting rules in turn makes the confluence check much faster for some presentations. For example, on Renner's monoid B41 shown in Table 2, we get a 2000× speedup. Despite being already quite efficient, our implementation of tries lacks some well-known features [2]. Indeed, to find where to rewrite, the algorithm repeatedly queries the trie for every position of the input word. If no matching rule is found at position n, the traversal of the trie starts again from the root at position n + 1. In particular, the knowledge obtained from the unsuccessful traversal at position n is completely ignored. A realistic implementation would instead have stored enough information in the leaves of the trie, so that the traversal could restart from a better node than the root. This is future work.

Choosing compact data types (e.g., int, array) and implementing efficient algorithms are only part of the work. The proofs of decidability still have to run these algorithms inside the logic of the system. Fortunately, Rocq proposes some efficient evaluation strategies to normalise Gallina terms. Given the cost of our use cases, we have chosen the nativeLER machinery [5]. This machinery translates a Rocq term as well as its dependencies into an untyped OCaml term, compiles it into a dynamic library using the OCaml compiler, loads the library, and executes the term. The result of this computation (typically a boolean value in our case) is convertible to the original Rocq term. As long as all the parts of the original term are relevant, computing the result is much faster than any other convertibility mechanism provided by Rocq. Still, one has to be careful that the cost of the three other stages (translation, compilation, loading) does not cancel what can be gained from a faster convertibility test.

To reduce the impact of these three stages, one has to understand when OCaml terms are produced and compiled. First, once a Rocq script has been successfully checked (i.e., a .vo file has been produced from the .v script), all the toplevel
transparent definitions are translated into OCaml code and compiled into libraries. Second, when a Rocq script uses the `native_computemachinery` inside a proof, Rocq translates and compiles all the toplevel transparent definitions of the current script, as well as the terms under consideration. It then loads the needed libraries as well as the freshly compiled one and executes them. As a consequence, while having a single script containing toplevel definitions for a presentation and its certificate and a proof of decidability seems like a natural way of structuring a Rocq development, it is actually counterproductive. Indeed, it means that both the presentation and the certificate would be compiled twice (once for `native_computemachinery` inside the proof, and once the script has been successfully checked). Moreover, the certificate would bloat the library, as no subsequent call of `native_computemachinery` would ever need it. This overhead becomes noticeable when checking millions of proofs. Therefore, the proper way of structuring the development is to have the presentation in one script, and to have the proof of decidability in another script, with the certificate directly embedded inside the opaque proof. That way, not only are the presentations and the certificate compiled only once, but the certificate never makes it into the precompiled OCaml libraries.

To optimise even further the verification time, one needs to make as few calls to `native_computemachinery` as possible. In other words, instead of having one proof per presentation, one should have a single proof for a large number of presentations. Therefore, presentations are stored in large batches (i.e., Rocq lists), and all the presentations of a batch are checked at once. To do so, the parameter *r* of a recursive certificate is actually a record of the following type:

```hml
Record recursive_certificate := RecCert
  { lpres : seq (pres Alph);
   _ : ∀ P, P ∈ lpres → WPdecidable P;
   _ : int;
  }.
```

For example, the certificate `Reverse (RecCert _ CompleteRewritingSystem_batch032_dec.all_pres_dec 604)` would mean that decidability for the current presentation holds because it is the dual of the 604th presentation of the 32nd batch of presentations already proved using the complete rewriting system criteria.

Such a record might seem uselessly large, as its first field is a very long list of presentations, while only one is relevant for the certificate. Fortunately, the second field points to a named theorem, and by inference, the first field points to the list of presentations that appears in the statement of that theorem. As a consequence, such a recursive certificate has a constant size in practice. Accessing the actual presentation, however, takes a linear time.

Concretely, the output of the compilation for a batch is a theorem stating that all the presentations in this batch have a decidable word problem:

```hml
Lemma all_pres_dec (P : pres int) :
  P ∈ CompleteRewritingSystem_batch013_pres.all_pres →
  WPdecidable P.
```

As batch membership is a computable predicate, to recover a proof of decidability for a given presentation, the user just has to indicate which batch/file it is part of and Rocq will complete the proof. For example, here is how one can prove that the presentation from Equation (7) is ▷ decidable:

```hml
Require Import database_dec.
Require CompleteRewritingSystem_batch013_dec.
```

```hml
Definition P := make_pres [:::0;1]
  [::: ([:::1;0;1;0;0;1;0;0], [:::0;1;0;0;0;1;0;0;0])].
```

```hml
Theorem P_dec: WPdecidable P.
Proof.
exact: CompleteRewritingSystem_batch013_dec.all_pres_dec.
Qed.
```

Finally, there is one last optimisation we have applied. Indeed, the OCaml compiler does not produce the best machine code for the Rocq terms we are interested in. For example, the comparison of two generators should ideally be a single assembly instruction that compares two machine integers. But due to the generic nature of the algorithms we have implemented, the executed code first has to recover the comparison function from the record that instantiates the type `Alph` and then to apply it to the generators. More generally, while most computations are operationally trivial, they are hidden beyond layers upon layers of abstraction. Therefore, we have tediously reimplemented all the algorithms using only the most primitive constructions and we have proved that these new algorithms produce the exact same results as the generic ones, which is often trivial by convertibility. This optimisation, which is a kind of monomorphization or partial reduction, roughly brings a 10× speedup.

# 7 Benchmarks and Applications

The database of SA certificates produced from the oracle traces stores 700,262 proofs of decidability of 522,479 distinct monoids. The total size of all certificates is about 624 MB. Note that the decidability of the word problem is equivalent in certain monoids, for example those monoids obtained from a given presentation by applying an isomorphism permuting the alphabet, or those monoids obtained by reversing all relation words. The database de-duplicates such presentations, so the actual number of presentations which can be shown to have decidable word problem via the SA certificates is about 4 times larger. Consequently, when constructing the Rocq certificates, an increase in the number of proofs and presentations is observed, since we need to perform a certain amount of re-duplication to make the recursive proofs work. Some presentations of an especially simple form, namely
presentations $\langle a, b | u = v \rangle$ where $|u| = |v|$, are also omitted from the database.

Running the decidability oracles on the presentations and collecting the oracle traces took about 6 days and 14 hours running on a 2021 Macbook Pro M1 (16GB RAM) laptop, the vast majority of time (about 6 days and 7 hours) were spent on the Knuth-Bendix based decidability criteria. Converting these traces to the SA certificate format and constructing the database takes about 20 minutes. The Python based SA certificate checkers can be used to verify the well-formedness of the certificates in about 5 to 7 minutes total. The SA certificate database can be transformed into the Rocq certificate corpus in about 11 to 20 minutes. Formally verifying the correctness of the certificates with Rocq takes about 30 minutes, which is 6 to 8 hours of CPU time, measured on an Intel(R) Xeon(R) CPU E5-2650 v4 @2.20GHz server using only one core. More precisely, the time needed to compile the Rocq files are shared out this way:

* monoid theorem and checking infrastructure: 1'37";

* real life examples: 2'08";

* presentation definitions from the database: 146'16";

* certificates from the database: 277'51".

We also provide below the time needed to build and check the database using Python with the same processor and settings:

* building the database: 20'00";

* running the partial Python-only checker: 7'51";

* running the Python/C++ checker: 5'52".

## 7.1 Applications

We now discuss how the same methodology used to verify SA certificates can be used to scrutinise the existing literature. We provide two examples for which we have proved formally that certain two presentations did not represent the same monoid, although this was claimed on paper.

Our first example comes from [20, Page 720], where the authors give 3 presentations for the symmetric group: the first presentation (Equation 2.5) which they call the “Coxeter presentation” due to Moore [34], a second presentation (Equation 2.6) and a third presentation (unnumbered) at the bottom of the page which they found to be “even more symmetrical than the preceding one”. However this last presentation is wrong. For $n = 4$, it defines a group of cardinality 72! We check this last claim as follows. The Moore presentation is defined under the name ▷S4_Moore whereas the wrong presentation is defined under the name ▷not_S4. Then a C++ Knuth-Bendix oracle gives us two complete rewriting systems S4_rws and not_S4_rws which we certify to be equivalent to the original ones:

Theorem isopres_S4 : isopres S4_Moore S4_rws.

Theorem S4_rws_convergent : convergent (prelat S4_rws).

Theorem isopres_not_S4 : isopres not_S4 not_S4_rws.

Theorem not_S4_rws_convergent : convergent (prelat not_S4_rws).

Now isomorphism of presentation must preserve the cardinality of the defined monoid. To be able to speak about the cardinality of a finite presented monoid without defining the monoid itself, we use the following ▷ two definitions which formalise that a list 1 is a complete duplicate free list of normal forms of a presentation P:

Definition normalword_of (u : word) ::= (u ∈ words_of P) && (normal P u).

Definition isenet_normal (l : seq word) ::= uniq 1 ∧ ∨ u, (normalword_of P u) = (u ∈ l).

Then the ▷ preservation of the cardinality for two presentations P and Q is stated as follows:

Corollary isopres_sizeenet (P Q : pres) : isopres P Q → convergent P → convergent Q → ∨ 1P 1Q, isenet_normal P 1P → isenet_normal Q 1Q → size 1P = size 1Q

By comparing the two sizes we can prove the following ▷ theorem:

Theorem not_iseq_S4 : isopres S4_Moore not_S4 → False.

We stress that given the two presentations, all the proofs are automatic. There is only one place where human intervention is needed; since we do not know a priori that the monoids are finite, we cannot ensure that the enumeration of normal forms will terminate. So, we need to give an upper bound *b* to the length of the longest normal form. This bound is certified by checking that the list of normal forms of size *b* + 1 is empty.

We have applied the same methodology to some much larger monoids due to Renner, for which Godelle described a method to compute a presentation [17]. Recall that the *n*-th rook monoid is the monoid of the *n* × *n* matrices containing only 0 and 1 entries such that each line and row contains at most a single 1. It contains the symmetric group realised as the subset of matrices whose rows and columns contain exactly one 1. Renner monoids are the analogues of the rook monoid for Coxeter groups. There is a well-known complete classification of those, the *n*-th symmetric group is the Coxeter group of type $A_{n-1}$. For example the Renner monoid of type $B_{n-1}$ is the monoid of $2n \times 2n$ rook matrices which moreover are invariant when rotated by 180 degrees.

However, computing the presentation of a Renner monoid using [17, Theorem 1.1] requires to enumerate some specific elements in the associated Coxeter group which is a non-trivial task. In [17, section 3], the author wrongly argued that the number of those specific elements does not depend on *n* for the Renner monoids of type *B* and *D*. In his PhD thesis [15], Gay corrected the enumeration using more elementary combinatorial methods adding the missing relation in Godelle's presentations.

Our main result is to formally prove that Godelle's and Gay's presentations do not define isomorphic monoids and
that Godelle’s presentations are actually missing relations.<fnref n="5" />
We give Godelle’s presentation as a not_RennerB41 and add
the two missing relations to define RennerB41_Gay. As with
the symmetric group, we have used a C++ Knuth-Bendix or-
acle to get two complete rewriting systems RennerB41_Gay_rws
and not_RennerB41_rws.

By enumerating normal forms for both presentations, we
can then formally prove that Gay’s version defines a monoid
with exactly 13889 elements (which agrees with the known
number) whereas Godelle’s version contains at least 15327
elements. According to the C++ oracle, it is actually infi-
nite but we do not need to prove it. In the end, the whole
proof culminating with the following theorem takes only
a fraction of second to be checked by Rocq.

Theorem not_iso_RennerB41 :
isopres RennerB41_Gay not_RennerB41 → False.

Again the only human intervention is in the choice of the
bounds when computing normal forms.

As a benchmark, we considered more Renner monoids,
providing much larger examples. Table 2 summarises the
size of the presentation and certificates as well as the time
needed to check those.

# 8 Conclusion and Related Work

Pedersen’s work seems to be the only computer-aided ex-
ploration of the word problem for 1-relation monoids to
have been published [37]. It is devoted to left-cycle free 2-
generated 1-relation presentations ⟨a, b | u = v⟩ with u, v
of size less that 6 – when we consider sizes less than 10.
A similar computational exploration focusing on conver-
gent rewriting systems for 2-generated 2-relation monoids
⟨a, b | u₁ = v₁, u₂ = v₂⟩ with |u₁| + |v₁| + |u₂| + |v₂| ≤ 10 has
been undertaken in [38].

The Coq Library of Undecidability Proofs [14] contains a
proof that Thue system reachability and string rewriting are
undecidable [13]. Yet to the best of our knowledge, there has
been no previous attempt to formally verify results related to
the decidability of the word problem in monoids. The closest
work may be the formalisation of some combinatorics on
words in Isabelle/HOL [26], but it focuses on equations and
has almost no overlap with the present work.

On the topic of verifying certificates for abstract rewrite
systems with the Rocq prover, some loosely related works are
the libraries Coccinelle [10] and CoLoR [4]. They both aim at
checking termination certificates produced by external tools.
In particular, the Coccinelle library can be used to prove the
confluence of a rewriting system by checking the joinability
of critical pairs. The IsaFor/CeTa library [42] provides a broad
corpus of abstract rewriting techniques, including a checker
producing formal proofs of termination from certificates.

Verifying computer-produced mathematics typically relies
on the general approach which consists in using an untrusted
oracle to explore a certain search space and hopefully pro-
duce a certificate, used to build a formal proof a *posteriori*
and mechanically. Hales' formally verified proof of the Ke-
pler conjecture, on the density of sphere packing [21], is
a pioneering large-scale example of this approach, some-
how pushed to an extreme by the verification in ACL2 of
the value of the 5th Schur number [22]. In Rocq, the formal
disproof of the Hirsch conjecture [3] is a recent example
of computationally intensive formal proof of a contempo-
rary mathematical result, here in combinatorial optimisation.
Such applications have challenged the computational skills
of interactive provers and motivated significant evolutions
thereof, sometimes at the cost of extending the trusted base
of code. For instance, the verification of primality certifi-
cates [19, 43] was actually used to benchmark evaluation
strategies and primitive datastructures in Rocq.

Several large-scale projects are currently following an
approach similar to ours, and while they have completed
their computations, they are still in the process of publishing
their results. One can cite the *Equational Theories Project* [6],
which aims at finding a relation (either an entailment or
a counterexample) between all the 4694 magmas defined
by a single equational law containing at most four opera-
tions. Around 600 thousand relations were found and for-
mally proved using the Lean system, and the remaining 21
million relations can be deduced from those by transitive
closure. Another example is the *Busy Beaver Challenge* [41],
which aims at deciding the halting problem for 2-symbol
5-state Turing machines. The Rocq proof computationally
enumerates 180 million machines and runs them through
a formally verified algorithm using the *nativeLER compute* ma-
chinery in about 10 CPU hours. Interestingly enough, both
projects were highly collaborative, with volunteers provid-
ing manual proofs for all the cases that were eluding the
more automated approaches.

The presented experiment makes it possible to apply soft-
ware designed to produce formal proofs, like the Rocq prover,
to a meaningful benchmark of state-of-the-art computer-
produced mathematical proofs. We believe that the outcome
of this experiment is definitely promising, and we thus con-
clude by mentioning some research perspectives. The frame-
work we have presented is modular and open-ended; more
formal proofs of decidability will directly follow from prov-
ing formally more criteria and from the possible availability
of more termination certificates. We also believe that optimi-
sation aspects should be investigated further. In particular,
replacing bare tries by Aho-Corasick [2] and Gilman [16]
automata could not only improve the speed of rewriting but
it could also make it possible to compute the cardinality of a
monoid without enumerating the normal forms, and even
certify that a monoid is infinite.

<footnote n="5">⁵Note that we did not formalise the Renner monoids, so we do not prove
that Gay’s presentation is correct.</footnote>
<table><caption>**Table 2.** Table giving for each monoid the number of relations, the sum of the sizes of the left and right-hand sides of all the relations, the number of rules in the complete rewriting system, the sum of the sizes of the left and right-hand sides of all the rewriting rules, the number of Tietze steps to go from the presentation to the rewriting system, the time to formally verify the isomorphisms between the presentation and the rewriting system, the time to formally verify that the rewriting system is convergent, the size of (or a lower bound thereof) the monoid, the time to compute this size. Times are given in seconds.</caption><thead><tr><th>Monoid</th><th># rel</th><th>Σ rel</th><th># rules</th><th>Σ rules</th><th># Tietze</th><th>time iso</th><th>time conv.</th><th>size</th><th>time size</th></tr></thead><tbody><tr><td>Sym. Grp. S<sub>4</sub></td><td>6</td><td>22</td><td>7</td><td>30</td><td>7</td><td>0.002</td><td>0.195</td><td>24</td><td>0.011</td></tr><tr><td>not Sym. Grp S<sub>4</sub></td><td>15</td><td>114</td><td>18</td><td>178</td><td>27</td><td>0.015</td><td>0.184</td><td>72</td><td>0.017</td></tr><tr><td>Renner B<sub>4</sub></td><td>93</td><td>353</td><td>337</td><td>3589</td><td>340</td><td>0.028</td><td>0.388</td><td>13889</td><td>0.138</td></tr><tr><td>not Renner B<sub>4</sub></td><td>91</td><td>331</td><td>326</td><td>3447</td><td>327</td><td>0.023</td><td>0.164</td><td>≥ 15327</td><td>0.156</td></tr><tr><td>Renner B<sub>5</sub></td><td>136</td><td>523</td><td>1430</td><td>26666</td><td>1440</td><td>0.241</td><td>5.297</td><td>322021</td><td>2.259</td></tr><tr><td>Renner D<sub>4</sub></td><td>104</td><td>388</td><td>398</td><td>3173</td><td>402</td><td>0.030</td><td>0.479</td><td>10625</td><td>0.124</td></tr><tr><td>not Renner D<sub>4</sub></td><td>102</td><td>370</td><td>396</td><td>3155</td><td>398</td><td>0.027</td><td>0.359</td><td>≥ 12185</td><td>0.126</td></tr><tr><td>Renner D<sub>5</sub></td><td>151</td><td>577</td><td>1254</td><td>15242</td><td>1267</td><td>0.170</td><td>3.068</td><td>258661</td><td>1.719</td></tr><tr><td>not Renner D<sub>5</sub></td><td>147</td><td>533</td><td>1229</td><td>14893</td><td>1238</td><td>0.173</td><td>2.771</td><td>≥ 270926</td><td>1.951</td></tr></tbody></table>

We would also like to streamline the whole pipeline so as to improve the accessibility of this instrument to more users. In particular, we need to improve the current preliminary infrastructure available for proving formally that monoids, such as the Renner monoids or the symmetric group, actually are defined by a given presentation.

## Acknowledgments

This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No. 101001995).

## References

[1] Sergei Ivanovich Adyan and Oganesyan. 1987. On the word and divisibility problems for semigroups with one relation. *Math. Notes* 41 (1987), 235–240. [Mat. Zametki 41, 3 (1987)].

[2] Alfred V. Aho and Margaret J. Corasick. 1975. Efficient string matching: an aid to bibliographic search. *Commun. ACM* 18, 6 (June 1975), 333–340. doi:10.1145/360825.360855

[3] Xavier Allamigeon, Quentin Canu, and Pierre-Yves Strub. 2023. A formal disproof of Hirsch conjecture. In *12th ACM SIGPLAN International Conference on Certified Programs and Proofs*, Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic (Eds.). 17–29. doi:10.1145/3573105.3575678

[4] Frédéric Blanqui and Adam Koprowski. 2011. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. *Mathematical Structures in Computer Science* 21, 4 (2011), 827–859. doi:10.1017/S0960129511000120

[5] Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. 2011. Full reduction at full throttle. In *1st International Conference on Certified Programs and Proofs*. 362–377. doi:10.1007/978-3-642-25379-9_26

[6] Matthew Bolan, Joachim Breitner, Jose Brox, Nicholas Carlini, Mario Carneiro, Floris van Doorn, Martin Dvorak, Andrés Goens, Aaron Hill, Harald Husum, Hernán Ibarra Mejia, Zoltan Kocsis, Bruno Le Floch, Amir Livne Bar-on, Lorenzo Luccioli, Douglas McNeil, Alex Meiburg, Pietro Monticone, Pace P. Nielsen, Emmanuel Osalotioman Osazuwa, Giovanni Paolini, Marco Petracci, Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux, Jérémy Scanvic, Shreyas Srinivas, Anand Rao Tadipatri, Terence Tao, Vlad Tsyrklevich, Fernando Vaquerizo-Villar, Daniel Weber, and Fan Zheng. 2025. The Equational Theories Project: Advancing collaborative mathematical research at scale. https://teorth.github.io/equational_theories/paper.pdf

[7] Reinis Cirpons, Joseph Edwards, James D. Mitchell, Maria Tsalakou, and Murray Whyte. 2025. libsemigroups_pybind11. doi:10.5281/zenodo.16814180

[8] Reinis Cirpons, James D. Mitchell, and Finn Smith. 2025. *Database of 1-relation monoid word problem decidability proofs*. doi:10.5281/zenodo.17726031

[9] Reinis Cirpons, James D. Mitchell, and Finn L. Smith. 2025. Off with the head: termination provers and the word problem for 1-relation monoids. In *20th International Workshop on Termination*. https://www.imn.htwk-leipzig.de/WST2025/proceedings/WST2025_paper_16.pdf

[10] Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier Urbain. 2011. Automated certified proofs with CiME3. In *22nd International Conference on Rewriting Techniques and Applications (Leibniz International Proceedings in Informatics, Vol. 10)*, Manfred Schmidt-Schauss (Ed.). 21–30. doi:10.4230/LIPICS.RTA.2011.21

[11] Trevor Evans. 1952. Embedding theorems for multiplicative systems and projective geometries. *Proc. Amer. Math. Soc.* 3, 4 (1952), 614–620. doi:10.2307/2032597

[12] Yannick Forster. 2021. Church’s thesis and related axioms in Coq’s type theory. In *29th EACSL Annual Conference on Computer Science Logic (Leibniz International Proceedings in Informatics, Vol. 183)*, Christel Baier and Jean Goubault-Larrecq (Eds.). 21:1–21:19. doi:10.4230/LIPICS.CSL.2021.21

[13] Yannick Forster, Edith Heiter, and Gert Smolka. 2018. Verification of PCP-related computational reductions in Coq. In *9th International Conference on Interactive Theorem Proving (Lecture Notes in Computer Science, Vol. 10895)*, Jeremy Avigad and Assia Mahboubi (Eds.). 253–269. doi:10.1007/978-3-319-94821-8_15

[14] Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, and Maximilian Wuttke. 2020. A Coq library of undecidable problems. In *6th International Workshop on Coq for Programming Languages*. https://popl20 sigplan.org/details/CoqPL-2020-papers/5/A-Coq-Library-of-Undecidable-Problems

[15] Joël Gay. 2018. Representation of Monoids and Lattice Structures in the Combinatorics of Weyl Groups. Ph. D. Dissertation. Université Paris-Saclay. https://theses.fr/2018SACLS209

[16] Robert H. Gilman. 1979. Presentations of groups and monoids. 57, 2 (April 1979), 544–554. doi:10.1016/0021-8693(79)90238-2

[17] Eddy Godelle. 2011. Presentation for Renner monoids. *Bulletin of the Australian Mathematical Society* 83, 1 (Feb. 2011), 30–45. doi:10.1017/S0004972710000365
[18] Georges Gonthier. 2008. Formal proof—the four-color theorem. *Notices of the AMS* 55, 11 (2008), 1382–1393.

[19] Benjamin Grégoire, Laurent Théry, and Benjamin Werner. 2006. A computational approach to Pocklington certificates in type theory. In *8th International Symposium on Functional and Logic Programming (Lecture Notes in Computer Science, Vol. 3945)*, Masami Hagiya and Philip Wadler (Eds.). 97–113. doi:10.1007/11737414_8

[20] Robert M. Guralnick, William M. Kantor, Martin Kassabov, and Alexander Lubotzky. 2008. Presentations of finite simple groups: A quantitative approach. *Journal of the American Mathematical Society* 21, 3 (Feb. 2008), 711–774. doi:10.1090/s0894-0347-08-00590-0

[21] Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller. 2017. A formal proof of the Kepler conjecture. *Forum of Mathematics, Pi* 5 (2017), 29 pages. doi:10.1017/fmp.2017.1

[22] Marijn J. H. Heule. 2018. Schur Number Five. In *32nd AAAI Conference on Artificial Intelligence*, Vol. 32. 6598–6606. doi:10.1609/aaai.v32i1.12209

[23] Florent Hivert, Assia Mahboubi, James Mitchell, Guillaume Melquiond, and Reinis Cirpons. 2025. *hivert/MonoidPresentation: CPP-2026*. doi:10.5281/zenodo.17802630

[24] Dieter Hofbauer. 2016. MultumNonMulta: System description. In *15th International Workshop on Termination*, Aart Middeldorp and René Thiemann (Eds.). 90–90. http://cl-informatik.uibk.ac.at/workspace/events/wst2016.pdf

[25] Derek Holt. 2023. KBMAG: Knuth-Bendix on Monoids and Automatic Groups. https://gap-packages.github.io/kbmag/. GAP package version 1.5.11.

[26] Štěpán Holub and Štěpán Starosta. 2021. Formalization of basic combinatorics on words. In *12th International Conference on Interactive Theorem Proving (Leibniz International Proceedings in Informatics, Vol. 193)*, Liron Cohen and Cezary Kaliszyk (Eds.). 22:1–22:17. doi:10.4230/LIPIcs.ITP.2021.22

[27] Mark Kambites. 2009. Small overlap monoids I: The word problem. *Journal of Algebra* 321, 8 (2009), 2187–2205. doi:10.1016/j.jalgebra.2008.09.038

[28] Donald E. Knuth and Peter B. Bendix. 1970. Simple word problems in universal algebras. In *Computational Problems in Abstract Algebra*, John Leech (Ed.). Pergamon, 263–297. doi:10.1016/B978-0-08-012975-4.50028-X

[29] Wilhelm Magnus. 1932. Das Identitätsproblem für Gruppen mit einer definierenden Relation. *Math. Ann.* 106 (1932), 295–307. doi:10.1007/BF01455888

[30] Assia Mahboubi and Enrico Tassi. 2020. *Mathematical Components*. Zenodo. doi:10.5281/zenodo.3999478

[31] Yuri V. Matiyasevich. 1967. Simple examples of undecidable associative calculi. *Soviet Mathematics. Doklady* 8 (1967), 555–557.

[32] James D. Mitchell and Maria Tsalakou. 2023. An explicit algorithm for normal forms in small overlap monoids. *Journal of Algebra* 630 (2023), 394–433. doi:10.1016/j.jalgebra.2023.04.019

[33] James D. Mitchell, Michael Young, Finn Smith, Reinis Cirpons, Florent Hivert, Jerry James, Nicolas M. Thiéry, Joe Edwards, Wilf Wilson, Dima Pasechnik, Isuru Fernando, Jan Engelhardt, Luke Elliott, and Max Horn. 2023. *libsemigroups/libsemigroups: 2.7.0*. doi:10.5281/ZENODO.7761055

[34] Eliakim Hastings Moore. 1896. Concerning the abstract groups of order k! and ½k! holohedrically isomorphic with the symmetric and the alternating substitution-groups on k Letters. *Proceedings of The London Mathematical Society* (1896), 357–367. doi:10.1112/plms/s1-28.1.357

[35] Carl-Fredrik Nyberg-Brodda. 2021. The word problem for one-relation monoids: a survey. *Semigroup Forum* 103, 2 (Aug. 2021), 297–355. doi:10.1007/s00233-021-10216-8

[36] Carl-Fredrik Nyberg-Brodda. 2022. Correction to: The word problem for one-relation monoids: a survey. *Semigroup Forum* 105, 3 (Sept. 2022), 834–838. doi:10.1007/s00233-022-10310-5

[37] John Pedersen. 1985. Obtaining complete sets of reductions and equations without using special unification algorithms. In *European Conference on Computer Algebra (Lecture Notes in Computer Science, Vol. 204)*, Bob F. Caviness (Ed.). 422–423. doi:10.1007/3-540-15984-3_302

[38] Slava Pestov. 2025. A two-relation monoid does not have finite derivation type. (2025). In preparation.

[39] John Hermann Remmers. 1971. *Some algorithmic problems for semigroups: a geometric approach*. Ph. D. Dissertation. USA. AAI7123856.

[40] Nikola Ruškuc. 1995. *Semigroup presentations*. Ph. D. Dissertation. University of St Andrews. http://hdl.handle.net/10023/2821

[41] The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kądziołka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Naściszewski, savask, Tristan Stérin, Chris Xu, Jason Yuen, and Théo Zimmermann. 2025. Determination of the fifth Busy Beaver value. arXiv:2509.12337 [cs.LO] https://bbchallenge.org/

[42] René Thiemann and Christian Sternagel. 2009. Certification of termination proofs using CeTA. In *22nd International Conference on Theorem Proving in Higher Order Logics (Lecture Notes in Computer Science, Vol. 5674)*, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). 452–468. doi:10.1007/978-3-642-03359-9_31

[43] Laurent Théry. 2025. The CoqPrime Library. https://github.com/thery/coqprime

[44] Johannes Waldmann. 2004. Matchbox: A tool for match-bounded string rewriting. In *15th International Conference on Rewriting Techniques and Applications (Lecture Notes in Computer Science, Vol. 3091)*, Vincent van Oostrom (Ed.). 85–94. doi:10.1007/978-3-540-25979-4_6

[45] Ian Wehrman, Aaron Stump, and Edwin Westbrook. 2006. Slothrop: Knuth-Bendix completion with a modern termination checker. In *17th International Conference on Term Rewriting and Applications (Lecture Notes in Computer Science, Vol. 4098)*, Frank Pfenning (Ed.). 287–296. doi:10.1007/11805618_22

[46] Sarah Winkler, Haruhiko Sato, Aart Middeldorp, and Masahito Kurihara. 2013. Multi-completion with termination tools. *Journal of Automated Reasoning* 50, 3 (March 2013), 317–354. doi:10.1007/s10817-012-9249-2

Received 2025-09-12; accepted 2025-11-13