\begin{thebibliography}{YALSM00}

\bibitem[ALS94a]{AvLo94}
J{\"u}rgen Avenhaus and Carlos Lor{\'\i}a-S{\'a}enz.
\newblock Higher order conditional rewriting and narrowing.
\newblock In J.-P. Jouannaud, editor, {\em Proc.~1st Int.\ Conf.\ on
  Constraints in Computational Logics (CCL'94)}, volume 845 of {\em Lecture
  Notes in Computer Science}, pages 269--284. Springer-Verlag, 1994.

\bibitem[ALS94b]{AvLo94a}
J{\"u}rgen Avenhaus and Carlos Lor{\'\i}a-S{\'a}enz.
\newblock On conditional rewrite systems with extra variables and deterministic
  logic programs.
\newblock In F.~Pfenning, editor, {\em Proc.~5th Int.~Conf.~on Logic
  Programming and Automated Reasoning}, volume 822 of {\em Lecture Notes in
  Artificial Intelligence}, pages 215--229, Kiev, Ukraine, July 1994.
  Springer-Verlag.

\bibitem[BD94]{BaDe94}
Leo Bachmair and Nachum Dershowitz.
\newblock Equational inference, canonical proofs, and proof orderings.
\newblock {\em Journal of the {ACM}}, 41(2):236--276, 1994.

\bibitem[BDJ78]{BrDaJo78}
Daniel Brand, {John A.} Darringer, and {William H.} {Joyner Jr}.
\newblock Completeness of conditional reductions.
\newblock Technical Report RC 7404, IBM Research Center, Yorktown Heights,
  N.Y., December 1978.

\bibitem[BGM87]{BoGiMo87}
{Pier Giorgio} Bosco, Elio Giovannetti, and Corrado Moiso.
\newblock Refined strategies for semantic unification.
\newblock In Hartmut Ehrig, {Robert A.} Kowalski, Giorgio Levi, and Ugo
  Montanari, editors, {\em TAPSOFT'87: Proceedings of the International Joint
  Conference on Theory and Practice of Software Development, Volume 2: Advanced
  Seminar on Foundations of Innovative Software Development II and Colloquium
  on Functional and Logic Programming and Specifications (CFLP)}, volume 250 of
  {\em Lecture Notes in Computer Science}, pages 276--290, Pisa, Italy, March
  1987. Springer-Verlag.

\bibitem[BGM88]{BoGiMo88}
{Pier Giorgio} Bosco, Elio Giovannetti, and Corrado Moiso.
\newblock Narrowing vs.\ sld-resolution.
\newblock {\em Theoretical Computer Science}, 59:3--23, 1988.

\bibitem[BK86]{BeKl86}
J.A. Bergstra and {Jan Willem} Klop.
\newblock Conditional rewrite rules: Confluence and termination.
\newblock {\em Journal of Computer and System Sciences}, 32(3):323--362, 1986.

\bibitem[DJ90]{DeJo90}
Nachum Dershowitz and Jean-Pierre Jouannaud.
\newblock Rewrite systems.
\newblock In J.~van Leeuwen, editor, {\em Formal models and semantics, Handbook
  of Theoretical Computer Science}, volume~B, chapter~6, pages 243--320.
  Elsevier, 1990.

\bibitem[DMS90]{DeMiSi90}
Nachum Dershowitz, Subrata Mitra, and G.~Sivakumar.
\newblock Equation solving in conditional ac-theories.
\newblock In H{\'e}l{\`e}ne Kirchner and Wolfgang Wechler, editors, {\em
  Proc.~2nd Int.~Conf.~on Algebraic and Logic Programming (ALP'90)}, volume 463
  of {\em Lecture Notes in Computer Science}, pages 283--297, Nancy, France,
  October 1990. Springer-Verlag.
\newblock ISBN 3-540-53162-9.

\bibitem[DO88a]{DeOk88a}
Nachum Dershowitz and Mitsuhiro Okada.
\newblock Conditional equational programming and the theory of conditional term
  rewriting.
\newblock In Institute for New Generation Computer Technology~(ICOT), editor,
  {\em Proceedings of the International Conference on Fifth Generation Computer
  Systems 1988}, pages 337--346, Tokyo, Japan, November 28--December 2 1988.
\newblock 3 Volumes, OHMSHA Ltd. Tokyo and Springer-Verlag, 1988 ISBN
  3-540-19558-0, 0-387-19558-0 and 4-274-19558-0.

\bibitem[DO88b]{DeOk88}
Nachum Dershowitz and Mitsuhiro Okada.
\newblock Proof-theoretic techniques for term rewriting theory.
\newblock In {\em Proceedings of the Third Annual Symposium on Logic in
  Computer Science (LICS '88)}, pages 104--111, Edinburgh, Scotland, UK, July
  1988. IEEE Computer Society.
\newblock ISBN 0-8186-0853-6.

\bibitem[DO90]{DeOk90}
Nachum Dershowitz and Mitsuhiro Okada.
\newblock A rationale for conditional equational programming.
\newblock {\em Theoretical Computer Science}, 75:111--138, 1990.

\bibitem[DOS88a]{DeOkSi88}
Nachum Dershowitz, Mitsuhiro Okada, and G.~Sivakumar.
\newblock Canonical conditional rewrite systems.
\newblock In E.\ Lusk and R.\ Overbeek, editors, {\em Proc.~9th Int.~Conf.~on
  Automated Deduction}, volume 310 of {\em Lecture Notes in Computer Science},
  pages 538--549. Springer-Verlag, 1988.

\bibitem[DOS88b]{DeOkSi88a}
Nachum Dershowitz, Mitsuhiro Okada, and G.~Sivakumar.
\newblock Confluence of conditional rewrite systems.
\newblock In S.~Kaplan and J.-P. Jouannaud, editors, {\em Proc.~1st
  Int.~Workshop on Conditional Term Rewriting Systems}, volume 308 of {\em
  Lecture Notes in Computer Science}, pages 31--44, Orsay, France, 1988.
  Springer-Verlag.

\bibitem[DP87]{DePl87}
Nachum Dershowitz and {David A.} Plaisted.
\newblock Equational programming.
\newblock {\em Machine Intelligence}, 11:21--56, 1987.
\newblock Oxford University Press.

\bibitem[GM87]{GiMo88a}
Elio Giovanetti and Corrado Moiso.
\newblock Notes on the elimination of conditions.
\newblock In St{\'e}phane Kaplan and Jean-Pierre Jouannaud, editors, {\em
  Proc.\ 1st Int.\ Workshop on Conditional Rewriting Systems (CTRS'87)}, volume
  308 of {\em Lecture Notes in Computer Science}, pages 91--97, Orsay, France,
  July 1987. Springer-Verlag.
\newblock ISBN 3-540-19242-5.

\bibitem[GM88]{GiMo88}
Elio Giovanetti and Corrado Moiso.
\newblock A completeness result for {E}-unification algorithms based on
  conditional narrowing.
\newblock In M.~Boscarol, {L.~Carlucci} Aiello, and G.~Levi, editors, {\em
  Proc.~Workshop on Foundations of Logic and Functional Programming (WFLP'86)},
  volume 306 of {\em Lecture Notes in Computer Science}, pages 157--167,
  Trento, Italy, December 1988. Springer-Verlag.

\bibitem[Gra94]{Gr94a}
Bernhard Gramlich.
\newblock On modularity of termination and confluence properties of conditional
  rewrite systems.
\newblock In Giorgio Levi and Mario Rodr{\'\i}guez-Artalejo, editors, {\em
  Proc.~4th Int.~Conf.~on Algebraic and Logic Programming, Madrid}, volume 850
  of {\em Lecture Notes in Computer Science}, pages 186--203. Springer-Verlag,
  1994.

\bibitem[Gra95]{Gr95a}
Bernhard Gramlich.
\newblock On termination and confluence of conditional rewrite systems.
\newblock In Nachum Dershowitz and Naomi Lindenstrauss, editors, {\em Proc.~4th
  Int.~Workshop on Conditional and Typed Rewriting Systems, Jerusalem, Israel
  (1994)}, volume 968 of {\em Lecture Notes in Computer Science}, pages
  166--185. Springer-Verlag, 1995.

\bibitem[Gra96a]{Gr96d}
Bernhard Gramlich.
\newblock Conditional rewrite systems under signature extensions: Some
  counterexamples.
\newblock In K.U. Schulz and S.~Kepser, editors, {\em Proc.~10th Int.~Workshop
  on Unification (Extended Abstracts), CIS-Bericht-96-91, Universit{\"a}t
  M{\"u}nchen}, pages 45--50, June 1996.

\bibitem[Gra96b]{Gr96b}
Bernhard Gramlich.
\newblock Confluence without termination via parallel critical pairs.
\newblock In H.~Kirchner, editor, {\em Proc.~21st Coll.~on Trees in Algebra and
  Programming}, volume 1059 of {\em Lecture Notes in Computer Science}, pages
  211--225. Springer-Verlag, April 1996.

\bibitem[Gra96c]{Gr96}
Bernhard Gramlich.
\newblock Confluence without termination via parallel critical pairs.
\newblock In {\em Proc.~Coll.~on Trees in Algebra and Programming (CAAP'96)},
  1996.
\newblock To appear.

\bibitem[Gra96d]{Gr96e}
Bernhard Gramlich.
\newblock On termination and confluence properties of disjoint and
  constructor-sharing conditional rewrite systems.
\newblock {\em Theoretical Computer Science}, 165(1):97--131, September 1996.
\newblock special issue of ALP'94.

\bibitem[Gra96e]{Gr96a}
Bernhard Gramlich.
\newblock {\em Termination and Confluence Properties of Structured Rewrite
  Systems}.
\newblock PhD thesis, Fachbereich Informatik, Universit{\"a}t Kaiserslautern,
  January 1996.

\bibitem[GW96]{GrWi96}
Bernhard Gramlich and Claus-Peter Wirth.
\newblock Confluence of terminating conditional rewrite systems revisited.
\newblock In H.~Ganzinger, editor, {\em Proc.~7th Int.~Conf.~on Rewriting
  Techniques and Applications (RTA'96)}, volume 1103 of {\em Lecture Notes in
  Computer Science}, pages 245--259, New Brunswick, NJ, USA, July 1996.
  Springer-Verlag.

\bibitem[HOHT97]{HaOkHiTa97}
S.\ Hattori, K.\ Okano, T.\ Higashino, and K.\ Taniguchi.
\newblock Modularity of level-confluence for conditional term rewriting systems
  with extra variables in right-hand sides.
\newblock In {\em TGCOMP}, 1997.

\bibitem[Hue80]{Hu80a}
G{\'e}rard Huet.
\newblock Confluent reductions: Abstract properties and applications to term
  rewriting systems.
\newblock {\em Journal of the {ACM}}, 27(4):797--821, October 1980.

\bibitem[Hue81]{Hu81}
G{\'e}rard Huet.
\newblock A complete proof of correctness of the {Knuth-Bendix} completion
  algorithm.
\newblock {\em Journal of Computer and System Sciences}, 23(1):11--21, 1981.

\bibitem[Hus85a]{Hu85}
Heinrich Hussmann.
\newblock Unification in conditional-equational theories.
\newblock Technical Report MIP-8502, Univ. Passau, Passau, January 1985.
\newblock (Corrigenda 1988).

\bibitem[Hus85b]{Hu85a}
Heinrich Hussmann.
\newblock Unification in conditional-equational theories.
\newblock In {\em Proc. EUROCAL '87 (?)}, Lecture Notes in Computer Science,
  pages 543--553, Linz, Austria, April 1985. Springer-Verlag.

\bibitem[JS86]{JaSi86}
Bharat Jayaraman and {Frank S.~K.} Silbermann.
\newblock Equations, sets, and reduction semantics for functional and logic
  programming.
\newblock In {\em Proceedings of the 1986 ACM Conference on LISP and Functional
  Programming}, pages 320--331, Cambridge, Massachusetts, USA, 1986. ACM Press.
\newblock August.

\bibitem[JW86]{JoWa86}
Jean-Pierre Jouannaud and Bernard Waldmann.
\newblock Reductive conditional term rewriting systems.
\newblock In {\em Proceedings of the 3rd {IFIP} Working Conference on Formal
  Description of Programming Concepts}, pages 223--244. North-Holland, 1986.

\bibitem[Kap84]{Ka84}
St{\'e}phane Kaplan.
\newblock Conditional rewrite rules.
\newblock {\em Theoretical Computer Science}, 33:175--193, 1984.

\bibitem[Kap87a]{Ka87a}
St{\'e}phane Kaplan.
\newblock Positive/negative conditional rewriting.
\newblock In St{\'e}phane Kaplan and J.-P. Jouannaud, editors, {\em Proc.~1st
  Int.~Workshop on Conditional Term Rewriting Systems}, volume 308 of {\em
  Lecture Notes in Computer Science}, pages 129--143. Springer-Verlag, 1987.

\bibitem[Kap87b]{Ka87}
St{\'e}phane Kaplan.
\newblock Simplifying conditional term rewriting systems: Unification,
  termination and confluence.
\newblock {\em Journal of Symbolic Computation}, 4:295--334, 1987.

\bibitem[KB70]{KnBe70}
Donald~E. Knuth and Peter~B. Bendix.
\newblock Simple word problems in universal algebra.
\newblock In J.~Leech, editor, {\em Computational Problems in Abstract
  Algebra}, pages 263--297. Pergamon Press, Oxford, U. K., 1970.
\newblock Reprinted 1983 in ``Automation of Reasoning 2'', Springer, Berlin,
  pp. 342--376.

\bibitem[Klo92]{Kl92}
Jan~Willem Klop.
\newblock Term rewriting systems.
\newblock In S.~Abramsky, D.~Gabbay, and T.~Maibaum, editors, {\em Handbook of
  Logic in Computer Science}, volume~2, chapter~1, pages 2--117. Clarendon
  Press, Oxford, 1992.

\bibitem[KMN88]{KaMuNa88}
Deepak Kapur, D.R. Musser, and Paliath Narendran.
\newblock Only prime superpositions need be considered in the {Knuth-Bendix}
  completion procedure.
\newblock {\em Journal of Symbolic Computation}, 1988(6):19--36, 1988.

\bibitem[KW97]{KuWi97}
Ulrich K{\"u}hler and Claus-Peter Wirth.
\newblock Conditional equational specifications of data types with partial
  operations for inductive theorem proving.
\newblock In H.\ Comon, editor, {\em Proc.~8th Int.~Conf.~on Rewriting
  Techniques and Applications (RTA'97)}, volume 1232 of {\em Lecture Notes in
  Computer Science}, pages 38--52, Sitges, Spain, June 1997. Springer-Verlag.

\bibitem[Mar97]{Ma97b}
Massimo Marchiori.
\newblock On deterministic conditional rewriting.
\newblock Technical Report MIT LCS CSG Memo n.405, MIT, Cambridge, MA, USA,
  October 1997.

\bibitem[Mid92]{Mi92}
Aart Middeldorp.
\newblock Personal communication, 1992.

\bibitem[MS88]{MoSr87}
{Chilukuri K.} Mohan and {Mandayam K.} Srivas.
\newblock Conditional specifications with inequational assumptions.
\newblock In St{\'e}phane Kaplan and Jean-Pierre Jouannaud, editors, {\em
  Proc.~1st Int.~Workshop on Conditional Term Rewriting Systems}, volume 308 of
  {\em Lecture Notes in Computer Science}, pages 161--178, Orsay, France, 1988.
  Springer-Verlag.

\bibitem[MS89]{MoSr89}
{Chilukuri K.} Mohan and {Mandayam K.} Srivas.
\newblock Negation with logical variables in conditional rewriting.
\newblock In Nachum Dershowitz, editor, {\em Proc.~3rd Int.~Conf.~on Rewriting
  Techniques and Applications (RTA'89)}, volume 355 of {\em Lecture Notes in
  Computer Science}, pages 292--310, Chapel Hill, North Carolina, USA, April
  1989. Springer-Verlag.

\bibitem[New42]{Ne42}
Maxwell Herman~Alexander Newman.
\newblock On theories with a combinatorial definition of equivalence.
\newblock {\em Annals of Mathematics}, 43(2):223--242, 1942.

\bibitem[OG89a]{OkGr89a}
Mitsuhiro Okada and Peter Grogono.
\newblock New results in term rewriting theory.
\newblock In ???, editor, {\em Proc.~of the Int.~Conf.~on Symbolic and Logic
  Computation}, ???, page ???, ???, ??? 1989. ???

\bibitem[OG89b]{OkGr89}
Mitsuhiro Okada and Peter Grogono.
\newblock Practical application of conditional term rewriting systems.
\newblock In ???, editor, {\em Proc.~IX Conf.~of the Chilean Computer Sceince
  Society / XV Latin American Conf.~on Informatics}, ???, page ???, ???, ???
  1989. ???

\bibitem[Ros73]{Ro73}
Barry~K. Rosen.
\newblock Tree-manipulating systems and {C}hurch-{R}osser theorems.
\newblock {\em Journal of the {ACM}}, 20:160--187, 1973.

\bibitem[Siv89]{Si89}
G.~Sivakumar.
\newblock {\em Proofs and Computations in Conditional Equational Theories}.
\newblock PhD thesis, University of Illinois at Urbana-Champaign, 1989.

\bibitem[SMI95]{SuMiId95}
Taro Suzuki, Aart Middeldorp, and Tetsuo Ida.
\newblock Level-confluence of conditional rewrite systems with extra variables
  in right-hand sides.
\newblock In J.~Hsiang, editor, {\em Proc.~6th Int.~Conf.~on Rewriting
  Techniques and Applications (RTA'95)}, volume 914 of {\em Lecture Notes in
  Computer Science}, pages 179--193, Kaiserslautern, Germany, April 1995.
  Springer-Verlag.

\bibitem[Toy88]{To88a}
Yoshihito Toyama.
\newblock Confluent term rewriting systems with membership conditions.
\newblock In St{\'e}phane Kaplan and Jean-Pierre Jouannaud, editors, {\em
  Proc.~1st Int.~Workshop on Conditional Term Rewriting Systems}, volume 308 of
  {\em Lecture Notes in Computer Science}, pages 228--241, Orsay, France, 1988.
  Springer-Verlag.

\bibitem[WG94]{WiGr94a}
Claus-Peter Wirth and Bernhard Gramlich.
\newblock A constructor-based approach for positive/negative conditional
  equational specifications.
\newblock {\em Journal of Symbolic Computation}, 17:51--90, 1994.

\bibitem[Wir95]{Wi95}
Claus-Peter Wirth.
\newblock Syntactic confluence criteria for constructor-based
  positive/negative-conditional term rewriting systems.
\newblock {SEKI}-Report SR-95-09, Fachbereich Informatik, Universit{\"a}t
  Kaiserslautern, 1995.

\bibitem[Wir97]{Wi97}
Claus-Peter Wirth.
\newblock {\em Positive/Negative-Conditional Equations}.
\newblock PhD thesis, Fachbereich Informatik, Universit{\"a}t Kaiserslautern,
  Verlag, Dr.\ Kova\v{c}, Hamburg, 1997.

\bibitem[YALSM97]{YaAvLoMi97}
Toshiyuki Yamada, J{\"u}rgen Avenhaus, Carlos Lor{\'\i}a-S{\'a}enz, and Aart
  Middeldorp.
\newblock Logicality of conditional rewrite systems.
\newblock In Max Dauchet, editor, {\em Proc.~Coll.~on Trees in Algebra and
  Programming (CAAP'97)}, volume 1214 of {\em Lecture Notes in Computer
  Science}, pages 141--152, Lille, France, April 1997. Springer-Verlag.

\bibitem[YALSM00]{YaAvLoMi00}
Toshiyuki Yamada, J{\"u}rgen Avenhaus, Carlos Lor{\'\i}a-S{\'a}enz, and Aart
  Middeldorp.
\newblock Logicality of conditional rewrite systems.
\newblock {\em Theoretical Computer Science}, 236(1,2):209--232, 2000.

\end{thebibliography}