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