| # |  | Year | Author(s) [non member] | Editor(s) [non member] | | Title | Type | |
|---|
| 1 |
 | Baader, Franz |
| |
| 9 |
| |
| 1 |
| Bachem, A. (ed.) |
| |
| 20 |
| |
| | 2001 | Bachmair, Leo
Ganzinger, Harald | [Robinson, J. A.]
[Voronkov, A.] |  | Resolution Theorem Proving
In: Handbook of Automated Reasoning, 19-99 | Part of a Book | |
| | 1998 | [Bachmair, Leo]
Ganzinger, Harald | | | Ordered Chaining Calculi for First-Order Theories of Transitive Relations
In: Journal of the ACM [45], 1007-1049 | Journal Article | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald | Bibel, Wolfgang
Schmitt, Peter H. | | Equational Reasoning in Saturation-Based Theorem Proving
In: Automated Deduction: A Basis for Applications, 353-397 | Part of a Book | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald | Kirchner, Claude
Kirchner, Hélène | | Strict Basic Superposition
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 160-174 | Proceedings Article | |
| | 1998 | Bachmair, Leo
Ganzinger, Harald
Voronkov, Andrei | Kirchner, Claude
Kirchner, Hélène | | Elimination of Equality via Transformation with Ordering Constraints
In: Proceedings of the 15th International Conference on Automated Deduction (CADE-98), 175-190 | Proceedings Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald | Dershowitz, N.
Lindenstrauss, N. | | Associative-Commutative Superposition
In: Proceedings of the 4th International Workshop on Conditional and Typed Rewrite Systems (CTRS-94), 1-14 | Proceedings Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald
[Lynch, Christopher]
[Snyder, Wayne] | | | Basic Paramodulation
In: Information and Computation [121], 172-192 | Journal Article | |
| | 1995 | Bachmair, Leo
Ganzinger, Harald
Stuber, Jürgen | Astesiano, Egidio
Reggio, Gianna
Tarlecki, Andrzej | | Combining Algebra and Universal Algebra in First-Order Theorem Proving: The Case of Commutative Rings
In: Recent Trends in Data Type Specification. 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, 1-29 | Proceedings Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | | | Rewrite-based equational theorem proving with selection and simplification
In: Journal of Logic and Computation [4], 217-247 | Journal Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | | | Rewrite Techniques for Transitive Relations
In: Proceedings of the 9th IEEE Symposium on Logic in Computer Science, 384-393 | Proceedings Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | Bundy, Alan | | Ordered Chaining for Total Orderings
In: Proceedings of the 12th International Conference on Automated Deduction (CADE-12), 435-450 | Proceedings Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald | Jouannaud, Jean-Pierre | | Buchberger's algorithm: a constraint-based completion procedure
In: Proceedings of the 1st International Conference on Constraints in Computational Logics (CCL'94), 285-301 | Proceedings Article | |
| | 1994 | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | | | Refutational Theorem Proving for Hierarchic First-Order Theories
In: Applicable Algebra in Engineering, Communication and Computing (AAECC) [5], 193-212 | Journal Article | |
| | 1993 | [Bachmair, Leo]
Ganzinger, Harald
Waldmann, Uwe | | | Set Constraints are the Monadic Class
In: Eighth Annual IEEE Symposium on Logic in Computer Science, 75-83 | Proceedings Article | |
| | 1993 | [Bachmair, Leo]
Ganzinger, Harald
Waldmann, Uwe | [Gottlob, Georg]
[Leitsch, Alexander]
[Mundici, Daniele] | | Superposition with simplification as a decision procedure for the monadic class with equality
In: Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, 83-96 | Proceedings Article | |
| | 1992 | Bachmair, Leo
Ganzinger, Harald
Lynch, Christopher
Snyder, Wayne | Kapur, D. | | Basic Paramodulation and Superposition
In: Proceedings of the 11th International Conference on Automated Deduction (CADE-11), 462-476 | Proceedings Article | |
| | 1992 | Bachmair, Leo
Ganzinger, Harald | Voronkov, A. | | Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria
In: Logic Programming and Automated Reasoning, 273-284 | Proceedings Article | |
| | 1992 | Bachmair, Leo
Ganzinger, Harald
Waldmann, Uwe | Kirchner, Hélène
Levi, G. | | Theorem proving for hierarchic first-order theories
In: Algebraic and Logic Programming, 420-434 | Proceedings Article | |
| | 1991 | Bachmair, Leo
Ganzinger, Harald | | | Perfect model semantics for logic programs with equality
In: Proceedings International Conference on Logic Programming '91, 645-659 | Proceedings Article | |
| | 1991 | Bachmair, Leo
Ganzinger, Harald | Kaplan, St.
Okada, M. | | Completion of first-order clauses with equality by strict superposition
In: Proceedings of the 2nd International Workshop on Conditional and Typed Rewriting, 162-180 | Proceedings Article | |
| 1 |
| Bachmair, Leo (ed.) |
| |
| 1 |
| |
| 3 |
| Backes, Werner |
| |
| 3 |
| |
| 1 |
| Balbiani, Philippe (ed.) |
| |
| 1 |
| |
