# Selected Publications

#### Canonical Equational Proofs

*L. Bachmair*

Birkhäuser, Boston, 1991.

#### Completion without Failure

*L. Bachmair, N. Dershowitz, and D. A. Plaisted*

Chapter 1 of Vol. II of Resolution of Equations in Algebraic Structures, H. Ait-Kaci and M. Nivat, eds., Academic Press, 1989.

#### Equational Reasoning in Saturation-Based Theorem Proving

*L. Bachmair and H. Ganzinger*

Chapter 11 of Vol. I of Automated Deduction - A Basis for Applications, W. Bibel and P. Schmitt, eds., Kluwer, 1998.

#### Resolution Theorem Proving

*L. Bachmair and H. Ganzinger*

Chapter 2 of Handbook of Automated Reasoning, J.A. Robinson and A. Voronkov, eds., Elsevier, 2001.

#### Equational Inference, Canonical Proofs, and Proof Orderings

*L. Bachmair and N. Dershowitz*

J. ACM 41 (1994):236-276.

#### Rewrite-Based Equational Theorem Proving with Selection and Simplification

*L. Bachmair and H. Ganzinger*

J. Logic and Computation 4 (1994): 217-247.

#### Basic Paramodulation

*L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder*

Information and Computation 121 (1995):172-192.

#### Ordered Chaining Calculi for First-Order Theories of Binary Relations

*L. Bachmair and H. Ganzinger*

J. ACM 46 (1999):1007-1049.

#### Abstract Congruence Closure

*L. Bachmair, A. Tiwari, and L. Vigneron*

J. Automated Reasoning 31 (2003):129--168.

#### Orderings for Equational Proofs

*L. Bachmair, N. Dershowitz, and J. Hsiang*

In Proc. First Annual Symp. on Logic in Computer Science, pp. 346--357, IEEE Computer Science Society Press, 1986.

**IEEE LICS 2006 Test-of-Time Award**

#### Commutation, transformation, and termination

*L. Bachmair and N. Dershowitz*

In Proc. Eighth Int. Conf. on Automated Deduction,
pp. 5--20,
Lecture Notes in Computer Science 230,
Springer-Verlag, Berlin, 1986.

**2015 CADE Thoralf Skolem Award**

#### Proof by Consistency in Equational Theories

*L. Bachmair*

In Proc. Third Annual Symp. on Logic in Computer Science, pp. 228-233, IEEE Computer Science Society Press, 1988.

#### Set Constraints are the Monadic Class

*L. Bachmair, H. Ganzinger, and U. Waldmann*

In Proc. Eigth Annual Symp. on Logic in Computer Science, pp. 75-83, IEEE Computer Science Society Press, 1993.

**IEEE LICS 2013 Test-of-Time Award**