Unification and Gaussian Elimination 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.
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.

History and basic features of the critical-pair/completion procedure, Bruno Buchberger, 1987
Canonical Reduction Systems in Symbolic Mathematics, Franz Winkler. Springer Link

Let me know if you find better references.