http://www.springerlink.com/content/u222753gl333221p/; Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedu... View more
 M. Aiguier and D. Bahrami. Structures for abstract rewriting. Journal of Automated Reasoning, 2006. To appear.
 F. Baader and T. Nipkow. Term Rewriting and all That. Cambridge University Press, 1998.
 L. Bachmair. Proof methods for equational theories. PhD thesis, University of Illinois, Urbana-Champaign, (Ill., USA), 1987. Revised version, August 1988.
 L. Bachmair and N. Dershowitz. Equational inference, canonical proofs, and proof orderings. Journal of Association for Computing Machinery, 41(2):236-276, 1994.
 L. Bachmair and H. Ganzinger. Resolution theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 2, pages 19-99. Elsevier Science, 2001.
 M. P. Bonacina and N. Dershowitz. Abstract Canonical Inference. ACM Transactions on Computational Logic, 2006. To appear.
 M. P. Bonacina and J. Hsiang. On rewrite programs: semantics and relationship with Prolog. Journal of Logic Programming, 14(1 & 2):155-180, October 1992.
 P. Borovansky, C. Kirchner, H. Kirchner, and P.-E. Moreau. ELAN from a rewriting logic point of view. Theoretical Computer Science, 2(285):155-185, July 2002.
 B. Buchberger. An algorithm for finding a basis for the residue class ring of a zero-dimensional polynomial ideal. PhD thesis, University of Inssbruck (Austria), 1965. (in German).
 B. Buchberger. A critical-pair/completion algorithm for finitely generated ideals in rings. In E. B¨orger, G. Hasenjaeger, and D. R¨odding, editors, Proceedings of Logic and Machines: Decision problems and Complexity, volume 171 of Lecture Notes in Computer Science, pages 137-161. Springer-Verlag, 1983.