Leo Bachmair, Harald Ganzinger, Jürgen Stuber: Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings. COMPASS/ADT 1994: 1-29