\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Avenhaus \bgroup\&al.\egroup
  }{2003}]{quodlibet-cade}
\juergen\ Avenhaus, Ulrich K{\ue}hler, Tobias Schmidt-Samoa, and Claus-Peter
  Wirth\protect\index{Wirth, Claus-Peter}.
\newblock How to prove inductive theorems? {\QUODLIBET}!
\newblock In {\em {\thenineteenthCADEthree}}, number 2741 in Lecture Notes in
  Artificial Intelligence, pages 328--333. \springerverlag, 2003.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/quodlibet}.

\bibitem[\protect\citeauthoryear{Baaz \bgroup\&al.\egroup
  }{1997}]{leaninduction}
Matthias Baaz, Uwe Egly, and {\mbox{Ch}}ristian~G. Ferm{\ue ller}.
\newblock Lean induction principles for tableaus.
\newblock In Didier Galmiche, editor, {\em \thesixthTABLEAUninetyseven}, number
  1227 in Lecture Notes in Artificial Intelligence, pages 62--75.
  \springerverlag, 1997.

\bibitem[\protect\citeauthoryear{Boyer \bgroup\&\ \egroup Moore}{1979}]{bm}
Robert~S. Boyer and J~S. Moore.
\newblock {\em A Computational Logic}.
\newblock \academicpress, 1979.

\bibitem[\protect\citeauthoryear{Bundy}{1999}]{bundy-survey}
Alan Bundy.
\newblock {\em The Automation of Proof by Mathematical Induction}.
\newblock Informatics Research Report \Numero\,2, Division of Informatics,
  \uniEBshort, 1999.
\newblock Also in \cite[\Vol\,1, \PP{845}{911}]{handbookAR}.

\bibitem[\protect\citeauthoryear{Enderton}{1972}]{enderton}
Herbert~B. Enderton.
\newblock {\em A Mathematical Introduction to Logic}.
\newblock {\academicpress}, 1972.

\bibitem[\protect\citeauthoryear{Gabbay \bgroup\&al.\egroup
  }{1994}]{handbooklogicailpvol2}
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\,2}: Deduction Methodologies}.
\newblock \oxfordunipress, 1994.

\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 \nth 8 RTA 1997, LNCS 1232, {pp.\,38--52}, Springer.
  \url{http://www.ags.uni-sb.de/~cp/p/rta97}.

\bibitem[\protect\citeauthoryear{Miller}{1992}]{miller}
Dale~A. Miller.
\newblock Unification under a mixed prefix.
\newblock {\em \jscname}, 14:321--358, 1992.

\bibitem[\protect\citeauthoryear{Robinson\protect\index{Robinson, J. Alan}
  \bgroup\&\ \egroup Voronkow}{2001}]{handbookAR}
Alan Robinson\protect\index{Robinson, J. Alan} and Andrei Voronkow, editors.
\newblock {\em Handbook of Automated Reasoning}.
\newblock {\elsevier}, 2001.

\bibitem[\protect\citeauthoryear{Walther}{1994}]{waltherhandbook}
Christoph Walther.
\newblock Mathematical induction.
\newblock 1994.
\newblock In \cite[\PP{127}{228}]{handbooklogicailpvol2}.

\bibitem[\protect\citeauthoryear{Wirth\protect\index{Wirth,
  Claus-Peter}}{2004}]{wirthcardinal}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}.
\newblock {\DescenteInfinie\ + Deduction}.
\newblock {\em Logic J. of the IGPL}, 12:1--96, 2004.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/d}.

\bibitem[\protect\citeauthoryear{Wirth\protect\index{Wirth,
  Claus-Peter}}{2008}]{wirth-jal}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}.
\newblock \hilbert's epsilon as an operator of indefinite committed choice.
\newblock {\em J. Applied Logic\protect\index{Hilbert!'s epsilon}}, 6:287--317,
  2008.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/epsi},
  \url{http://dx.doi.org/10.1016/j.jal.2007.07.009}.

\end{thebibliography}
