\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Asser}{1957}]{asserepsilon}
G{\"u}nter Asser.
\newblock {Theorie der logischen Au\esi wahl\-funk\-tionen}.
\newblock {\em \ZLGname}, 3:30--68, 1957.

\bibitem[\protect\citeauthoryear{Asser}{1990}]{asserpeano}
G{\"u}nter Asser, editor.
\newblock {\em {\peanoname\ --- Arbeiten zur Analysi\es\ und zur mathematischen
  Logik}}.
\newblock Number~13 in \teubner-Archiv zur Mathe\-ma\-tik. \teubnerverlag,
  1990.

\bibitem[\protect\citeauthoryear{Berka \bgroup\&\ \egroup
  Kreiser}{1973}]{logiktexte}
Karel Berka and Lothar Kreiser, editors.
\newblock {\em {Logik-Texte -- Kommentierte Au\esi wahl zur Geschichte der
  modernen Logik}}.
\newblock Akademie-Verlag, \Berlin, 1973.
\newblock \nth 2\,\rev\,\ed\ (\nth 1\,\ed\,1971; \nth
  4\,\rev\,\rev\,\ed\,1986).

\bibitem[\protect\citeauthoryear{Bibel \bgroup\&\ \egroup
  Schmitt}{1998}]{deduction}
Wolfgang Bibel and Peter~H. Schmitt, editors.
\newblock {\em Automated Deduction --- A Basis for Applications}.
\newblock \kluwer, 1998.

\bibitem[\protect\citeauthoryear{Caferra \bgroup\&\ \egroup
  Salzer}{2000}]{ftpwien}
Ricardo Caferra and Gernot Salzer, editors.
\newblock {\em Automated Deduction in Classical and Non-Classical Logics}.
\newblock Number 1761 in Lecture Notes in Artificial Intelligence.
  \springerverlag, 2000.

\bibitem[\protect\citeauthoryear{Clocksin \bgroup\&\ \egroup
  Mellish}{2003}]{Prolog}
William~F. Clocksin and Christopher~S. Mellish.
\newblock {\em {Programming in \PROLOG}}.
\newblock \springerverlag, 2003.
\newblock \nth 5\,\ed\ (\nth 1\,\ed\,1981).

\bibitem[\protect\citeauthoryear{Fitting}{1996}]{fitting}
Melvin Fitting.
\newblock {\em First-order logic and automated theorem proving}.
\newblock \springerverlag, 1996.
\newblock \nth 2\,\rev\,\ed\ (\nth 1\,\ed\,1990).

\bibitem[\protect\citeauthoryear{Frege\protect\index{Frege,
  Gottlob}}{1893/1903}]{frege-grundgesetze}
Gottlob Frege\protect\index{Frege, Gottlob}.
\newblock {\em Grundgesetze der Arithmetik --- \Begriffsschrift lich
  abgeleitet}.
\newblock Verlag von \hermann\ Pohle, \Jena, 1893/1903.
\newblock As facsimile with corrigenda by \christian\ Thiel: \georg\ Olms
  Verlag, \Hildesheim, 1998. English translation:
  \cite{frege-grundgesetze-furth}.

\bibitem[\protect\citeauthoryear{Frege\protect\index{Frege,
  Gottlob}}{1964}]{frege-grundgesetze-furth}
Gottlob Frege\protect\index{Frege, Gottlob}.
\newblock {\em The Basic Laws of Arithmetic}.
\newblock \Univ\ of California Press, 1964.
\newblock English translation of \cite{frege-grundgesetze}, with an
  introduction, by {\namefont Montgomery Furth}.

\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{Gentzen}{1935}]{gentzen}
Gerhard Gentzen.
\newblock {Untersuchungen \ue ber das logische Schlie\sz en}.
\newblock {\em Mathematische Zeitschrift}, 39:176--210,405--431, 1935.
\newblock Also in \cite[\PP{192}{253}]{logiktexte}. {English} translation in
  \cite{gentzen-collected}.

\bibitem[\protect\citeauthoryear{Gentzen}{1969}]{gentzen-collected}
Gerhard Gentzen.
\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{Hermes}{1965}]{hermesepsilon}
Hans Hermes.
\newblock {\em {Eine Termlogik mit Au\esi wahl\-opera\-tor}}.
\newblock Number~6 in LNM. \springerverlag, 1965.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}
  \bgroup\&\ \egroup Bernays\protect\index{Bernays,
  Paul}}{1934}]{grundlagen-first-edition-volume-one}
David Hilbert\protect\index{Hilbert!David} and Paul
  Bernays\protect\index{Bernays, Paul}.
\newblock {\em {Die Grundlagen der Mathematik --- Erster Band}}.
\newblock Number~XL in {Die Grundlehren der Mathematischen Wissenschaften in
  Einzeldarstellungen}. \springerverlag, 1934.
\newblock \nth 1\,\ed\ (\nth 2\,\ed\ is
  \cite{grundlagen-second-edition-volume-one}).

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}
  \bgroup\&\ \egroup Bernays\protect\index{Bernays,
  Paul}}{1939}]{grundlagen-first-edition-volume-two}
David Hilbert\protect\index{Hilbert!David} and Paul
  Bernays\protect\index{Bernays, Paul}.
\newblock {\em {Die Grundlagen der Mathematik --- Zweiter Band}}.
\newblock Number~L in {Die Grundlehren der Mathematischen Wissenschaften in
  Einzeldarstellungen}. \springerverlag, 1939.
\newblock \nth 1\,\ed\ (\nth 2\,\ed\ is
  \cite{grundlagen-second-edition-volume-two}).

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}
  \bgroup\&\ \egroup Bernays\protect\index{Bernays,
  Paul}}{1968}]{grundlagen-second-edition-volume-one}
David Hilbert\protect\index{Hilbert!David} and Paul
  Bernays\protect\index{Bernays, Paul}.
\newblock {\em {Die Grundlagen der Mathematik~I}}.
\newblock Number~40 in {Die Grundlehren der Mathematischen Wissenschaften in
  Einzeldarstellungen}. \springerverlag, 1968.
\newblock \nth 2\,\rev\,\ed\ of \cite{grundlagen-first-edition-volume-one}.

\bibitem[\protect\citeauthoryear{Hilbert\protect\index{Hilbert!David}
  \bgroup\&\ \egroup Bernays\protect\index{Bernays,
  Paul}}{1970}]{grundlagen-second-edition-volume-two}
David Hilbert\protect\index{Hilbert!David} and Paul
  Bernays\protect\index{Bernays, Paul}.
\newblock {\em {Die Grundlagen der Mathematik~II}}.
\newblock Number~50 in {Die Grundlehren der Mathematischen Wissenschaften in
  Einzeldarstellungen}. \springerverlag, 1970.
\newblock \nth 2\,\rev\,\ed\ of \cite{grundlagen-first-edition-volume-two}.

\bibitem[\protect\citeauthoryear{Hintikka}{1974}]{hintikkaquantification}
K.~Jaakko~J. Hintikka.
\newblock Quantifiers {\vs} quantification theory.
\newblock {\em \linguisticinquiryname}, V(2):153--177, 1974.

\bibitem[\protect\citeauthoryear{Hintikka}{1996}]{hintikkaprinciples}
K.~Jaakko~J. Hintikka.
\newblock {\em The Principles of Mathematics Revisited}.
\newblock {\cambridgeunipress}, 1996.

\bibitem[\protect\citeauthoryear{Kanger}{1963}]{kanger}
Stig Kanger.
\newblock A simplified proof method for elementary logic.
\newblock 1963.
\newblock In \cite[\Vol\,1, \PP{364}{371}]{siekmannwrightson}.

\bibitem[\protect\citeauthoryear{Kennedy}{1973}]{kennedypeanoworks}
Hubert~C. Kennedy.
\newblock {\em Selected works of {\peanoname}}.
\newblock \allenandunwin, 1973.

\bibitem[\protect\citeauthoryear{Kohlhase}{1998}]{kohlhasetableauupdated}
Micha{\"e}l Kohlhase.
\newblock Higher-order automated theorem proving.
\newblock 1998.
\newblock In \cite[\Vol\,1, \PP{431}{462}]{deduction}.

\bibitem[\protect\citeauthoryear{Leisenring}{1969}]{leisenring}
\leisenringfirstname Leisenring.
\newblock {\em Mathematical Logic and {\hilbertsepsilon}-Symbol}.
\newblock Gordon and Breach, New York, 1969.

\bibitem[\protect\citeauthoryear{Mattick \bgroup\&\ \egroup
  Wirth}{1999}]{productmodel}
Volker Mattick and Claus-Peter Wirth.
\newblock An algebraic {Dexter}-based hypertext reference model.
\newblock Research Report (green/grey series) 719/1999, FB Informatik, {Univ.\
  Dortmund}, 1999.
\newblock \url{http://www.ags.uni-sb.de/~cp/p/gr719},
  \url{http://arxiv.org/abs/0902.3648}.

\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{Peano}{1884}]{peanogenocchi}
Guiseppe Peano, editor.
\newblock {\em {Angelo Genocchi} --- Calcolo differenziale e principii di
  calcolo integrale}.
\newblock Fratelli Bocca, \Torino, 1884.
\newblock German translation: \cite{peanogenocchigerman}.

\bibitem[\protect\citeauthoryear{Peano}{1896\f}]{peanoiotabar}
Guiseppe Peano.
\newblock Studii di logica matematica.
\newblock {\em \AttiAccadTorinoname}, 32:565--583, 1896\f.
\newblock Also in
  \AttiAccadTorinoFisicheMatematicheNaturali{1896\f}{32}{361}{397}. English
  translation\emph{Studies in Mathematical Logic} in
  \cite[\PP{190}{205}]{kennedypeanoworks}. German translation:
  \cite{peanoiotabargerman}.

\bibitem[\protect\citeauthoryear{Peano}{1899a}]{peanogenocchigerman}
Guiseppe Peano, editor.
\newblock {\em {Angelo Genocchi --- Differentialrechnung und Grund\-z\ue ge der
  Integral\-rechnung}}.
\newblock \teubnerverlag, \Leipzig, 1899.
\newblock German translation of \cite{peanogenocchi}.

\bibitem[\protect\citeauthoryear{Peano}{1899b}]{peanoiotabargerman}
Guiseppe Peano.
\newblock {\Ue ber mathematische Logik}.
\newblock 1899.
\newblock German translation of \cite{peanoiotabar}. In
  \cite[Appendix\,1]{peanogenocchigerman}. Facsimile also in
  \cite[\PP{10}{26}]{asserpeano}.

\bibitem[\protect\citeauthoryear{Prawitz}{1960}]{prawitzimproved}
Dag Prawitz.
\newblock An improved proof procedure.
\newblock {\em Theoria: A Swedish Journal of Philosophy}, 26:102--139, 1960.
\newblock Also in \cite[\Vol\,1, \PP{159}{199}]{siekmannwrightson}.

\bibitem[\protect\citeauthoryear{Quine}{1981}]{ML}
Willard Van~O. Quine.
\newblock {\em Mathematical Logic}.
\newblock \harvardunipress, 1981.
\newblock \nth 4\,\rev\,\ed\ (\nth 1\,\ed\ 1940).

\bibitem[\protect\citeauthoryear{Russell\protect\index{Russell!Bertrand}}{1905%
}]{denoting}
Bertrand Russell\protect\index{Russell!Bertrand}.
\newblock On denoting.
\newblock {\em \mindname}, 14:479--493, 1905.

\bibitem[\protect\citeauthoryear{Russell\protect\index{Russell!Bertrand}}{1919%
}]{mathematicalphilosophy}
Bertrand Russell\protect\index{Russell!Bertrand}.
\newblock {\em Introduction to Mathematical Philosophy}.
\newblock {\allenandunwin}, 1919.

\bibitem[\protect\citeauthoryear{Schmidt-Samoa}{2006}]{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{Siek{\-}mann\protect\index{Siekmann, J\"org}
  \bgroup\&\ \egroup Wrightson}{1983}]{siekmannwrightson}
J{\"o}rg Siek{\-}mann\protect\index{Siekmann, J\"org} and Graham Wrightson,
  editors.
\newblock {\em Automation of Reasoning}.
\newblock \springerverlag, 1983.

\bibitem[\protect\citeauthoryear{Smullyan}{1968}]{smullyan}
Raymond~M. Smullyan.
\newblock {\em First-Order Logic}.
\newblock \springerverlag, 1968.

\bibitem[\protect\citeauthoryear{Urban \bgroup\&al.\egroup
  }{2004}]{gabbay:nomu-jv}
Christian Urban, Murdoch~J. Gabbay, and Andrew~M. Pitts.
\newblock Nominal unification.
\newblock {\em \tcsname}, 323:473--497, 2004.

\bibitem[\protect\citeauthoryear{Wallen}{1990}]{wallen}
Lincoln~A. Wallen.
\newblock {\em Automated Proof Search in Non-Classical Logics}.
\newblock MIT Press, 1990.

\bibitem[\protect\citeauthoryear{Whitehead \bgroup\&\ \egroup
  Russell\protect\index{Russell!Bertrand}}{1910--1913}]{PM}
Alfred~North Whitehead and Bertrand\protect\index{Principia Mathematica}
  Russell\protect\index{Russell!Bertrand}.
\newblock {\em Principia Mathematica}.
\newblock {\cambridgeunipress}, 1910--1913.
\newblock {\nth 1\,\ed}.

\bibitem[\protect\citeauthoryear{Wirth}{1998}]{wirthgreen}
Claus-Peter Wirth.
\newblock Full first-order sequent and tableau calculi with preservation of
  solutions and the liberalized {$\delta$}-rule but without {Skolemization}.
\newblock Research Report (green/grey series) 698/1998, FB Informatik, {Univ.\
  Dortmund}, 1998.
\newblock \url{http://arxiv.org/abs/0902.3730}. Short version in \salzername,
  \caferraname\ (\eds). \Proc\ \nth 2\,\Int\ Workshop on First-Order Theorem
  Proving (FTP'98), \PP{244}{255}, \Tech\ \Univ\ Vienna, 1998. Short version
  also in \cite[\PP{283}{298}]{ftpwien}.

\bibitem[\protect\citeauthoryear{Wirth}{2002}]{wirthhilbertepsilon}
Claus-Peter Wirth.
\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}{2004}]{wirthcardinal}
Claus-Peter Wirth.
\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}{2006}]{nonpermut}
Claus-Peter Wirth.
\newblock {\em {$\lim$$+$}, {$\delta^+$}, and Non-Permutability of
  {$\beta$}-Steps}.
\newblock {SEKI-Report SR--2005--01 (ISSN 1437--4447)}. {SEKI Publications},
  Saarland Univ., 2006.
\newblock \Rev\,\ed, \url{http://arxiv.org/abs/0902.3635}. Thoroughly improved
  version is \cite{wirth-jsc-non-permut}.

\bibitem[\protect\citeauthoryear{Wirth}{2008}]{wirth-jal}
Claus-Peter Wirth.
\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}.

\bibitem[\protect\citeauthoryear{Wirth}{2010}]{wirth-hilbert-seki}
Claus-Peter Wirth.
\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., 2010.
\newblock \Rev\,\ed\ {\url{http://arxiv.org/abs/0902.3749}}.

\bibitem[\protect\citeauthoryear{Wirth}{2011}]{wirth-jsc-non-permut}
Claus-Peter Wirth.
\newblock {\math{\lim\tight+}, \math{\delta^+}, and \NonPermutability\ of
  \math\beta-Steps}.
\newblock {\em {\jscname}}, 2011.
\newblock To appear. More funny version is \cite{nonpermut}.

\bibitem[\protect\citeauthoryear{Wittgenstein\protect\index{Wittgenstein,
  Ludwig}}{1939}]{wittgenstein}
Ludwig Wittgenstein\protect\index{Wittgenstein, Ludwig}.
\newblock {\em Lectures on the Foundations of Mathematics, \Cambridge}.
\newblock \Univ\ of \Chicago\ Press, copyright 1989, 1939.
\newblock {Cora Diamond} (\ed), from the notes of {R. G. Bosanquet}, {Norman
  Malcolm}, {Rush Rhees}, and {Yorick Smythies}.

\end{thebibliography}
