| 2005 | ||
|---|---|---|
| 48 | EE | Paul Agron, Leo Bachmair, Frank Nielsen: A Visual Interactive Framework for Formal Derivation. International Conference on Computational Science (1) 2005: 1019-1026 |
| 2004 | ||
| 47 | EE | Christelle Scharff, Leo Bachmair: On the Combination of Congruence Closure and Completion. AISC 2004: 103-117 |
| 2003 | ||
| 46 | EE | Leo Bachmair, Ashish Tiwari, Laurent Vigneron: Abstract Congruence Closure. J. Autom. Reasoning 31(2): 129-168 (2003) |
| 2001 | ||
| 45 | Leo Bachmair, Harald Ganzinger: Resolution Theorem Proving. Handbook of Automated Reasoning 2001: 19-99 | |
| 2000 | ||
| 44 | Leo Bachmair: Rewriting Techniques and Applications, 11th International Conference, RTA 2000, Norwich, UK, July 10-12, 2000, Proceedings Springer 2000 | |
| 43 | Ashish Tiwari, Leo Bachmair, Harald Rueß: Rigid E-Unification Revisited. CADE 2000: 220-234 | |
| 42 | Leo Bachmair, Ashish Tiwari: Abstract Congruence Closure and Specializations. CADE 2000: 64-78 | |
| 41 | Leo Bachmair, I. V. Ramakrishnan, Ashish Tiwari, Laurent Vigneron: Congruence Closure Modulo Associativity and Commutativity. FroCos 2000: 245-259 | |
| 1999 | ||
| 40 | EE | Leo Bachmair, C. R. Ramakrishnan, I. V. Ramakrishnan, Ashish Tiwari: Normalization via Rewrite Closures. RTA 1999: 190-204 |
| 1998 | ||
| 39 | EE | Leo Bachmair, Harald Ganzinger: Strict Basic Superposition. CADE 1998: 160-174 |
| 38 | EE | Leo Bachmair, Harald Ganzinger, Andrei Voronkov: Elimination of Equality via Transformation with Ordering Constraints. CADE 1998: 175-190 |
| 37 | Maxim Lifantsev, Leo Bachmair: An LPO-based Termination Ordering for Higher-Order Terms without lambda-abstraction. TPHOLs 1998: 277-293 | |
| 36 | EE | Leo Bachmair, Harald Ganzinger: Ordered Chaining Calculi for First-Order Theories of Transitive Relations. J. ACM 45(6): 1007-1049 (1998) |
| 1997 | ||
| 35 | Leo Bachmair: Paramodulation, Superposition, and Simplification. Kurt Gödel Colloquium 1997: 1-3 | |
| 34 | Leo Bachmair, Ashish Tiwari: D-Bases for Polynomial Ideals over Commutative Noetherian Rings. RTA 1997: 113-127 | |
| 1996 | ||
| 33 | Leo Bachmair, Ta Chen, C. R. Ramakrishnan, I. V. Ramakrishnan: Subsumption Algorithms Based on Search Trees. CAAP 1996: 135-148 | |
| 1995 | ||
| 32 | Leo Bachmair, Ta Chen, I. V. Ramakrishnan, Siva Anantharaman, Jacques Chabin: Experiments with Associative-Commutative Discrimination Nets. IJCAI 1995: 348-355 | |
| 31 | Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder: Basic Paramodulation Inf. Comput. 121(2): 172-192 (1995) | |
| 1994 | ||
| 30 | Leo Bachmair, Harald Ganzinger: Ordered Chaining for Total Orderings. CADE 1994: 435-450 | |
| 29 | Leo Bachmair, Harald Ganzinger: Buchberger's Algorithm: A Constraint-Based Completion Procedure. CCL 1994: 285-301 | |
| 28 | 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 | |
| 27 | Leo Bachmair, Harald Ganzinger: Associative-Commutative Superposition. CTRS 1994: 1-14 | |
| 26 | Leo Bachmair, Harald Ganzinger: Rewrite Techniques for Transitive Relations LICS 1994: 384-393 | |
| 25 | Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Refutational Theorem Proving for Hierachic First-Order Theories. Appl. Algebra Eng. Commun. Comput. 5: 193-212 (1994) | |
| 24 | EE | Leo Bachmair, Nachum Dershowitz: Equational Inference, Canonical Proofs, and Proof Orderings. J. ACM 41(2): 236-276 (1994) |
| 23 | Leo Bachmair, Harald Ganzinger: Rewrite-Based Equational Theorem Proving with Selection and Simplification. J. Log. Comput. 4(3): 217-247 (1994) | |
| 1993 | ||
| 22 | Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality. Kurt Gödel Colloquium 1993: 83-96 | |
| 21 | Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Set Constraints are the Monadic Class LICS 1993: 75-83 | |
| 20 | Leo Bachmair: Rewrite Techniques in Theorem Proving (Abstract). RTA 1993: 1 | |
| 19 | Leo Bachmair, Ta Chen, I. V. Ramakrishnan: Associative-Commutative Discrimination Nets. TAPSOFT 1993: 61-74 | |
| 1992 | ||
| 18 | Leo Bachmair, Harald Ganzinger, Uwe Waldmann: Theorem Proving for Hierarchic First-Order Theories. ALP 1992: 420-434 | |
| 17 | Leo Bachmair, Harald Ganzinger, Christopher Lynch, Wayne Snyder: Basic Paramodulation and Superposition. CADE 1992: 462-476 | |
| 16 | Leo Bachmair, Harald Ganzinger: Non-Clausal Resolution and Superposition with Selection and Redundancy Criteria. LPAR 1992: 273-284 | |
| 15 | Leo Bachmair: Associative-Commutative Reduction Orderings. Inf. Process. Lett. 43(1): 21-27 (1992) | |
| 1991 | ||
| 14 | Leo Bachmair, Harald Ganzinger: Perfect Model Semantics for Logic Programs with Equality. ICLP 1991: 645-659 | |
| 1990 | ||
| 13 | Leo Bachmair, Harald Ganzinger: On Restrictions of Ordered Paramodulation with Simplification. CADE 1990: 427-441 | |
| 12 | Leo Bachmair, Harald Ganzinger: Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract). CTRS 1990: 162-180 | |
| 1989 | ||
| 11 | Leo Bachmair: Proof Normalization for Resolution and Paramodulation. RTA 1989: 15-28 | |
| 10 | Leo Bachmair, Nachum Dershowitz: Completion for Rewriting Modulo a Congruence. Theor. Comput. Sci. 67(2&3): 173-201 (1989) | |
| 1988 | ||
| 9 | Leo Bachmair: Proof by Consistency in Equational Theories LICS 1988: 228-233 | |
| 8 | Leo Bachmair, Nachum Dershowitz: Critical Pair Criteria for Completion. J. Symb. Comput. 6(1): 1-18 (1988) | |
| 1987 | ||
| 7 | Leo Bachmair, Nachum Dershowitz: A critical pair criterion for completion modulo a congruence. EUROCAL 1987: 452-453 | |
| 6 | Leo Bachmair, Nachum Dershowitz: Inference Rules for Rewrite-Based First-Order Theorem Proving LICS 1987: 331-337 | |
| 5 | Leo Bachmair, Nachum Dershowitz: Completion for Rewriting Modulo a Congruence. RTA 1987: 192-203 | |
| 1986 | ||
| 4 | Leo Bachmair, Nachum Dershowitz: Commutation, Transformation, and Termination. CADE 1986: 5-20 | |
| 3 | Leo Bachmair, Nachum Dershowitz, Jieh Hsiang: Orderings for Equational Proofs LICS 1986: 346-357 | |
| 1985 | ||
| 2 | Leo Bachmair, David A. Plaisted: Associative Path Orderings. RTA 1985: 241-254 | |
| 1 | Leo Bachmair, David A. Plaisted: Termination Orderings for Associative-Commutative Rewriting Systems. J. Symb. Comput. 1(4): 329-349 (1985) | |
| 1 | Paul Agron | [48] |
| 2 | Siva Anantharaman | [32] |
| 3 | Jacques Chabin | [32] |
| 4 | Ta Chen | [19] [32] [33] |
| 5 | Nachum Dershowitz | [3] [4] [5] [6] [7] [8] [10] [24] |
| 6 | Harald Ganzinger | [12] [13] [14] [16] [17] [18] [21] [22] [23] [25] [26] [27] [28] [29] [30] [31] [36] [38] [39] [45] |
| 7 | Jieh Hsiang | [3] |
| 8 | Maxim Lifantsev | [37] |
| 9 | Christopher Lynch | [17] [31] |
| 10 | Frank Nielsen | [48] |
| 11 | David A. Plaisted | [1] [2] |
| 12 | C. R. Ramakrishnan | [33] [40] |
| 13 | I. V. Ramakrishnan | [19] [32] [33] [40] [41] |
| 14 | Harald Rueß | [43] |
| 15 | Christelle Scharff | [47] |
| 16 | Wayne Snyder | [17] [31] |
| 17 | Jürgen Stuber | [28] |
| 18 | Ashish Tiwari | [34] [40] [41] [42] [43] [46] |
| 19 | Laurent Vigneron | [41] [46] |
| 20 | Andrei Voronkov | [38] |
| 21 | Uwe Waldmann | [18] [21] [22] [25] |
Colors in the list of coauthors