\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Anon}{2004}]{lics/2004}
Anon, editor.
\newblock {\em \nth{19} IEEE Symposium on Logic in Computer Science (LICS
  2004), Turku, Finland}. IEEE Computer Society, 2004.

\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{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{Dershowitz \bgroup\&al.\egroup
  }{2009}]{dershowitz-wirth}
Nachum Dershowitz, Bernhard Gramlich\protect\index{Gramlich, Bernhard},
  \okadaname, \sivakumarname, and Claus-Peter Wirth\protect\index{Wirth,
  Claus-Peter}.
\newblock Conditional confluence.
\newblock In preparation, 2009.

\bibitem[\protect\citeauthoryear{Gabbay \bgroup\&\ \egroup
  Cheney}{2004}]{lics/GabbayC04}
Murdoch~J. Gabbay and James Cheney.
\newblock A sequent calculus for nominal logic.
\newblock 2004.
\newblock In \cite[\PP{139}{148}]{lics/2004}.

\bibitem[\protect\citeauthoryear{Gabbay \bgroup\&\ \egroup
  Mathijssen}{2007}]{wollic/GabbayM07}
Murdoch~J. Gabbay and Aad Mathijssen.
\newblock A formal calculus for informal equality with binding.
\newblock 2007.
\newblock In \cite[\PP{162}{176}]{wollic/2007}.

\bibitem[\protect\citeauthoryear{Gabbay \bgroup\&\ \egroup
  Mathijssen}{2008}]{fac/GabbayM08}
Murdoch~J. Gabbay and Aad Mathijssen.
\newblock Capture-avoiding substitution as a nominal algebra.
\newblock {\em Formal Asp. Comput.}, 20:451--479, 2008.
\newblock \url{http://dx.doi.org/10.1007/s00165-007-0056-1}.

\bibitem[\protect\citeauthoryear{Gabbay \bgroup\&\ \egroup
  Pitts}{2002}]{fac/GabbayP02}
Murdoch~J. Gabbay and Andrew~M. Pitts.
\newblock A new approach to abstract syntax with variable binding.
\newblock {\em Formal Asp. Comput.}, 13:341--363, 2002.

\bibitem[\protect\citeauthoryear{Gabbay \bgroup\&al.\egroup
  }{2010\ff}]{hilbert-bernays-project}
Dov Gabbay, J{\oe}rg Siek{\-}mann\protect\index{Siekmann, J\"org}, and
  Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}.
\newblock {\hilbertbernaysproject}.
\newblock {\url{http://www.ags.uni-sb.de/~cp/p/hilbertbernays/goal.htm}},
  2010\ff.

\bibitem[\protect\citeauthoryear{Gabbay}{2009}]{tcs/Gabbay09}
Murdoch~J. Gabbay.
\newblock A study of substitution, using nominal techniques and
  {\fraenkel--\mostowski} sets.
\newblock {\em \tcsname}, 410:1159--1189, 2009.
\newblock \url{http://dx.doi.org/10.1016/j.tcs.2008.11.013}.

\bibitem[\protect\citeauthoryear{Gramlich\protect\index{Gramlich, Bernhard}
  \bgroup\&\ \egroup Wirth\protect\index{Wirth, Claus-Peter}}{1996}]{gwrta}
Bernhard Gramlich\protect\index{Gramlich, Bernhard} and Claus-Peter
  Wirth\protect\index{Wirth, Claus-Peter}.
\newblock Confluence of terminating conditional term rewriting systems
  revisited.
\newblock In {\em \theseventhRTAninetysix}, number 1103 in Lecture Notes in
  Computer Science, pages 245--259. \springerverlag, 1996.

\bibitem[\protect\citeauthoryear{K{\ue}hler}{2000}]{kuehlerdiss}
Ulrich K{\ue}hler.
\newblock {\em A Tactic-Based Inductive Theorem Prover for Data Types with
  Partial Operations}.
\newblock \infixverlag, 2000.
\newblock \PhDthesis, \url{http://www.ags.uni-sb.de/~cp/p/kuehlerdiss}.

\bibitem[\protect\citeauthoryear{Leivant \bgroup\&\ \egroup
  Queiroz}{2007}]{wollic/2007}
Daniel Leivant and Ruy J. G. B.~de Queiroz, editors.
\newblock {\em Logic, Language, Information and Computation, \nth{14}
  International Workshop, WoLLIC 2007, Rio de Janeiro}, number 4576 in Lecture
  Notes in Computer Science. \springerverlag, 2007.

\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{Schmidt-Samoa}{2006a}]{samoacalculemus}
Tobias Schmidt-Samoa.
\newblock An even closer integration of linear arithmetic into inductive
  theorem proving.
\newblock {\em \ENTCSname}, 151:3--20, 2006.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/evencloser},
  \url{http://dx.doi.org/10.1016/j.entcs.2005.11.020}.

\bibitem[\protect\citeauthoryear{Schmidt-Samoa}{2006b}]{samoa-phd}
Tobias Schmidt-Samoa.
\newblock {\em Flexible Heuristic Control for Combining Automation and
  User-Interaction in Inductive Theorem Proving}.
\newblock PhD thesis, \uniKLshort, 2006.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/samoadiss}.

\bibitem[\protect\citeauthoryear{Schmidt-Samoa}{2006c}]{jancl}
Tobias Schmidt-Samoa.
\newblock Flexible heuristics for simplification with conditional lemmas by
  marking formulas as forbidden, mandatory, obligatory, and generous.
\newblock {\em Journal of Applied Non-Classical Logics}, 16:209--239, 2006.
\newblock \url{http://dx.doi.org/10.3166/jancl.16.208-239}.

\bibitem[\protect\citeauthoryear{Wirth\protect\index{Wirth, Claus-Peter}
  \bgroup\&\ \egroup Gramlich\protect\index{Gramlich, Bernhard}}{1994}]{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}}{2002}]{wirthhilbertepsilon}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}.
\newblock A new indefinite semantics for {\hilbert's} epsilon.
\newblock In Uwe Egly and {\mbox{Ch}}ristian~G. Ferm{\ue ller}, editors, {\em
  \theeleventhTABLEAUtwo}, number 2381 in Lecture Notes in Artificial
  Intelligence, pages 298--314. {\springerverlag}\index{Hilbert!'s epsilon},
  2002.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/epsi}.

\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}}{2006}]{wirth-hilbert-seki}
Claus-Peter Wirth\protect\index{Wirth, Claus-Peter}.
\newblock {\em \hilbert's epsilon as an Operator of Indefinite Committed
  Choice}.
\newblock {SEKI-Report SR--2006--02 (ISSN 1437--4447)}. {SEKI Publications},
  Saarland Univ., 2006.
\newblock {\url{http://arxiv.org/abs/0902.3749},
  \url{http://www.ags.uni-sb.de/~cp/p/epsi}}.

\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://dx.doi.org/10.1016/j.jal.2007.07.009},
  \url{http://www.ags.uni-sb.de/~cp/p/epsi}.

\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://dx.doi.org/10.1016/j.jsc.2008.05.005}.

\end{thebibliography}