\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Avenhaus and Lor{\'\i}a-S{\'a}enz}{Avenhaus
  and Lor{\'\i}a-S{\'a}enz}{1994a}]{AvLo94}
{\sc Avenhaus, J.} {\sc and} {\sc Lor{\'\i}a-S{\'a}enz, C.} 1994a.
\newblock Higher order conditional rewriting and narrowing.
\newblock In {\em Proc.~1st Int.\ Conf.\ on Constraints in Computational Logics
  (CCL'94)}, {J.-P. Jouannaud}, Ed. Lecture Notes in Computer Science, vol.
  845. Springer-Verlag, 269--284.

\bibitem[\protect\citeauthoryear{Avenhaus and Lor{\'\i}a-S{\'a}enz}{Avenhaus
  and Lor{\'\i}a-S{\'a}enz}{1994b}]{AvLo94a}
{\sc Avenhaus, J.} {\sc and} {\sc Lor{\'\i}a-S{\'a}enz, C.} 1994b.
\newblock On conditional rewrite systems with extra variables and deterministic
  logic programs.
\newblock In {\em Proc.~5th Int.~Conf.~on Logic Programming and Automated
  Reasoning}, {F.~Pfenning}, Ed. Lecture Notes in Artificial Intelligence, vol.
  822. Springer-Verlag, Kiev, Ukraine, 215--229.

\bibitem[\protect\citeauthoryear{Bachmair and Dershowitz}{Bachmair and
  Dershowitz}{1988}]{BaDe88}
{\sc Bachmair, L.} {\sc and} {\sc Dershowitz, N.} 1988.
\newblock Critical pair criteria for completion.
\newblock {\em Journal of Symbolic Computation\/}~{\em 6,\/}~1, 1--18.

\bibitem[\protect\citeauthoryear{Bergstra and Klop}{Bergstra and
  Klop}{1986}]{BeKl86}
{\sc Bergstra, J.} {\sc and} {\sc Klop, J.} 1986.
\newblock Conditional rewrite rules: Confluence and termination.
\newblock {\em Journal of Computer and System Sciences\/}~{\em 32,\/}~3,
  323--362.

\bibitem[\protect\citeauthoryear{Bevers and Levi}{Bevers and
  Levi}{1990}]{BeLe90}
{\sc Bevers, E.} {\sc and} {\sc Levi, J.} 1990.
\newblock Proof by consistency in conditional equational theories.
\newblock draft 8/90.

\bibitem[\protect\citeauthoryear{Bevers and Lewi}{Bevers and
  Lewi}{1993}]{BeLe93}
{\sc Bevers, E.} {\sc and} {\sc Lewi, J.} 1993.
\newblock Proving termination of (conditional) rewrite systems.
\newblock {\em Acta Informatica\/}~{\em 30}, 537--568.

\bibitem[\protect\citeauthoryear{Bosco, Giovannetti, and Moiso}{Bosco
  et~al\mbox{.}}{1987}]{BoGiMo87}
{\sc Bosco, P.}, {\sc Giovannetti, E.}, {\sc and} {\sc Moiso, C.} 1987.
\newblock Refined strategies for semantic unification.
\newblock In {\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)}, {H.~Ehrig},
  {R.~Kowalski}, {G.~Levi}, {and} {U.~Montanari}, Eds. Lecture Notes in
  Computer Science, vol. 250. Springer-Verlag, Pisa, Italy, 276--290.

\bibitem[\protect\citeauthoryear{Bosco, Giovannetti, and Moiso}{Bosco
  et~al\mbox{.}}{1988}]{BoGiMo88}
{\sc Bosco, P.}, {\sc Giovannetti, E.}, {\sc and} {\sc Moiso, C.} 1988.
\newblock Narrowing vs.\ sld-resolution.
\newblock {\em Theoretical Computer Science\/}~{\em 59}, 3--23.

\bibitem[\protect\citeauthoryear{Dershowitz and Jouannaud}{Dershowitz and
  Jouannaud}{1990}]{DeJo90}
{\sc Dershowitz, N.} {\sc and} {\sc Jouannaud, J.-P.} 1990.
\newblock Rewrite systems.
\newblock In {\em Formal models and semantics, Handbook of Theoretical Computer
  Science}, {J.~van Leeuwen}, Ed. Vol.~B. Elsevier, Chapter~6, 243--320.

\bibitem[\protect\citeauthoryear{Dershowitz, Mitra, and Sivakumar}{Dershowitz
  et~al\mbox{.}}{1990}]{DeMiSi90}
{\sc Dershowitz, N.}, {\sc Mitra, S.}, {\sc and} {\sc Sivakumar, G.} 1990.
\newblock Equation solving in conditional ac-theories.
\newblock In {\em Proc.~2nd Int.~Conf.~on Algebraic and Logic Programming
  (ALP'90)}, {H.~Kirchner} {and} {W.~Wechler}, Eds. Lecture Notes in Computer
  Science, vol. 463. Springer-Verlag, Nancy, France, 283--297.
\newblock ISBN 3-540-53162-9.

\bibitem[\protect\citeauthoryear{Dershowitz, Mitra, and Sivakumar}{Dershowitz
  et~al\mbox{.}}{1992}]{DeMiSi92}
{\sc Dershowitz, N.}, {\sc Mitra, S.}, {\sc and} {\sc Sivakumar, G.} 1992.
\newblock Decidable matching for convergent systems (preliminary version).
\newblock In {\em Proc.~11th Int.~Conf.~on Automated Deduction (CADE'92)},
  {D.~Kapur}, Ed. Lecture Notes in Artificial Intelligence, vol. 607.
  Springer-Verlag, Saratoga Springs, NY, USA, 589--602.
\newblock ISBN 3-540-55602-8.

\bibitem[\protect\citeauthoryear{Dershowitz and Okada}{Dershowitz and
  Okada}{1988a}]{DeOk88a}
{\sc Dershowitz, N.} {\sc and} {\sc Okada, M.} 1988a.
\newblock Conditional equational programming and the theory of conditional term
  rewriting.
\newblock In {\em Proceedings of the International Conference on Fifth
  Generation Computer Systems 1988}, {I.~for New Generation Computer
  Technology~(ICOT)}, Ed. Tokyo, Japan, 337--346.
\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[\protect\citeauthoryear{Dershowitz and Okada}{Dershowitz and
  Okada}{1988b}]{DeOk88}
{\sc Dershowitz, N.} {\sc and} {\sc Okada, M.} 1988b.
\newblock Proof-theoretic techniques for term rewriting theory.
\newblock In {\em Proceedings of the Third Annual Symposium on Logic in
  Computer Science (LICS '88)}. IEEE Computer Society, Edinburgh, Scotland, UK,
  104--111.
\newblock ISBN 0-8186-0853-6.

\bibitem[\protect\citeauthoryear{Dershowitz and Okada}{Dershowitz and
  Okada}{1990}]{DeOk90}
{\sc Dershowitz, N.} {\sc and} {\sc Okada, M.} 1990.
\newblock A rationale for conditional equational programming.
\newblock {\em Theoretical Computer Science\/}~{\em 75}, 111--138.

\bibitem[\protect\citeauthoryear{Dershowitz, Okada, and Sivakumar}{Dershowitz
  et~al\mbox{.}}{1988a}]{DeOkSi88}
{\sc Dershowitz, N.}, {\sc Okada, M.}, {\sc and} {\sc Sivakumar, G.} 1988a.
\newblock Canonical conditional rewrite systems.
\newblock In {\em Proc.~9th Int.~Conf.~on Automated Deduction}, {E.~Lusk} {and}
  {R.~Overbeek}, Eds. Lecture Notes in Computer Science, vol. 310.
  Springer-Verlag, 538--549.

\bibitem[\protect\citeauthoryear{Dershowitz, Okada, and Sivakumar}{Dershowitz
  et~al\mbox{.}}{1988b}]{DeOkSi88a}
{\sc Dershowitz, N.}, {\sc Okada, M.}, {\sc and} {\sc Sivakumar, G.} 1988b.
\newblock Confluence of conditional rewrite systems.
\newblock In {\em Proc.~1st Int.~Workshop on Conditional Term Rewriting
  Systems}, {S.~Kaplan} {and} {J.-P. Jouannaud}, Eds. Lecture Notes in Computer
  Science, vol. 308. Springer-Verlag, Orsay, France, 31--44.

\bibitem[\protect\citeauthoryear{Dershowitz and Plaisted}{Dershowitz and
  Plaisted}{1987}]{DePl87}
{\sc Dershowitz, N.} {\sc and} {\sc Plaisted, D.} 1987.
\newblock Equational programming.
\newblock {\em Machine Intelligence\/}~{\em 11}, 21--56.
\newblock Oxford University Press.

\bibitem[\protect\citeauthoryear{Dershowitz and Sivakumar}{Dershowitz and
  Sivakumar}{1988a}]{DeSi88}
{\sc Dershowitz, N.} {\sc and} {\sc Sivakumar, G.} 1988a.
\newblock Goal-directed equation solving.
\newblock In {\em Proceedings of the 7th National Conference on Artificial
  Intelligence (AAAI'88)}. AAAI Press / The MIT Press,, St.~Paul, Minnesota,
  USA, 166--170.
\newblock ISBN 0-262-51055-3.

\bibitem[\protect\citeauthoryear{Dershowitz and Sivakumar}{Dershowitz and
  Sivakumar}{1988b}]{DeSi88a}
{\sc Dershowitz, N.} {\sc and} {\sc Sivakumar, G.} 1988b.
\newblock Solving goals in equational languages.
\newblock In {\em Proc.\ 1st Int.\ Workshop on Conditional Rewriting Systems
  (CTRS'87)}, {S.~Kaplan} {and} {J.-P. Jouannaud}, Eds. Lecture Notes in
  Computer Science, vol. 308. Springer-Verlag, Orsay, France, 45--55.
\newblock ISBN 3-540-19242-5.

\bibitem[\protect\citeauthoryear{Giovanetti and Moiso}{Giovanetti and
  Moiso}{1987}]{GiMo88a}
{\sc Giovanetti, E.} {\sc and} {\sc Moiso, C.} 1987.
\newblock Notes on the elimination of conditions.
\newblock In {\em Proc.\ 1st Int.\ Workshop on Conditional Rewriting Systems
  (CTRS'87)}, {S.~Kaplan} {and} {J.-P. Jouannaud}, Eds. Lecture Notes in
  Computer Science, vol. 308. Springer-Verlag, Orsay, France, 91--97.
\newblock ISBN 3-540-19242-5.

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

\bibitem[\protect\citeauthoryear{Gramlich}{Gramlich}{1994}]{Gr94a}
{\sc Gramlich, B.} 1994.
\newblock On modularity of termination and confluence properties of conditional
  rewrite systems.
\newblock In {\em Proc.~4th Int.~Conf.~on Algebraic and Logic Programming,
  Madrid}, {G.~Levi} {and} {M.~Rodr{\'\i}guez-Artalejo}, Eds. Lecture Notes in
  Computer Science, vol. 850. Springer-Verlag, 186--203.

\bibitem[\protect\citeauthoryear{Gramlich}{Gramlich}{1995}]{Gr95a}
{\sc Gramlich, B.} 1995.
\newblock On termination and confluence of conditional rewrite systems.
\newblock In {\em Proc.~4th Int.~Workshop on Conditional and Typed Rewriting
  Systems, Jerusalem, Israel (1994)}, {N.~Dershowitz} {and} {N.~Lindenstrauss},
  Eds. Lecture Notes in Computer Science, vol. 968. Springer-Verlag, 166--185.

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

\bibitem[\protect\citeauthoryear{Gramlich}{Gramlich}{1996b}]{Gr96b}
{\sc Gramlich, B.} 1996b.
\newblock Confluence without termination via parallel critical pairs.
\newblock In {\em Proc.~21st Coll.~on Trees in Algebra and Programming},
  {H.~Kirchner}, Ed. Lecture Notes in Computer Science, vol. 1059.
  Springer-Verlag, 211--225.

\bibitem[\protect\citeauthoryear{Gramlich}{Gramlich}{1996c}]{Gr96e}
{\sc Gramlich, B.} 1996c.
\newblock On termination and confluence properties of disjoint and
  constructor-sharing conditional rewrite systems.
\newblock {\em Theoretical Computer Science\/}~{\em 165,\/}~1 (Sept.), 97--131.
\newblock special issue of ALP'94.

\bibitem[\protect\citeauthoryear{Gramlich and Wirth}{Gramlich and
  Wirth}{1996}]{GrWi96}
{\sc Gramlich, B.} {\sc and} {\sc Wirth, C.-P.} 1996.
\newblock Confluence of terminating conditional rewrite systems revisited.
\newblock In {\em Proc.~7th Int.~Conf.~on Rewriting Techniques and Applications
  (RTA'96)}, {H.~Ganzinger}, Ed. Lecture Notes in Computer Science, vol. 1103.
  Springer-Verlag, New Brunswick, NJ, USA, 245--259.

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

\bibitem[\protect\citeauthoryear{Hoot}{Hoot}{1995}]{Ho95}
{\sc Hoot, C.} 1995.
\newblock Termination for restricted derivations and conditional rewrite
  systems.
\newblock In {\em Proc.~4th Int.~Workshop on Conditional and Typed Rewriting
  Systems, Jerusalem, Israel (1994)}, {N.~Dershowitz} {and} {N.~Lindenstrauss},
  Eds. Lecture Notes in Computer Science, vol. 968. Springer-Verlag, 206--222.

\bibitem[\protect\citeauthoryear{Hussmann}{Hussmann}{1985a}]{Hu85}
{\sc Hussmann, H.} 1985a.
\newblock Unification in conditional-equational theories.
\newblock Tech. Rep. MIP-8502, Univ. Passau, Passau. Jan.
\newblock (Corrigenda 1988).

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

\bibitem[\protect\citeauthoryear{Jayaraman and Silbermann}{Jayaraman and
  Silbermann}{1986}]{JaSi86}
{\sc Jayaraman, B.} {\sc and} {\sc Silbermann, F.} 1986.
\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}. ACM Press, Cambridge, Massachusetts, USA, 320--331.
\newblock Aug.

\bibitem[\protect\citeauthoryear{Jouannaud and Waldmann}{Jouannaud and
  Waldmann}{1986}]{JoWa86}
{\sc Jouannaud, J.-P.} {\sc and} {\sc Waldmann, B.} 1986.
\newblock Reductive conditional term rewriting systems.
\newblock In {\em Proceedings of the 3rd {IFIP} Working Conference on Formal
  Description of Programming Concepts}. North-Holland, 223--244.

\bibitem[\protect\citeauthoryear{Kaplan}{Kaplan}{1984}]{Ka84}
{\sc Kaplan, S.} 1984.
\newblock Conditional rewrite rules.
\newblock {\em Theoretical Computer Science\/}~{\em 33}, 175--193.

\bibitem[\protect\citeauthoryear{Kaplan}{Kaplan}{1987a}]{Ka87a}
{\sc Kaplan, S.} 1987a.
\newblock Positive/negative conditional rewriting.
\newblock In Proc.~1st Int.~Workshop on Conditional Term Rewriting Systems,
  {S.~Kaplan} {and} {J.-P. Jouannaud}, Eds. {\em Journal of Symbolic
  Computation\/}~{\em 308}, 129--143.

\bibitem[\protect\citeauthoryear{Kaplan}{Kaplan}{1987b}]{Ka87}
{\sc Kaplan, S.} 1987b.
\newblock Simplifying conditional term rewriting systems: Unification,
  termination and confluence.
\newblock {\em Journal of Symbolic Computation\/}~{\em 4}, 295--334.

\bibitem[\protect\citeauthoryear{Kapur, Musser, and Narendran}{Kapur
  et~al\mbox{.}}{1988}]{KaMuNa88}
{\sc Kapur, D.}, {\sc Musser, D.}, {\sc and} {\sc Narendran, P.} 1988.
\newblock Only prime superpositions need be considered in the {Knuth-Bendix}
  completion procedure.
\newblock {\em Journal of Symbolic Computation\/}~{\em 1988,\/}~6, 19--36.

\bibitem[\protect\citeauthoryear{Klop}{Klop}{1992}]{Kl92}
{\sc Klop, J.~W.} 1992.
\newblock Term rewriting systems.
\newblock In {\em Handbook of Logic in Computer Science}, {S.~Abramsky},
  {D.~Gabbay}, {and} {T.~Maibaum}, Eds. Vol.~2. Clarendon Press, Oxford,
  Chapter~1, 2--117.

\bibitem[\protect\citeauthoryear{K{\"u}hler and Wirth}{K{\"u}hler and
  Wirth}{1997}]{KuWi97}
{\sc K{\"u}hler, U.} {\sc and} {\sc Wirth, C.-P.} 1997.
\newblock Conditional equational specifications of data types with partial
  operations for inductive theorem proving.
\newblock In {\em Proc.~8th Int.~Conf.~on Rewriting Techniques and Applications
  (RTA'97)}, {H.~Comon}, Ed. Lecture Notes in Computer Science, vol. 1232.
  Springer-Verlag, Sitges, Spain, 38--52.

\bibitem[\protect\citeauthoryear{Marchiori}{Marchiori}{1996}]{Ma96}
{\sc Marchiori, M.} 1996.
\newblock Unravelings and ultra-properties.
\newblock In {\em Proc.~5th Int.~Conf.~on Algebraic and Logic Programming,
  Aachen}, {M.~Hanus} {and} {M.-R. Artalejo}, Eds. Lecture Notes in Computer
  Science, vol. 1139. Springer-Verlag, 107--121.

\bibitem[\protect\citeauthoryear{Marchiori}{Marchiori}{1997a}]{Ma97b}
{\sc Marchiori, M.} 1997a.
\newblock On deterministic conditional rewriting.
\newblock Technical Report MIT LCS CSG Memo n.405, MIT, Cambridge, MA, USA.
  Oct.

\bibitem[\protect\citeauthoryear{Marchiori}{Marchiori}{1997b}]{Ma97a}
{\sc Marchiori, M.} 1997b.
\newblock On the expressive power of rewriting.
\newblock In {\em Proc.~17th Conf.~on the Foundations of Software Technology
  and Theoretical Computer Science (FSTTCS'97)}, {S.~Ramesh} {and}
  {G.~Sivakumar}, Eds. Lecture Notes in Computer Science, vol. 1346.
  Springer-Verlag, Kharagpur, India, 88--102.

\bibitem[\protect\citeauthoryear{Middeldorp}{Middeldorp}{1990}]{Mi90a}
{\sc Middeldorp, A.} 1990.
\newblock Confluence of the disjoint union of conditional term rewriting
  systems.
\newblock In {\em Proc.~2nd Int.~Workshop on Conditional and Typed Rewriting
  Systems}, {S.~Kaplan} {and} {M.~Okada}, Eds. Lecture Notes in Computer
  Science, vol. 516. Springer-Verlag, 295--306.

\bibitem[\protect\citeauthoryear{Middeldorp}{Middeldorp}{1993a}]{Mi93}
{\sc Middeldorp, A.} 1993a.
\newblock Completeness of combinations of conditional constructor systems.
\newblock In {\em Proc.~3rd Int.~Workshop on Conditional Term Rewriting Systems
  (CTRS, July 1992)}, {M.~Rusinowitch} {and} {J.-L. R{\'e}my}, Eds. Lecture
  Notes in Computer Science, vol. 656. Springer-Verlag, 82--96.

\bibitem[\protect\citeauthoryear{Middeldorp}{Middeldorp}{1993b}]{Mi93a}
{\sc Middeldorp, A.} 1993b.
\newblock Modular properties of conditional term rewriting systems.
\newblock {\em Information and Computation\/}~{\em 104,\/}~1 (May), 110--158.

\bibitem[\protect\citeauthoryear{Middeldorp}{Middeldorp}{1994}]{Mi94a}
{\sc Middeldorp, A.} 1994.
\newblock Completeness of combinations of conditional constructor systems.
\newblock {\em Journal of Symbolic Computation\/}~{\em 17}, 3--21.

\bibitem[\protect\citeauthoryear{Mohan}{Mohan}{1989}]{Mo89}
{\sc Mohan, C.} 1989.
\newblock Priority rewriting: Semantics, confluence, and conditional.
\newblock In {\em Proc.~3rd Int.~Conf.~on Rewriting Techniques and Applications
  (RTA'89)}, {N.~Dershowitz}, Ed. Lecture Notes in Computer Science, vol. 355.
  Springer-Verlag, Chapel Hill, North Carolina, USA, 278--291.

\bibitem[\protect\citeauthoryear{Mohan and Srivas}{Mohan and
  Srivas}{1988}]{MoSr87}
{\sc Mohan, C.} {\sc and} {\sc Srivas, M.} 1988.
\newblock Conditional specifications with inequational assumptions.
\newblock In {\em Proc.~1st Int.~Workshop on Conditional Term Rewriting
  Systems}, {S.~Kaplan} {and} {J.-P. Jouannaud}, Eds. Lecture Notes in Computer
  Science, vol. 308. Springer-Verlag, Orsay, France, 161--178.

\bibitem[\protect\citeauthoryear{Mohan and Srivas}{Mohan and
  Srivas}{1989}]{MoSr89}
{\sc Mohan, C.} {\sc and} {\sc Srivas, M.} 1989.
\newblock Negation with logical variables in conditional rewriting.
\newblock In {\em Proc.~3rd Int.~Conf.~on Rewriting Techniques and Applications
  (RTA'89)}, {N.~Dershowitz}, Ed. Lecture Notes in Computer Science, vol. 355.
  Springer-Verlag, Chapel Hill, North Carolina, USA, 292--310.

\bibitem[\protect\citeauthoryear{Ohlebusch}{Ohlebusch}{1992}]{Oh92}
{\sc Ohlebusch, E.} 1992.
\newblock Combinations of simplifying conditional term rewriting systems.
\newblock In {\em Proc. of the 3rd International Workshop on Conditional Term
  Rewriting Systems, Pont-{\`a}-Mousson}, {M.~Rusinowitch} {and} {J.~Remy},
  Eds. Lecture Notes in Computer Science, vol. 656. Springer-Verlag, 113--127.

\bibitem[\protect\citeauthoryear{Ohlebusch}{Ohlebusch}{1995a}]{Oh95}
{\sc Ohlebusch, E.} 1995a.
\newblock Modular properties of composable term rewriting systems.
\newblock {\em Journal of Symbolic Computation\/}~{\em 20,\/}~1 (July), 1--42.

\bibitem[\protect\citeauthoryear{Ohlebusch}{Ohlebusch}{1995b}]{Oh95a}
{\sc Ohlebusch, E.} 1995b.
\newblock Modular properties of constructor-sharing conditional term rewriting
  systems.
\newblock In {\em Proc.~4th Int.~Workshop on Conditional and Typed Rewriting
  Systems, Jerusalem, Israel (1994)}, {N.~Dershowitz} {and} {N.~Lindenstrauss},
  Eds. Lecture Notes in Computer Science, vol. 968. Springer-Verlag, 296--315.

\bibitem[\protect\citeauthoryear{Ohlebusch}{Ohlebusch}{1997}]{Oh97a}
{\sc Ohlebusch, E.} 1997.
\newblock Conditional term graph rewriting.
\newblock In {\em Algebraic and Logic Programming, 6th International Joint
  Conference, ALP'97 -- HOA'97, Proceedings}, {M.~Hanus}, {J.~Heering}, {and}
  {K.~Meinke}, Eds. Lecture Notes in Computer Science, vol. 1298.
  Springer-Verlag, Southampton, UK, 144--158.

\bibitem[\protect\citeauthoryear{Ohlebusch}{Ohlebusch}{1999a}]{Oh99a}
{\sc Ohlebusch, E.} 1999a.
\newblock On quasi-reductive and quasi-simplifying deterministic conditional
  rewrite systems.
\newblock In {\em Proc.\ 4th Fuji Int.\ Symp.\ on Functional and Logic
  Programming (FLOPS'99)}, {A.~Middeldorp} {and} {T.~Sato}, Eds. Lecture Notes
  in Computer Science, vol. 1722. Springer-Verlag, Tsukuba, Japan, 179--193.

\bibitem[\protect\citeauthoryear{Ohlebusch}{Ohlebusch}{1999b}]{Oh99}
{\sc Ohlebusch, E.} 1999b.
\newblock Transforming conditional rewrite systems with extra variables into
  unconditional systems.
\newblock In {\em Proc.~6th Int.~Conf.~on Logic Programming and Automated
  Reasoning (LPAR'99)}, {H.~Ganzinger}, {D.~McAllester}, {and} {A.~Voronkov},
  Eds. Lecture Notes in Computer Science, vol. 1705. Springer-Verlag, Tbilisi,
  Georgia, 111--130.

\bibitem[\protect\citeauthoryear{Ohlebusch}{Ohlebusch}{1999c}]{Oh99b}
{\sc Ohlebusch, E.} 1999c.
\newblock Transforming conditional rewrite systems with extra variables into
  unconditional systems.
\newblock Forschungsbericht der Technischen Fakult{\"a}t Abteilung
  Informationstechnik Report 99--02, Universit{\"a}t Bielefeld.

\bibitem[\protect\citeauthoryear{Ohlebusch}{Ohlebusch}{2000}]{Oh00}
{\sc Ohlebusch, E.} 2000.
\newblock A uniform framework for term and graph rewriting applied to combined
  systems.
\newblock {\em Information Processing Letters\/}~{\em 73,\/}~1--2 (Jan.),
  53--59.
\newblock communicated by Harald Ganzinger.

\bibitem[\protect\citeauthoryear{Okada}{Okada}{1987}]{Ok87}
{\sc Okada, M.} 1987.
\newblock Report on conditional rewrite systems.
\newblock (unpublished), Department of Computer Science, University of
  Illinois, Urbana, IL.

\bibitem[\protect\citeauthoryear{Okada}{Okada}{1988}]{Ok88}
{\sc Okada, M.} 1988.
\newblock A logical analysis for theory of conditional rewriting.
\newblock In {\em Proc.\ 1st Int.\ Workshop on Conditional Rewriting Systems
  (CTRS'87)}, {S.~Kaplan} {and} {J.-P. Jouannaud}, Eds. Lecture Notes in
  Computer Science, vol. 308. Springer-Verlag, Orsay, France, 179--198.

\bibitem[\protect\citeauthoryear{Okada and Grogono}{Okada and
  Grogono}{1989a}]{OkGr89a}
{\sc Okada, M.} {\sc and} {\sc Grogono, P.} 1989a.
\newblock New results in term rewriting theory.
\newblock In {\em Proc.~of the Int.~Conf.~on Symbolic and Logic Computation},
  {???}, Ed. ??? ???, ???, ???

\bibitem[\protect\citeauthoryear{Okada and Grogono}{Okada and
  Grogono}{1989b}]{OkGr89}
{\sc Okada, M.} {\sc and} {\sc Grogono, P.} 1989b.
\newblock Practical application of conditional term rewriting systems.
\newblock In {\em Proc.~IX Conf.~of the Chilean Computer Sceince Society / XV
  Latin American Conf.~on Informatics}, {???}, Ed. ??? ???, ???, ???

\bibitem[\protect\citeauthoryear{Okada and Takeuti}{Okada and
  Takeuti}{1987}]{OkTa87}
{\sc Okada, M.} {\sc and} {\sc Takeuti, G.} 1987.
\newblock On the theory of quasi ordinal diagrams.
\newblock In {\em Logic and combinatorics, Proc.\ AMS-IMS-SIAM Conf.,
  Arcata/Calif.\ 1985,}, {S.~Simpson}, Ed. Contemporary Mathematics, vol.~68.
  American Mathematical Society, 295--308.

\bibitem[\protect\citeauthoryear{Sivakumar}{Sivakumar}{1989}]{Si89}
{\sc Sivakumar, G.} 1989.
\newblock Proofs and computations in conditional equational theories.
\newblock Ph.D. thesis, University of Illinois at Urbana-Champaign.

\bibitem[\protect\citeauthoryear{Suzuki, Middeldorp, and Ida}{Suzuki
  et~al\mbox{.}}{1995}]{SuMiId95}
{\sc Suzuki, T.}, {\sc Middeldorp, A.}, {\sc and} {\sc Ida, T.} 1995.
\newblock Level-confluence of conditional rewrite systems with extra variables
  in right-hand sides.
\newblock In {\em Proc.~6th Int.~Conf.~on Rewriting Techniques and Applications
  (RTA'95)}, {J.~Hsiang}, Ed. Lecture Notes in Computer Science, vol. 914.
  Springer-Verlag, Kaiserslautern, Germany, 179--193.

\bibitem[\protect\citeauthoryear{Takahashi, Sakai, and Toyama}{Takahashi
  et~al\mbox{.}}{1994}]{TaSaTo94}
{\sc Takahashi, Y.}, {\sc Sakai, M.}, {\sc and} {\sc Toyama, Y.} 1994.
\newblock On the confluence of conditional term rewriting systems.
\newblock IEICE Technical Report COMP94-65 (1994-11), IEICE, School of
  Information Science, JAIST.
\newblock (In Japanese).

\bibitem[\protect\citeauthoryear{Wirth}{Wirth}{1995}]{Wi95}
{\sc Wirth, C.-P.} 1995.
\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.

\bibitem[\protect\citeauthoryear{Wirth}{Wirth}{1997}]{Wi97}
{\sc Wirth, C.-P.} 1997.
\newblock Positive/negative-conditional equations.
\newblock Ph.D. thesis, Fachbereich Informatik, Universit{\"a}t Kaiserslautern,
  Verlag, Dr.\ Kova\v{c}, Hamburg.

\bibitem[\protect\citeauthoryear{Wirth and Gramlich}{Wirth and
  Gramlich}{1993}]{WiGr93}
{\sc Wirth, C.-P.} {\sc and} {\sc Gramlich, B.} 1993.
\newblock A constructor-based approach for positive/negative conditional
  equational specifications.
\newblock In {\em Proc.~3rd Int.~Workshop on Conditional Term Rewriting Systems
  (CTRS, July 1992)}, {M.~Rusinowitch} {and} {J.-L. R{\'e}my}, Eds. Lecture
  Notes in Computer Science, vol. 656. Springer-Verlag, Pont-{\`a}-Mousson,
  France, 198--212.

\bibitem[\protect\citeauthoryear{Wirth and Gramlich}{Wirth and
  Gramlich}{1994a}]{WiGr94a}
{\sc Wirth, C.-P.} {\sc and} {\sc Gramlich, B.} 1994a.
\newblock A constructor-based approach for positive/negative conditional
  equational specifications.
\newblock {\em Journal of Symbolic Computation\/}~{\em 17}, 51--90.

\bibitem[\protect\citeauthoryear{Wirth and Gramlich}{Wirth and
  Gramlich}{1994b}]{WiGr94}
{\sc Wirth, C.-P.} {\sc and} {\sc Gramlich, B.} 1994b.
\newblock On notions of inductive validity for first-order equational clauses.
\newblock In {\em Proc.~12th Int.~Conf.~on Automated Deduction}, {A.~Bundy},
  Ed. Lecture Notes in Artificial Intelligence, vol. 814. Springer-Verlag,
  Nancy, France, 162--176.

\bibitem[\protect\citeauthoryear{Yamada, Avenhaus, Lor{\'\i}a-S{\'a}enz, and
  Middeldorp}{Yamada et~al\mbox{.}}{1997}]{YaAvLoMi97}
{\sc Yamada, T.}, {\sc Avenhaus, J.}, {\sc Lor{\'\i}a-S{\'a}enz, C.}, {\sc and}
  {\sc Middeldorp, A.} 1997.
\newblock Logicality of conditional rewrite systems.
\newblock In {\em Proc.~Coll.~on Trees in Algebra and Programming (CAAP'97)},
  {M.~Dauchet}, Ed. Lecture Notes in Computer Science, vol. 1214.
  Springer-Verlag, Lille, France, 141--152.

\end{thebibliography}
