<p>I don't consider this an answer. I'm abusing the answer box to pretty print a comment.</p>
<p>There is a strict sense in which Euclid's GCD algorithm, Gaussian elimination, Buchberger's algorithm and Knuth-Bendix form a strict sequence of generalisations and are all instances of what is called a <em>completion algorithm</em>. There is also a close relationship between these algorithms and resolution in logic. I do not know a good reference for this but I have seen the fact mentioned very often. These might help.</p>
<ol>
<li><a href="http://www.risc.jku.at/publications/download/risc_353/1987-04-00-A.pdf" rel="noreferrer">History and basic features of the critical-pair/completion procedure</a>, Bruno Buchberger, 1987</li>
<li><a href="http://www.risc.jku.at/education/courses/ss2011/rw/1-intro.pdf" rel="noreferrer">Canonical Reduction Systems in Symbolic Mathematics</a>, Franz Winkler. <a href="http://www.springerlink.com/content/w37631426j273383/" rel="noreferrer">Springer Link</a></li>
</ol>
<p>Let me know if you find better references.</p>

CC BY-SA 3.0
2012-08-25T05:24:46.283Z
2012-08-25T10:21:55.003Z
2020-06-17T09:38:08.363Z
Vijay D
<p>Does anyone knows of references that precisely spell out the connection between the <a href="http://en.wikipedia.org/wiki/Unification_%28computer_science%29">unification algorithm</a> and Gaussian elimination? I'm particularly interested in the relationship between <a href="http://www.nicta.com.au/pub?doc=3724">triangular substitutions</a> and LU decompositions. </p>

<p>Wayne Snyder and Jean Gallier mention this analogy in passing in their paper, <a href="http://cifo.in/uploads/Higher%20order%20unification%20revisited.pdf"><em>Higher-Order Unification Revisited: Complete Sets of Transformations</em></a>. </p>

CC BY-SA 3.0
2012-08-16T14:42:19.377Z
As a non-expert, I had never heard of the connection.  Some reference which mentions this connection would be a nice addition to the question.
Tsuyoshi Ito
CC BY-SA 3.0
2012-08-16T22:08:10.193Z
as they state in the paper p2, its mostly an analogy, "which in the higher order case breaks down". there is a demonstrable connection or analogy between resolution & gaussian elimination. close enough?
vzn
CC BY-SA 3.0
2012-08-18T23:53:46.160Z
I expect that you already know this: Euclid's algorithm, Gaussian elimination, Buchberger's algorithm for Grobner bases and Knuth-Bendix completion are supposed to form a strictly increasing sequence in terms of generality and method they use. If the precise maps between these methods is known, maybe you could derive the connection above?
Vijay D
CC BY-SA 3.0
2012-08-20T05:27:24.037Z
@VijayD: I didn't know that, actually! I know what Buchberger's algorithm does, but I don't know the algorithm itself, or anything at all about its relationship to Guassian elimination or KB completion.
Neel Krishnaswami
<reference-request><lo.logic>
Unification and Gaussian Elimination
Neel Krishnaswami
# Unification and Gaussian Elimination

(Asked by: username_0 on 2012-08-16)

Does anyone knows of references that precisely spell out the connection between the [unification algorithm](http://en.wikipedia.org/wiki/Unification_%28computer_science%29) and Gaussian elimination? I'm particularly interested in the relationship between [triangular substitutions](http://www.nicta.com.au/pub?doc=3724) and LU decompositions.

Wayne Snyder and Jean Gallier mention this analogy in passing in their paper, [*Higher-Order Unification Revisited: Complete Sets of Transformations*](http://cifo.in/uploads/Higher%20order%20unification%20revisited.pdf).

**Tags:** reference-request, lo.logic

> **Comments:**
> **username_1**: As a non-expert, I had never heard of the connection.  Some reference which mentions this connection would be a nice addition to the question.  
> **username_2**: as they state in the paper p2, its mostly an analogy, "which in the higher order case breaks down". there is a demonstrable connection or analogy between resolution & gaussian elimination. close enough?  
> **username_3**: I expect that you already know this: Euclid's algorithm, Gaussian elimination, Buchberger's algorithm for Grobner bases and Knuth-Bendix completion are supposed to form a strictly increasing sequence in terms of generality and method they use. If the precise maps between these methods is known, maybe you could derive the connection above?  
> **username_0**: @VijayD: I didn't know that, actually! I know what Buchberger's algorithm does, but I don't know the algorithm itself, or anything at all about its relationship to Guassian elimination or KB completion.  

---

## 1 answers

### Answer by username_3 on 2012-08-25. Score: 13

I don't consider this an answer. I'm abusing the answer box to pretty print a comment.

There is a strict sense in which Euclid's GCD algorithm, Gaussian elimination, Buchberger's algorithm and Knuth-Bendix form a strict sequence of generalisations and are all instances of what is called a *completion algorithm*. There is also a close relationship between these algorithms and resolution in logic. I do not know a good reference for this but I have seen the fact mentioned very often. These might help.

1. [History and basic features of the critical-pair/completion procedure](http://www.risc.jku.at/publications/download/risc_353/1987-04-00-A.pdf), Bruno Buchberger, 1987
2. [Canonical Reduction Systems in Symbolic Mathematics](http://www.risc.jku.at/education/courses/ss2011/rw/1-intro.pdf), Franz Winkler. [Springer Link](http://www.springerlink.com/content/w37631426j273383/)

Let me know if you find better references.


---

