Your search returned the following 20 documents:

20. Resolution Theorem Proving
    Leo Bachmair and Harald Ganzinger
    In: Handbook of Automated Reasoning, 2001, 19-99
    [PS: Download: 2001Handbook.ps.gz]
    
19. 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
    
18. Equational Reasoning in Saturation-Based Theorem Proving
    Leo Bachmair and Harald Ganzinger
    In: Automated Deduction: A Basis for Applications, 1998, 353-397
    
17. Ordered Chaining Calculi for First-Order Theories of Transitive Relations
    Leo Bachmair and Harald Ganzinger
    Journal of the ACM 45 (6): 1007-1049, 1998. Note: Revised Version of MPI-I-95-2-009.
    
16. 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
    
15. Associative-Commutative Superposition
    Leo Bachmair and Harald Ganzinger
    In: Proceedings of the 4th International Workshop on Conditional and Typed Rewrite Systems (CTRS-94), Jerusalem, Israel, July, 13-15, 1994, 1995, 1-14. Note: Revised version of MPI-I-93-267, 1993
    
14. Basic Paramodulation
    Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder
    Information and Computation 121 (2): 172-192, 1995. Note: Revised version of TR MPI-I-93-236, 1993
    
13. Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings
    Leo Bachmair, Harald Ganzinger, and Jürgen Stuber
    In: Recent Trends in Data Type Specification. 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May/June 1994, 1995, 1-29
    
12. Buchberger's algorithm: a constraint-based completion procedure
    Leo Bachmair and Harald Ganzinger
    In: Proceedings of the 1st International Conference on Constraints in Computational Logics (CCL'94), Munich, Germany, September 7-9, 1994, 1994, 285-301
    
11. Ordered Chaining for Total Orderings
    Leo Bachmair and Harald Ganzinger
    In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), Nancy, France, June 26 - July 1, 1994, 1994, 435-450. Note: Full version available as Research Report MPI-I-93-250, 1993
    
10. Refutational Theorem Proving for Hierarchic First-Order Theories
    Leo Bachmair, Harald Ganzinger, and Uwe Waldmann
    Applicable Algebra in Engineering, Communication and Computing (AAECC) 5 (3/4): 193-212, 1994. Note: Earlier Version: Theorem Proving for Hierarchic First-Order Theories, in Giorgio Levi and H{\'e}l{\`e}ne Kirchner, editors, {\em Algebraic and Logic Programming, Third International Conference}, LNCS 632, pages 420--434, Volterra, Italy, September 2--4, 1992, Springer-Verlag
    
9. Rewrite-based equational theorem proving with selection and simplification
   Leo Bachmair and Harald Ganzinger
   Journal of Logic and Computation 4 (3): 217-247, 1994. Note: Revised version of Technical Report MPI-I-91-208, 1991
   
8. Rewrite Techniques for Transitive Relations
   Leo Bachmair and Harald Ganzinger
   In: Proceedings of the 9th IEEE Symposium on Logic in Computer Science, Paris, France, 1994, 384-393. Note: Full version available as Technical Report MPI-I-93-249
   
7. Set Constraints are the Monadic Class
   Leo Bachmair, Harald Ganzinger, and Uwe Waldmann
   In: Eighth Annual IEEE Symposium on Logic in Computer Science, Montreal, Canada, June 19-23, 1993, 1993, 75-83
   
6. Superposition with simplification as a decision procedure for the monadic class with equality
   Leo Bachmair, Harald Ganzinger, and Uwe Waldmann
   In: Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, Brno, Czech Republic, August 24-27, 1993, 1993, 83-96. Note: Revised version of Technical Report MPI-I-93-204
   
5. Basic Paramodulation and Superposition
   Leo Bachmair, Harald Ganzinger, Christopher Lynch, and Wayne Snyder
   In: Proceedings of the 11th International Conference on Automated Deduction (CADE-11), Saratoga Springs, NY, 1992, 1992, 462-476
   
4. Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria
   Leo Bachmair and Harald Ganzinger
   In: Logic Programming and Automated Reasoning, St.\ Petersburg, Russia, 1992, 1992, 273-284
   
3. 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)
   
2. Completion of first-order clauses with equality by strict superposition
   Leo Bachmair and Harald Ganzinger
   In: Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting, Montreal, Canada, 1990, 1991, 162-180
   
1. Perfect model semantics for logic programs with equality
   Leo Bachmair and Harald Ganzinger
   In: Proceedings International Conference on Logic Programming '91, Paris, France, 1991, 1991, 645-659