`Travelled to:`

1 × Canada

1 × Germany

1 × Spain

1 × United Kingdom

2 × Italy

5 × France

5 × USA

`Collaborated with:`

H.Ganzinger N.Dershowitz A.Tiwari ∅ I.V.Ramakrishnan D.A.Plaisted H.Rueß A.Voronkov U.Waldmann J.Hsiang T.Chen C.R.Ramakrishnan C.Lynch W.Snyder

`Talks about:`

order (8) rewrit (5) paramodul (3) theorem (3) commut (3) prove (3) proof (3) superposit (2) transform (2) congruenc (2)

## Person: Leo Bachmair

### DBLP: Bachmair:Leo

### Facilitated 1 volumes:

### Contributed to:

### Wrote 21 papers:

- CADE-2000-BachmairT #congruence
- Abstract Congruence Closure and Specializations (LB, AT), pp. 64–78.
- CADE-2000-TiwariBR #revisited
- Rigid E-Unification Revisited (AT, LB, HR), pp. 220–234.
- RTA-1999-BachmairRRT #normalisation #term rewriting
- Normalization via Rewrite Closures (LB, CRR, IVR, AT), pp. 190–204.
- CADE-1998-BachmairG #strict
- Strict Basic Superposition (LB, HG), pp. 160–174.
- CADE-1998-BachmairGV #constraints #similarity
- Elimination of Equality via Transformation with Ordering Constraints (LB, HG, AV), pp. 175–190.
- RTA-1997-BachmairT #commutative #polynomial
- D-Bases for Polynomial Ideals over Commutative Noetherian Rings (LB, AT), pp. 113–127.
- CADE-1994-BachmairG #order
- Ordered Chaining for Total Orderings (LB, HG), pp. 435–450.
- LICS-1994-BachmairG #transitive
- Rewrite Techniques for Transitive Relations (LB, HG), pp. 384–393.
- RTA-1993-Bachmair #proving #theorem proving
- Rewrite Techniques in Theorem Proving (LB), p. 1.
- ALP-1992-BachmairGW #first-order #proving #theorem proving
- Theorem Proving for Hierarchic First-Order Theories (LB, HG, UW), pp. 420–434.
- CADE-1992-BachmairGLS
- Basic Paramodulation and Superposition (LB, HG, CL, WS), pp. 462–476.
- ICLP-1991-BachmairG #logic programming #semantics #similarity #source code
- Perfect Model Semantics for Logic Programs with Equality (LB, HG), pp. 645–659.
- CADE-1990-BachmairG #on the #order #strict
- On Restrictions of Ordered Paramodulation with Simplification (LB, HG), pp. 427–441.
- RTA-1989-Bachmair #normalisation #proving
- Proof Normalization for Resolution and Paramodulation (LB), pp. 15–28.
- LICS-1988-Bachmair #consistency #equation #proving
- Proof by Consistency in Equational Theories (LB), pp. 228–233.
- LICS-1987-BachmairD #first-order #proving #theorem proving
- Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.
- RTA-1987-BachmairD #congruence
- Completion for Rewriting Modulo a Congruence (LB, ND), pp. 192–203.
- CADE-1986-BachmairD #termination
- Commutation, Transformation, and Termination (LB, ND), pp. 5–20.
- LICS-1986-BachmairDH #equation #order #proving
- Orderings for Equational Proofs (LB, ND, JH), pp. 346–357.
- RTA-1985-BachmairP #order
- Associative Path Orderings (LB, DAP), pp. 241–254.
- TAPSOFT-1993-BachmairCR #commutative
- Associative-Commutative Discrimination Nets (LB, TC, IVR), pp. 61–74.