\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Abramsky \bgroup\&al.\egroup
  }{1992}]{handbook-logic-in-computer-science}
S.~Abramsky, Dov Gabbay, and T.~S.~E. Maibaum, editors.
\newblock {\em Handbook of Logic in Computer \Sci}.
\newblock \clarendonpress, 1992.

\bibitem[\protect\citeauthoryear{A{\"\i}t-Kaci \bgroup\&\ \egroup
  Nivat}{1989}]{kaci-nivat}
Hassan A{\"\i}t-Kaci and Maurice Nivat, editors.
\newblock {\em Resolution of Equations in Algebraic Structures}.
\newblock \academicpress, 1989.

\bibitem[\protect\citeauthoryear{Avenhaus \bgroup\&\ \egroup
  Madlener}{1990}]{bossessurvey}
\juergen Avenhaus and Klaus Madlener.
\newblock Term rewriting and equational reasoning.
\newblock In R.~B. Banerji, editor, {\em Formal Techniques in Artificial
  Intelligence}, pages 1--43. {\elsevier}, 1990.

\bibitem[\protect\citeauthoryear{Bachmair \bgroup\&\ \egroup
  Ganzinger}{1991}]{bg}
Leo Bachmair and Harald Ganzinger.
\newblock Perfect model semantics for logic programs with equality.
\newblock 1991.
\newblock In \cite[\PP{645}{659}]{eighthCLP}.

\bibitem[\protect\citeauthoryear{Barendregt}{1984}]{lambda-calculus}
Hen(dri)k~P. Barendregt.
\newblock {\em The Lambda Calculus}.
\newblock \northholland, 1984.
\newblock \nth 2 \ed.

\bibitem[\protect\citeauthoryear{Becker}{1993}]{beckerctrs}
Klaus Becker.
\newblock {Semantics for \PNC\ Rewrite Systems}.
\newblock In {\em \thethirdCTRSninetytwo}, number 656 in Lecture Notes in
  Computer Science, pages 213--225. \springerverlag, 1993.

\bibitem[\protect\citeauthoryear{Bergstra \bgroup\&\ \egroup
  Klop}{1986}]{bergstraklop}
Jan~A. Bergstra and Jan~Willem Klop.
\newblock Conditional rewrite rules: Confluence and termination.
\newblock {\em \jcssname}, 32:323--362, 1986.

\bibitem[\protect\citeauthoryear{Bidoit \bgroup\&\ \egroup
  Hennicker}{2006}]{constructor-based-observational-logic}
Michel Bidoit and Rolf Hennicker.
\newblock Constructor-based observational logic.
\newblock {\em J. of Logic and Algebraic Programming}, 67:3--51, 2006.

\bibitem[\protect\citeauthoryear{Courcelle}{1984}]{ninthCAAPeightyfour}
Bruno Courcelle, editor.
\newblock {\em {\ninthCAAPeightyfourtitle}}. \cambridgeunipress, 1984.

\bibitem[\protect\citeauthoryear{Deemter \bgroup\&\ \egroup
  Peters}{1996}]{ambiguitycsli}
Kees~van Deemter and Stanley Peters, editors.
\newblock {\em Semantic Ambiguity and Underspecification}.
\newblock CLSI LN No.\,55, \Stanford, 1996.

\bibitem[\protect\citeauthoryear{Dershowitz \bgroup\&\ \egroup
  Jouannaud}{1990}]{term-rewriting-one}
Nachum Dershowitz and Jean-Pierre Jouannaud.
\newblock Rewrite systems.
\newblock 1990.
\newblock In \cite[\Vol\,B, \PP{243}{320}]{handbook-tcs}.

\bibitem[\protect\citeauthoryear{Furukawa}{1991}]{eighthCLP}
Koichi Furukawa, editor.
\newblock {\em {\eighthCLPtitle}}. \mitpress, 1991.

\bibitem[\protect\citeauthoryear{Gabbay \bgroup\&al.\egroup
  }{1993}]{handbooklogicailpvol1}
Dov Gabbay, Christopher~John Hogger, and J.~Alan
  Robinson\protect\index{Robinson, J. Alan}, editors.
\newblock {\em Handbook of Logic in Artificial Intelligence and Logic
  Programming. {\Vol\,1}: Logical Foundations}.
\newblock \clarendonpress, 1993.

\bibitem[\protect\citeauthoryear{Gentzen\protect\index{Gentzen!Gerhard}}{1938}%
]{gentzenconsistent}
Gerhard Gentzen\protect\index{Gentzen!Gerhard}.
\newblock {Die gegenw\ae rtige Lage in der mathematischen
  Grund\-lagen\-forschung -- Neue Fassung des Wider\-spruch\esi frei\-heit\esi
  beweise\es\ f\ue r die reine Zahlentheorie}.
\newblock {\em {Forschungen zur Logik und zur Grundlegung der exakten
  Wissenschaften, Neue Folge}}, 4:3--44, 1938.
\newblock {Reprinted as facsimile by
  \wissenschaftlichebuchgesellschaftdarmstadt, Verlag von S. Hirzel, Stuttgart.
  \ {English} translation in \cite{gentzen-collected}}.

\bibitem[\protect\citeauthoryear{Gentzen\protect\index{Gentzen!Gerhard}}{1969}%
]{gentzen-collected}
Gerhard Gentzen\protect\index{Gentzen!Gerhard}.
\newblock {\em The Collected Papers of \gentzenname}.
\newblock {\northholland}, 1969.
\newblock \Ed\ by \szaboname.

\bibitem[\protect\citeauthoryear{Gillman}{1987}]{writing-mathematics}
Leonard Gillman.
\newblock {\em Writing Mathematics Well}.
\newblock The Mathematical Association of America, 1987.

\bibitem[\protect\citeauthoryear{Gogolla}{1983}]{ordersorted}
Martin Gogolla.
\newblock {\em Algebraic Specifications with Partially Ordered Sorts and
  Declarations}.
\newblock \gruenereihe{1983}{169}, 1983.
\newblock Short version is \cite{ordersorted-conference}.

\bibitem[\protect\citeauthoryear{Gogolla}{1984}]{ordersorted-conference}
Martin Gogolla.
\newblock Partially ordered sorts in algebraic specifications.
\newblock 1984.
\newblock In \cite[\PP{139}{154}]{ninthCAAPeightyfour}. Long version is
  \cite{ordersorted}.

\bibitem[\protect\citeauthoryear{Hanu{\es}}{1994}]{hanus-extra-variables}
Micha{\"e}l Hanu{\es}.
\newblock {\em On Extra Variables in (Equational) Logic Programming}.
\newblock \mpireport{94}{246}, 1994.
\newblock Short version in \cite[\PP{665}{679}]{twelthCLP}.

\bibitem[\protect\citeauthoryear{Hanu{\es}}{2006}]{curry}
Micha{\"e}l Hanu{\es}.
\newblock {\CURRY\ --- an integrated functional logic language}.
\newblock Web only: \url{http://www.informatik.uni-kiel.de/~curry/report.html},
  2006.

\bibitem[\protect\citeauthoryear{Hobbs}{1996}]{hobbs}
Jerry~R. Hobbs.
\newblock Monotone decreasing quantifiers in a scope-free logical form.
\newblock 1996.
\newblock In \cite[\PP{55}{76}]{ambiguitycsli}.
  \url{http://www.isi.edu/~hobbs/monotone-decreasing.pdf}.

\bibitem[\protect\citeauthoryear{Hudlak \bgroup\&al.\egroup }{1999}]{haskell}
Paul Hudlak, John Peterson, and Joseph~H. Fasel.
\newblock A gentle introduction to {\HASKELL}.
\newblock Web only: \url{http://www.haskell.org/tutorial}, 1999.

\bibitem[\protect\citeauthoryear{Huet \bgroup\&\ \egroup
  Lankford}{1978}]{huet-lankford}
G{\'e}rard Huet and Dalla{\es}~S. Lankford.
\newblock {\em On the Uniform Halting Problem for Term Rewriting Systems}.
\newblock Rapport de Recherche 283, INRIA, 1978.
\newblock
  \url{http://www.ens-lyon.fr/LIP/REWRITING/OLD_PUBLICATIONS_ON_TERMINATION/HU%
ET_LANKFORD}.

\bibitem[\protect\citeauthoryear{Kaplan}{1988}]{kaplan}
St{\'e}phane Kaplan.
\newblock {\PNC\ Rewriting}.
\newblock In {\em \thefirstCTRSninetytwo}, number 308 in Lecture Notes in
  Computer Science, pages 129--143. \springerverlag, 1988.

\bibitem[\protect\citeauthoryear{K{\ue}hler \bgroup\&\ \egroup
  Wirth\protect\index{Wirth, Claus-Peter}}{1996}]{kwspec}
Ulrich K{\ue}hler and Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}.
\newblock {\em Conditional Equational Specifications of Data Types with Partial
  Operations for Inductive Theorem Proving}.
\newblock {SEKI-Report SR--1996--11 (ISSN 1437--4447)}. {SEKI Publications},
  Univ.\ Kaiserslautern, 1996.
\newblock Short version in 8th RTA 1997, LNCS 1232, {pp.\,38--52}, Springer.
  \url{http://www.ags.uni-sb.de/~cp/p/rta97}.

\bibitem[\protect\citeauthoryear{Klop}{1992}]{klophandbook}
Jan~Willem Klop.
\newblock Term rewriting systems.
\newblock 1992.
\newblock In \cite[\Vol\,II, \PP{1}{116}]{handbook-logic-in-computer-science}.

\bibitem[\protect\citeauthoryear{Leeuwen}{1990}]{handbook-tcs}
Jan~van Leeuwen, editor.
\newblock {\em Handbook of Theoretical Computer \Sci}.
\newblock \mitpress, 1990.

\bibitem[\protect\citeauthoryear{L{\"o}chner}{2006}]{loechner-lpo}
Bernd L{\"o}chner.
\newblock Things to know when implementing {LPO}.
\newblock {\em \artificialintelligencetools}, 15:53--79, 2006.

\bibitem[\protect\citeauthoryear{Nipkow \bgroup\&al.\egroup
  }{2000}]{isabelles-logics-hol}
Tobias Nipkow, Lawrence~C. Paulson, and Markus Wenzel.
\newblock {\ISABELLE's Logics: HOL}.
\newblock Web only: \url{http://isabelle.in.tum.de/PSV2000/doc/logics-HOL.pdf},
  2000.

\bibitem[\protect\citeauthoryear{Nipkow \bgroup\&al.\egroup
  }{2002}]{isabellehol}
Tobias Nipkow, Lawrence~C. Paulson, and Markus Wenzel.
\newblock {\em {\ISABELLEHOL\ --- A Proof Assistant for Higher-Order Logic}}.
\newblock Number 2283 in Lecture Notes in Computer Science. \springerverlag,
  2002.

\bibitem[\protect\citeauthoryear{Padawitz}{1988}]{padawitz-springer}
Peter Padawitz.
\newblock {\em Computing in Horn Clause Theories}.
\newblock \springerverlag, 1988.

\bibitem[\protect\citeauthoryear{Padawitz}{2000}]{padawitz-tcs}
Peter Padawitz.
\newblock Swinging types = functions + relations + transition systems.
\newblock {\em \tcsname}, 243:93--165, 2000.

\bibitem[\protect\citeauthoryear{Plaisted}{1993}]{plaisted-survey}
David Plaisted.
\newblock Equational reasoning and term rewriting systems.
\newblock 1993.
\newblock In \cite[\PP{273}{364}]{handbooklogicailpvol1}.

\bibitem[\protect\citeauthoryear{Ro{\c s}u}{2003}]{rosu-inductive-unhiding}
Grigore Ro{\c s}u.
\newblock Inductive behavioral proofs by unhiding.
\newblock {\em \ENTCSname}, 82:285--302, 2003.
\newblock \url{http://dx.doi.org/10.1016/S1571-0661(04)80645-5}. Revised
  version is \cite{rosu-inductive-unhiding-tcs}.

\bibitem[\protect\citeauthoryear{Ro{\c s}u}{2004}]{rosu-inductive-unhiding-tcs}
Grigore Ro{\c s}u.
\newblock Behavioral abstraction is hiding information.
\newblock {\em \tcsname}, 327:197--221, 2004.
\newblock \url{http://dx.doi.org/10.1016/j.tcs.2004.07.027}. Preliminary
  version is \cite{rosu-inductive-unhiding}.

\bibitem[\protect\citeauthoryear{Slind}{1996}]{slind-recursion}
Konrad Slind.
\newblock Function definition in higher-order logic.
\newblock In {\em {\nth 9 TPHOLs 1996}}, number 1125 in Lecture Notes in
  Computer Science, pages 381--397. \springerverlag, 1996.

\bibitem[\protect\citeauthoryear{Smoka \bgroup\&al.\egroup
  }{1989}]{ordersortedtwo}
Gerd Smoka, Werner Nutt, \goguenname, and \meseguername.
\newblock Order-sorted equational computation.
\newblock 1989.
\newblock In \cite[\Vol\,2, \PP{297}{367}]{kaci-nivat}.

\bibitem[\protect\citeauthoryear{Sterling}{1991}]{twelthCLP}
Leon Sterling, editor.
\newblock {\em {\twelvethCLPtitle}}. \mitpress, 1991.

\bibitem[\protect\citeauthoryear{Suzuki \bgroup\&al.\egroup }{1995}]{suzuki}
Taro Suzuki, Aart Middeldorp, and Tetsuo Ida.
\newblock Level-confluence of conditional rewrite systems with extra variables
  in right-hand sides.
\newblock In {\em \thesixthRTAninetyfive}, number 914 in Lecture Notes in
  Computer Science, pages 179--193. \springerverlag, 1995.

\bibitem[\protect\citeauthoryear{Waldmann}{1989a}]{compordersorted}
Uwe Waldmann.
\newblock {\em Semantics of Order-Sorted Specifications}.
\newblock \gruenereihe{1989}{297}, 1989.
\newblock Revised version in \tcsjournalprintyear{1992}{94}{1}{35}.

\bibitem[\protect\citeauthoryear{Waldmann}{1989b}]{unitary-order-sorted}
Uwe Waldmann.
\newblock {\em Unification in Order-Sorted Signatures}.
\newblock \gruenereihe{1989}{298}, 1989.
\newblock Revised version 1990,
  \url{http://www.mpi-sb.mpg.de/~uwe/paper/UNIDO-INF-298.dvi.gz}.

\bibitem[\protect\citeauthoryear{Wirth\protect\index{Wirth, Claus-Peter}
  \bgroup\&\ \egroup Gramlich\protect\index{Gramlich, Bernhard}}{1994a}]{wgjsc}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter} and Bernhard
  Gramlich\protect\index{Gramlich, Bernhard}.
\newblock A constructor-based approach for positive/negative-conditional
  equational specifications.
\newblock {\em \jscname}, 17:51--90, 1994.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/jsc94}.

\bibitem[\protect\citeauthoryear{Wirth\protect\index{Wirth, Claus-Peter}
  \bgroup\&\ \egroup Gramlich\protect\index{Gramlich,
  Bernhard}}{1994b}]{wgcade}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter} and Bernhard
  Gramlich\protect\index{Gramlich, Bernhard}.
\newblock On notions of inductive validity for first-order equational clauses.
\newblock In Alan Bundy, editor, {\em {\thetwelvethCADEninetyfour}}, number 814
  in Lecture Notes in Artificial Intelligence, pages 162--176. \springerverlag,
  1994.
\newblock {\url{www.ags.uni-sb.de/~cp/p/cade94}}.

\bibitem[\protect\citeauthoryear{Wirth\protect\index{Wirth, Claus-Peter}
  \bgroup\&\ \egroup Lunde}{1994}]{wirthlunde}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter} and R{\"udiger}~Lunde.
\newblock {\em Writing Positive/Negative-Conditional Equations Conveniently}.
\newblock {SEKI-Report SR--1994--04 (ISSN 1437--4447)}. {SEKI Publications},
  Univ.\ Kaiserslautern, 1994.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/swp9404}.

\bibitem[\protect\citeauthoryear{Wirth\protect\index{Wirth,
  Claus-Peter}}{1997}]{wirthdiss}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}.
\newblock {\em Positive/Negative-Conditional Equations: A Constructor-Based
  Framework for Specification and Inductive Theorem Proving}, volume~31 of {\em
  {Schriftenreihe Forschungsergebnisse zur Informatik}}.
\newblock {Verlag Dr.\ Kova\v c, Hamburg}, {Arnoldstr.\,49, D--27763 Hamburg},
  1997.
\newblock {ISBN 3--86064--551--X}, {\url{www.ags.uni-sb.de/~cp/p/diss}}.

\bibitem[\protect\citeauthoryear{Wirth\protect\index{Wirth,
  Claus-Peter}}{2006}]{swp200601}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}.
\newblock {\em Progress in Computer-Assisted Inductive Theorem Proving by
  Human-Orientedness and Descente Infinie?}
\newblock {SEKI-Working-Paper SWP--2006--01 (ISSN 1860--5931)}. {SEKI
  Publications}, Saarland Univ., 2006.
\newblock {\url{www.ags.uni-sb.de/~cp/p/swp200601/welcome.html}}.

\bibitem[\protect\citeauthoryear{Wirth\protect\index{Wirth,
  Claus-Peter}}{2009}]{wirth-jsc}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}.
\newblock Shallow confluence of conditional term rewriting systems.
\newblock {\em \jscname}, 44:69--98, 2009.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/shallow},
  \url{http://dx.doi.org/10.1016/j.jsc.2008.05.005}.

\end{thebibliography}
