upload.bbl
\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Bachmair and Dershowitz}{1988}]{BD88:jsc}
Leo Bachmair and Nachum Dershowitz.
\newblock Critical pair criteria for completion.
\newblock {\em J. Symbolic Computation}, 6(1):1--18, 1988.

\bibitem[\protect\citeauthoryear{Bachmair and Dershowitz}{1994}]{BD-94}
Leo Bachmair and Nachum Dershowitz.
\newblock Equational inference, canonical proofs, and proof orderings.
\newblock {\em J. of the Association for Computing Machinery}, 41(2):236--276,
  1994.

\bibitem[\protect\citeauthoryear{Bachmair and Ganzinger}{2001}]{BG01}
Leo Bachmair and Harald Ganzinger.
\newblock Resolution theorem proving.
\newblock In A.~Robinson and A.~Voronkov, editors, {\em Handbook of Automated
  Reasoning}, volume~I, chapter~2, pages 19--99. Elsevier Science, 2001.

\bibitem[\protect\citeauthoryear{Dershowitz and Kirchner}{2003a}]{DK}
Nachum Dershowitz and Claude Kirchner.
\newblock Abstract canonical inference systems.
\newblock Technical report, LORIA, 2003.
\newblock In preparation. Latest draft at {\tt
  http://www.loria.fr/$\sim$ckirchne/acis.ps}.

\bibitem[\protect\citeauthoryear{Dershowitz and Kirchner}{2003b}]{DK03:lics}
Nachum Dershowitz and Claude Kirchner.
\newblock Abstract saturation-based inference.
\newblock In {\em Proceedings of the 18th Annual Symposium on Logic in Computer
  Science}, Ottawa, 2003. IEEE Computer Society Press.

\bibitem[\protect\citeauthoryear{Dershowitz and
  Plaisted}{2001}]{DershowitzPlaisted:HandbookAR:rewriting:2001}
Nachum Dershowitz and David~A. Plaisted.
\newblock Rewriting.
\newblock In A.~Robinson and A.~Voronkov, editors, {\em Handbook of Automated
  Reasoning}, volume~I, chapter~9, pages 535--610. Elsevier Science, 2001.

\bibitem[\protect\citeauthoryear{Kapur \bgroup \em et al.\egroup
  }{1988}]{KMN88:jsc}
Deepak Kapur, David~R. Musser, and Paliath Narendran.
\newblock Only prime superpositions need be considered for the {Knuth-Bendix}
  procedure.
\newblock {\em J. Symbolic Computation}, 4:19--36, August 1988.

\bibitem[\protect\citeauthoryear{Nieuwenhuis and Rubio}{2001}]{NR01}
Robert Nieuwenhuis and Albert Rubio.
\newblock Paramodulation-based theorem proving.
\newblock In A.~Robinson and A.~Voronkov, editors, {\em Handbook of Automated
  Reasoning}, volume~I, chapter~7, pages 371--443. Elsevier Science, 2001.

\bibitem[\protect\citeauthoryear{Rusinowitch}{1989}]{Rusi}
Micha{\"e}l Rusinowitch.
\newblock {\em D{\'e}monstration Automatique: Techniques de R{\'e\'e}criture}.
\newblock Science Informatique. InterEditions, Paris, 1989.

\end{thebibliography}
