Does anyone knows of references that precisely spell out the connection between the unification algorithm and Gaussian elimination? I'm particularly interested in the relationship between triangular substitutions and LU decompositions.

Wayne Snyder and Jean Gallier mention this analogy in passing in their paper, Higher-Order Unification Revisited: Complete Sets of Transformations.

  • 7
    $\begingroup$ 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. $\endgroup$ Commented Aug 16, 2012 at 14:42
  • 1
    $\begingroup$ 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? $\endgroup$
    – vzn
    Commented Aug 16, 2012 at 22:08
  • 5
    $\begingroup$ 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? $\endgroup$
    – Vijay D
    Commented Aug 18, 2012 at 23:53
  • $\begingroup$ @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. $\endgroup$ Commented Aug 20, 2012 at 5:27

1 Answer 1


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, Bruno Buchberger, 1987
  2. Canonical Reduction Systems in Symbolic Mathematics, Franz Winkler. Springer Link

Let me know if you find better references.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.