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.