\begin{thebibliography}{10}

\bibitem{AM93}
G.~Aguzzi and U.~Modigliani.
\newblock Proving termination of logic programs by transforming them into
  equivalent term rewriting systems.
\newblock In {\em Foundations of Software Technology and Theoretical Computer
  Science}, volume 761 of {\em {LNCS}}, pages 114--124. {S}pringer--{V}erlag,
  1993.

\bibitem{AZ96}
T.~Arts and H.~Zantema.
\newblock Termination of logic programs using semantic unification.
\newblock In {\em Proceedings of the Fifth Workshop on Logic Program Synthesis
  and Transformation}, {LNCS}. {S}pringer--{V}erlag, 1996.
\newblock To appear.

\bibitem{AL94b}
J.~Avenhaus and C.~Lor{\'{\i}}a-S{\'a}enz.
\newblock On conditional rewrite systems with extra variables and deterministic
  logic programs.
\newblock In {\em Proc.\ Int.\ Conference on Logic Programming and Automated
  Reasoning}, volume 822 of {\em {LNAI}}, pages 215--229. Springer--Verlag,
  1994.

\bibitem{BG89}
H.~Bertling and H.~Ganzinger.
\newblock Completion-time optimization of rewrite-time goal solving.
\newblock In {\em Proceedings of the Third International Conference on
  Rewriting Techniques and Applications}, volume 355 of {\em {LNCS}}, pages
  45--58. Springer--Verlag, 1989.

\bibitem{Der94}
N.~Dershowitz.
\newblock Hierarchical termination.
\newblock In N.~Dershowitz and N.~Lindenstrauss, editors, {\em Proceedings 4th
  International Workshop on Conditional and Typed Rewriting Systems}, volume
  968 of {\em {LNCS}}. Springer--Verlag, 1995.

\bibitem{DJ90}
N.~Dershowitz and J.-P. Jouannaud.
\newblock Rewrite systems.
\newblock In J.~van Leeuwen, editor, {\em Handbook of Theoretical Computer
  Science}, volume~B, chapter~6, pages 243--320. {E}lsevier -- {MIT} {P}ress,
  1990.

\bibitem{DO90}
N.~Dershowitz and M.~Okada.
\newblock A rationale for conditional equational programming.
\newblock {\em Theoretical Computer Science}, 75:111--138, 1990.

\bibitem{DOS88}
N.~Dershowitz, M.~Okada, and G.~Sivakumar.
\newblock Canonical conditional rewrite systems.
\newblock In {\em Proceedings of the 9th Conference on Automated Deduction},
  volume 310 of {\em {LNCS}}, pages 538--549. Springer--Verlag, 1988.

\bibitem{Gan91b}
H.~Ganzinger.
\newblock Order-sorted completion: the many-sorted way.
\newblock {\em TCS}, 89:3--32, 1991.

\bibitem{GW92}
H.~Ganzinger and U.~Waldmann.
\newblock Termination proofs of well-moded logic programs via conditional
  rewrite systems.
\newblock In M.~Rusinowitch and J.L. R{\'e}my, editors, {\em CTRS'92}, volume
  656 of {\em {LNCS}}, pages 216--222. {S}pringer--{V}erlag, 1993.

\bibitem{Gra92}
B.~Gramlich.
\newblock Relating innermost, weak, uniform and modular termination of term
  rewriting systems.
\newblock In {\em International Conference on Logic Programming and Automated
  Reasoning}, volume 624 of {\em {LNAI}}, pages 285--296. Springer-Verlag,
  1992.

\bibitem{Gra94}
B.~Gramlich.
\newblock Generalized sufficient conditions for modular termination of
  rewriting.
\newblock {\em Applicable Algebra in Engineering, Communication and Computing},
  5:131--158, 1994.

\bibitem{Han94}
M.~Hanus.
\newblock The integration of functions into logic programming: From theory to
  practice.
\newblock {\em Journal of Logic Programming}, 19\&20:583--628, 1994.

\bibitem{JW86}
J.-P. Jouannaud and B.~Waldmann.
\newblock Reductive conditional term rewrite systems.
\newblock In {\em 3rd {IFIP} Working Conference on Formal Description of
  Programming Concepts}, pages 223--244, Ebberup, Denmark, 1986.

\bibitem{Kap84}
S.~Kaplan.
\newblock Conditional rewrite rules.
\newblock {\em Theoretical Computer Science}, 33(2):175--193, 1984.

\bibitem{Kap87}
S.~Kaplan.
\newblock Simplifying conditional term rewriting systems.
\newblock {\em Journal of Symbolic Computation}, 4(3):295--334, 1987.

\bibitem{Klo92}
J.W. Klop.
\newblock Term rewriting systems.
\newblock In S.~Abramsky, Dov~M. Gabbay, and T.S.E. Maibaum, editors, {\em
  Handbook of Logic in Computer Science}, volume~2, chapter~1, pages 1--116.
  Clarendon Press, Oxford, 1992.

\bibitem{KO90}
M.~Kurihara and A.~Ohuchi.
\newblock Modularity of simple termination of term rewriting systems.
\newblock {\em Journal of {IPS} {J}apan}, 31(5):633--642, 1990.

\bibitem{mLPTRS94}
M.~Marchiori.
\newblock Logic programs as term rewriting systems.
\newblock In G.~Levi and M.~Rodr\'{\i}guez-Artalejo, editors, {\em Proceedings
  of the Fourth International Conference on Algebraic and Logic Programming},
  volume 850 of {\em {LNCS}}, pages 223--241. {S}pringer--{V}erlag, 1994.

\bibitem{mJSC96}
M.~Marchiori.
\newblock On the modularity of normal forms in rewriting.
\newblock {\em Journal of Symbolic Computation}, 22(2):143--154, 1996.

\bibitem{mALP96}
M.~Marchiori.
\newblock Unravelings and ultra-properties.
\newblock In {\em Proceedings of the Fifth International Conference on
  Algebraic and Logic Programming (ALP'96)}, volume 1139 of {\em {LNCS}}, pages
  107--121. Springer--Verlag, 1996.

\bibitem{mFSTTCS97}
M.~Marchiori.
\newblock On the expressive power of rewriting.
\newblock In {\em Proceedings of the Seventeenth International Conference on
  the Foundations of Software Technology and Theoretical Computer Science
  (FST\&TCS')}, LNCS. Springer--Verlag, 1997.
\newblock In press.

\bibitem{mTCS98}
M.~Marchiori.
\newblock Bubbles in modularity.
\newblock {\em Theoretical Computer Science}, 192(1):31--54, 1998.

\bibitem{Mid89b}
A.~Middeldorp.
\newblock A sufficient condition for the termination of the direct sum of term
  rewriting systems.
\newblock In {\em Proceedings of the Fourth {IEEE} Symposium on Logic in
  Computer Science}, pages 396--401, 1989.

\bibitem{MH94}
A.~Middeldorp and E.~Hamoen.
\newblock Completeness results for basic narrowing.
\newblock {\em Applicable Algebra in Engineering, Communication and Computing},
  5:213--253, 1994.

\bibitem{Ohl94tcs}
E.~Ohlebusch.
\newblock On the modularity of termination of term rewriting systems.
\newblock {\em Theoretical Computer Science}, 136(2):333--360, 1994.

\bibitem{Ohl95}
E.~Ohlebusch.
\newblock Modular properties of composable term rewriting systems.
\newblock {\em Journal of Symbolic Computation}, 20(1):1--41, 1995.

\bibitem{Rao93}
K.~Rao.
\newblock Completeness of hierarchical combinations of term rewriting systems.
\newblock In {\em Proc.\ 13th FST\&TCS}, volume 761 of {\em {LNCS}}, pages
  125--139. Springer--Verlag, 1993.

\bibitem{Rao94}
K.~Rao.
\newblock Simple termination of hierarchical combinations of term rewriting
  systems.
\newblock In M.~Hagiya and J.C. Mitchell, editors, {\em Proc.\ TACS}, volume
  789 of {\em {LNCS}}, pages 203--223. Springer--Verlag, 1994.

\bibitem{RKS92}
K.~Rao, D.~Kapur, and R.K. Shyamasundar.
\newblock A transformational methodology for proving termination of logic
  programs.
\newblock In {\em Proceedings of the Fifth Conference on Computer Science
  Logic}, volume 626 of {\em {LNCS}}, pages 213--226, {B}erlin, 1992.
  {S}pringer--{V}erlag.

\bibitem{RV80}
K.-C. Raoult and J.~Vuillemin.
\newblock Operational and semantic equivalence between recursive programs.
\newblock {\em Journal of the {ACM}}, 27(4):772--796, 1980.

\bibitem{SS89}
M.~Schmidt-Schau\ss.
\newblock Unification in a combination of arbitrary disjoint equational
  theories.
\newblock {\em Journal of Symbolic Computation}, 8(1,2):51--99, 1989.

\bibitem{SSMP95}
M.~Schmidt-Schau\ss, M.~Marchiori, and S.E. Panitz.
\newblock Modular termination of r-consistent and left-linear term rewriting
  systems.
\newblock {\em Theoretical Computer Science}, 149(2):361--374, 1995.

\bibitem{SMI95}
T.~Suzuki, A.~Middeldorp, and T.~Ida.
\newblock Level-confluence of conditional rewrite systems with extra-variables
  in right-hand side.
\newblock In {\em Proceedings of the Sixth International Conference on
  Rewriting Techniques and Applications}, volume 914 of {\em {LNCS}}, pages
  179--193. Springer--Verlag, 1995.

\bibitem{Ver95}
R.M. Verma.
\newblock Unique normal forms and confluence of rewrite systems: Persistence.
\newblock In {\em Proc.\ 14th {IJCAI}}, volume~1, pages 362--368, 1995.

\end{thebibliography}
