| 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) |
