# Research

**Publications**

Complete list of publications on Google Scholar

**Proof Orderings**

Proof orderings and their application to equational theories was the core topic of my Ph.D. thesis [1]. The proof technique was introduced in a LICS '86 paper [2] that was subsequently selected for the IEEE LICS 2006 Test-of-Time Award. A journal version [3] that also included material from a LICS '88 paper [4] appeared with considerable delay. The monograph [6] contains the most detailed exposition of the technique and illustrates its application to various proof methods.

- L. Bachmair,
*Proof Methods for Equational Theories,*Ph.D. diss., University of Illinois, Urbana-Champaign, 1987. - L. Bachmair, N. Dershowitz, and J. Hsiang,
*Orderings for equational proofs.*In Proc. First Annual Symp. on Logic in Computer Science, pp. 346-357, IEEE Computer Science Society Press, 1986. - L. Bachmair and N. Dershowitz,
*Equational inference, canonical proofs, and proof orderings,*J. ACM 41 (1994):236-276. - L. Bachmair,
*Proof by consistency in equational theories.*In Proc. Third Annual Symp. on Logic in Computer Science, pp. 228-233, IEEE Computer Science Society Press, 1988. - L. Bachmair and N. Dershowitz,
*Completion for rewriting modulo a congruence,*Theor. Comp. Sci. 67 (1989):173-201. - L. Bachmair,
*Canonical Equational Proofs,*Birkhäuser, Boston, 1991.

**Superposition Calculus**

I developed the superposition calculus jointly with Harald Ganzinger. This work has been called "revolutionary" [LNCS 7797, p. 4] in that it combined known concepts with new ideas to develop a powerful, yet flexible proof method for automated deduction. The first results were presented at CTRS '90 [1], though the first publication appeared in the CADE '90 proceedings [2]. The latter paper was selected for the 2019 Thoralf Skolem Award. A journal version of the key results appeared in 1994 [3]. The model generation technique described in these and other papers proved to be very successful and allowed researchers in automated deduction "to make tremendous progress in all directions ever since, to a point that people did not feel the need to look for new methods" [LNCS 7797, p. 91]. The LICS '93 paper [4] was selected for the ACM/IEEE LICS 2013 Test-of-Time Award. A planned book on automated deduction was never completed, but there are two extensive survey papers, [5] and [6].

- L. Bachmair and H. Ganzinger,
*Completion of first-order clauses with equality by strict superposition.*In Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, pp. 162-181, Lecture Notes in Computer Science 516, Springer-Verlag, Berlin, 1991. - L. Bachmair and H. Ganzinger,
*On restrictions of ordered paramodulation with simplification.*In Proc. 10th Int. Conf. on Automated Deduction, pp. 427-441, Lecture Notes in Artificial Intelligence 449, Springer-Verlag, Berlin, 1990. - L. Bachmair and H. Ganzinger,
*Rewrite-based equational theorem proving with selection and simplification,*J. Logic and Computation 4 (1994): 217-247. - L. Bachmair, H. Ganzinger, and U. Waldmann,
*Set constraints are the monadic class.*In Proc. Eigth Annual IEEE Symp. on Logic in Computer Science, pp. 75-83, IEEE Computer Science Society Press, 1993. - L. Bachmair and H. Ganzinger,
*Equational Reasoning in Saturation-Based Theorem Proving,*Chapter 11 of vol. I of*Automated Deduction - A Basis for Applications,*W. Bibel and P. Schmitt, eds., pp. 353-397, Kluwer, 1998. - L. Bachmair and H. Ganzinger,
*Resolution Theorem Proving,*Chapter 2 of vol. I of*Handbook of Automated Reasoning,*J.A. Robinson and A. Voronkov, eds., pp. 19-99, Elsevier, 2001.