<p>The two obvious references are:</p>
<ul>
<li><p>Chapter 7 of <a href="https://rads.stackoverflow.com/amzn/click/com/0521779200" rel="noreferrer" rel="nofollow noreferrer">Term Rewriting and All That</a>, notable for its pedagogy and accessible examples</p>
</li>
<li><p>Chapter 7 of <a href="https://rads.stackoverflow.com/amzn/click/com/0521391156" rel="noreferrer" rel="nofollow noreferrer">Term Rewriting Systems</a>, notable for its completeness and attention to detail, though a bit dated at this point I guess.</p>
</li>
</ul>
<p>Note that neither refers to completion as &quot;Knuth-Bendix&quot; completion in the index, since the science of completion has come a long way since it was first introduced. <a href="https://www.cs.tau.ac.il/%7Enachum/papers/survey-draft.pdf" rel="noreferrer">This survey</a> by Dershowitz and Jouannaud might be a bit more historical.</p>
<p>It might help to understand what your needs are, since the field is vast, and somewhat technical. Are you trying to use a completion algorithm? Implement it? Adapt it to a specific setting?</p>

CC BY-SA 4.0
2020-10-30T15:58:30.443Z
"It might help to understand what your needs are" -- My goal is to understand what critical pairs are, what the Knuth-Bendix algorithm is, why it is correct, what purpose the concept of "critical pairs" serves and what purpose the algorithm serves. I became familiar with this algorithm by reading Sperschneider & Antoniou's "Logic: A Foundation for Computer Science" (Addison-Wesley, 1991), but I don't like the explanation given there and I'm looking for an alternative.
Evan Aad
CC BY-SA 4.0
2020-10-30T21:58:44.493Z
Critical pairs are a reasonably simple concept, heck, the wikipedia page is not too bad: https://en.wikipedia.org/wiki/Critical_pair_(logic). Completion algorithms are more complex, and the papers I gave give a reasonable first stab.
cody
CC BY-SA 4.0
2020-10-30T15:45:36.670Z
2020-10-30T15:45:36.670Z
cody
<p>There is a rather technically-detailed description to be found in any of the following:</p>
<p>D.F. Holt, D.B.A. Epstein, and S. Rees.
The use of knuth-bendix methods to solve the word problem in automatic groups.
J. Symbolic Computation, 12:397--414, 1991.</p>
<p>Charles C. Sims.
Computation with Finitely Presented Groups.
Cambridge, 1994.</p>
<p>Derek F. Holt.
The warwick automatic groups software.
In Proceedings of DIMACS Conference on Computational Group Theory, Rutgers, March 1994</p>
<p>A more informal, easily readable description can be found in Geoff Smith’s “Topics in Group Theory”.</p>

CC BY-SA 4.0
2020-10-29T23:14:39.763Z
2020-10-29T23:14:39.763Z
NietzscheanAI
<p>I'm looking for an explanation of critical pairs and the Knuth-Bendix completion algorithm that is at once rigorous and of high pedagogical value, i.e. clear, detailed, containing illustrative examples preferably with drawings, and reasonably self-contained. It can be inside a book, an article, lecture notes, website, whatever. Possible languages: English, French, German.</p>

CC BY-SA 4.0
2020-10-27T13:23:31.830Z
You should find that in any textbook on term rewriting.
Jan Johannsen
CC BY-SA 4.0
2020-10-27T13:42:41.270Z
@JanJohannsen: That is obvious. The question was not "where can I find an explanation of critical pairs", but "where can I find a clear and rigorous explanation of critical pairs". Answering this question requires judgement and personal familiarity with specific textbooks or other sources. Not all sources are equally good answers to this question.
Evan Aad
<reference-request><term-rewriting-systems><first-order-logic>
A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?
Evan Aad
# A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?

(Asked by: username_0 on 2020-10-27)

I'm looking for an explanation of critical pairs and the Knuth-Bendix completion algorithm that is at once rigorous and of high pedagogical value, i.e. clear, detailed, containing illustrative examples preferably with drawings, and reasonably self-contained. It can be inside a book, an article, lecture notes, website, whatever. Possible languages: English, French, German.

**Tags:** reference-request, term-rewriting-systems, first-order-logic
> **Comments:**
> **username_1**: You should find that in any textbook on term rewriting.  
> **username_0**: @JanJohannsen: That is obvious. The question was not "where can I find an explanation of critical pairs", but "where can I find a clear and rigorous explanation of critical pairs". Answering this question requires judgement and personal familiarity with specific textbooks or other sources. Not all sources are equally good answers to this question.  

---

## 2 answers

### Answer by username_2 on 2020-10-30. Score: 5

The two obvious references are:

* Chapter 7 of [Term Rewriting and All That](https://rads.stackoverflow.com/amzn/click/com/0521779200), notable for its pedagogy and accessible examples
* Chapter 7 of [Term Rewriting Systems](https://rads.stackoverflow.com/amzn/click/com/0521391156), notable for its completeness and attention to detail, though a bit dated at this point I guess.

Note that neither refers to completion as "Knuth-Bendix" completion in the index, since the science of completion has come a long way since it was first introduced. [This survey](https://www.cs.tau.ac.il/%7Enachum/papers/survey-draft.pdf) by Dershowitz and Jouannaud might be a bit more historical.

It might help to understand what your needs are, since the field is vast, and somewhat technical. Are you trying to use a completion algorithm? Implement it? Adapt it to a specific setting?

> **Comments:**
> **username_0**: "It might help to understand what your needs are" -- My goal is to understand what critical pairs are, what the Knuth-Bendix algorithm is, why it is correct, what purpose the concept of "critical pairs" serves and what purpose the algorithm serves. I became familiar with this algorithm by reading Sperschneider & Antoniou's "Logic: A Foundation for Computer Science" (Addison-Wesley, 1991), but I don't like the explanation given there and I'm looking for an alternative.  
> **username_2**: Critical pairs are a reasonably simple concept, heck, the wikipedia page is not too bad: https://en.wikipedia.org/wiki/Critical_pair_(logic). Completion algorithms are more complex, and the papers I gave give a reasonable first stab.  

---

### Answer by username_3 on 2020-10-29. Score: 3

There is a rather technically-detailed description to be found in any of the following:

D.F. Holt, D.B.A. Epstein, and S. Rees.
The use of knuth-bendix methods to solve the word problem in automatic groups.
J. Symbolic Computation, 12:397--414, 1991.

Charles C. Sims.
Computation with Finitely Presented Groups.
Cambridge, 1994.

Derek F. Holt.
The warwick automatic groups software.
In Proceedings of DIMACS Conference on Computational Group Theory, Rutgers, March 1994

A more informal, easily readable description can be found in Geoff Smith’s “Topics in Group Theory”.


---

