Your search returned the following 7 documents:

7. Elimination of Equality via Transformation with Ordering Constraints
   Leo Bachmair, Harald Ganzinger, and Andrei Voronkov
   In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), Lindau, Germany, July, 5-10 1998, 1998, 175-190. Note: Short version of MPI-I-97-2-012
   
6. On Generating Small Clause Normal Forms
   Andreas Nonnengart, Georg Rock, and Christoph Weidenbach
   In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), Lindau, Germany, July, 5-10 1998, 1998, 397-411
   
5. Strict Basic Superposition
   Leo Bachmair and Harald Ganzinger
   In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), Lindau, Germany, July, 5-10 1998, 1998, 160-174
   
4. Superposition for Divisible Torsion-Free Abelian Groups
   Uwe Waldmann
   In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), Lindau, Germany, July, 5 - 10 1998, 1998, 144-159
   
3. A Goal Oriented Strategy Based on Completion
   Rolf Socher-Ambrosius
   In: Proc.~3rd Intern.~Conference on Algebraic and Logic Programming, Volterra, Italy, 1992, 435-445. Note: Also available as Research Report MPI-I-92-206
   
2. Incremental Rewriting in Narrowing Derivations
   Michael Hanus
   In: Proceedings of the 3rd International Conference on Algebraic and Logic Programming (ALP-92), Volterra, Italy, September, 2-4, 1992, 228-243
   
1. Theorem proving for hierarchic first-order theories
   Leo Bachmair, Harald Ganzinger, and Uwe Waldmann
   In: Algebraic and Logic Programming, 1992, 420-434. Note: Revised version in AAECC, vol.\ 5, number 3/4, pp.\ 193--212, 1994)