\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Ackermann\protect\ackermannindex}{1925}]{acke%
rmann-1925}
Wilhelm Ackermann\protect\ackermannindex, 1925.
\newblock {Begr\ue ndung des \glqq tertium non datur\grqq\ mittel\es\ der
  \hilbert\-schen Theorie der Widerspruch\esi freiheit}.
\newblock {\em {\MathematischeAnnalen}}, 93:1--36.
\newblock Received \Mar\,30, 1924. Inauguraldissertation, 1924, \Goettingen.

\bibitem[\protect\citeauthoryear{Ackermann\protect\ackermannindex}{1938}]{acke%
rmann-mengentheoretische-Begruendung}
Wilhelm Ackermann\protect\ackermannindex, 1938.
\newblock {Mengen\-theoreti\-sche Be\-gr\ue n\-dung der Logik}.
\newblock {\em {\MathematischeAnnalen}}, 115:1--22.
\newblock Received \Apr\,23, 1937.

\bibitem[\protect\citeauthoryear{Ackermann\protect\ackermannindex}{1940}]{acke%
rmann-consistency-of-arithmetic}
Wilhelm Ackermann\protect\ackermannindex, 1940.
\newblock {Zur Wider\-spruch\esi frei\-heit der Zahlen\-theorie}.
\newblock {\em {\MathematischeAnnalen}}, 117:163--194.
\newblock Received \Aug\,15, 1939.

\bibitem[\protect\citeauthoryear{Anon}{1899}]{anon-1899}
Anon, editor, 1899.
\newblock {\em {Festschrift zur Feier der Enth\ue llung des\/
  \gauss-\weber-Denkmals in \Goettingen, herau\esi gegeben von dem
  Fest-Comitee.}}
\newblock Verlag von B. G. Teubner, \Leipzig.

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

\bibitem[\protect\citeauthoryear{Bell{\protectedbellindex}}{1993a}]{bellclassi%
calepsilon}
John~Lane Bell{\protectedbellindex}, 1993a.
\newblock {\hilbert's \math\varepsilon-Operator and Classical Logic}.
\newblock {\em \jphillogicname}, 22:1--18.

\bibitem[\protect\citeauthoryear{Bell{\protectedbellindex}}{1993b}]{bellintuit%
ionisticepsilon}
John~Lane Bell{\protectedbellindex}, 1993b.
\newblock {\hilbert's \math\varepsilon-Operator in Intuitionistic Type
  Theories}.
\newblock {\em \mathematicallogicquarterlyname}, 39:323--337.

\bibitem[\protect\citeauthoryear{Bell{\protectedbellindex} \bgroup\&al.\egroup
  }{2001}]{logicaloptions}
John~Lane Bell{\protectedbellindex}, David DeVidi, and Graham Solomon, 2001.
\newblock {\em Logical Options: An Introduction to Classical and Alternative
  Logics}.
\newblock Broadview Press.

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

\bibitem[\protect\citeauthoryear{Bibel \bgroup\&\ \egroup
  Schmitt}{1998}]{deduction}
Wolfgang Bibel and Peter~H. Schmitt, editors, 1998.
\newblock {\em Automated Deduction --- A Basis for Applications}.
\newblock Number 8--10 in Applied Logic Series. \kluwer.
\newblock \Vol\,I: Foundations --- Calculi and Methods. \Vol\,II: Systems and
  Implementation Techniques. \Vol\,III: Applications.

\bibitem[\protect\citeauthoryear{Blass \bgroup\&\ \egroup
  Gurevich}{2000}]{logicofchoice}
Andreas Blass and Yuri Gurevich, 2000.
\newblock The logic of choice.
\newblock {\em {\jslname}}, 65:1264--1310.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1939\ff}]{%
bourbaki}
Nicola{\es} Bourbaki{\protectedbourbakiindex}, 1939\ff.
\newblock {\em {\'El\'ements des Math\'ematique} --- Livres\,1--9}.
\newblock \hermannparisseries. \hermannparis.

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

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

\bibitem[\protect\citeauthoryear{DeVidi}{1995}]{vext}
David DeVidi, 1995.
\newblock Intuitionistic {\math\varepsilon}- and {\math\tau}-calculi.
\newblock {\em \mathematicallogicquarterlyname}, 41:523--546.

\bibitem[\protect\citeauthoryear{Diamond{\protectedwittgensteinindex}}{1976}]{%
wittgenstein-lectures-foundations-of-mathematics}
Cora Diamond{\protectedwittgensteinindex}, editor, 1976.
\newblock {\em {\wittgenstein's Lectures on the Foundations of Mathematics,
  \Cambridge, 1939}}.
\newblock Cornell \Univ, Ithaca (NY).
\newblock From the notes of {\namefont R. G. Bosanquet}, {\namefont Norman
  Malcolm}, {\rheesname}, and {\namefont Yorick Smythies}. German translation
  is \cite{wittgenstein-lectures-diamond}.

\bibitem[\protect\citeauthoryear{Diamond{\protectedwittgensteinindex}}{1978}]{%
wittgenstein-lectures-diamond}
Cora Diamond{\protectedwittgensteinindex}, editor, 1978.
\newblock {\em {\wittgenstein s Vorlesungen \ue ber die
  \grundlagendermathematiknoindex, \Cambridge, 1939}}.
\newblock {\suhrkampverlagfrankfurt}.
\newblock {German translation of
  \cite{wittgenstein-lectures-foundations-of-mathematics} by {\namefont Joachim
  Schulte}. \nth 1\,\edn\ as ``\wittgensteinname, Schriften\,7''
  (ISBN\,3518072471)\@. Note that this volume was excluded from the later
  Suhrkamp \edn\ ``\wittgensteinname, Werkau\esi gabe''.}

\bibitem[\protect\citeauthoryear{Egly \bgroup\&\ \egroup Ferm{\ue
  ller}}{2002}]{eleventhTABLEAUtwo}
Uwe Egly and {\mbox{Ch}}ristian~G. Ferm{\ue ller}, editors, 2002.
\newblock {\em {\theeleventhTABLEAUtwo}}, number 2381 in Lecture Notes in
  Artificial Intelligence. {\springerverlag}.

\bibitem[\protect\citeauthoryear{Ewald}{1996}]{ewald-1996}
William Ewald, editor, 1996.
\newblock {\em From {\kant} to {\hilbert} --- A source book in the foundations
  of mathematics}.
\newblock {\oxfordunipress}.

\bibitem[\protect\citeauthoryear{Fitting}{1975}]{fittingepsilon}
Melvin Fitting, 1975.
\newblock A modal logic {\math\varepsilon}-calculus.
\newblock {\em \notredamename}, XVI:1--16.

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

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

\bibitem[\protect\citeauthoryear{Fitting}{1999}]{fittingquantifiedmodal}
Melvin Fitting, 1999.
\newblock On quantified modal logic.
\newblock {\em \fundamentainformaticaename}, 39:105--121.

\bibitem[\protect\citeauthoryear{Frege\protectedfregeindex}{1893/1903}]{frege-%
grundgesetze}
Gottlob Frege\protectedfregeindex, 1893/1903.
\newblock {\em {Grundgesetze der Arithmetik --- \Begriffsschrift lich
  abgeleitet}}.
\newblock Verlag von \hermann\ Pohle, \Jena.
\newblock \Vol\,I/II\@. As facsimile with corrigenda by {\namefont\christian\
  Thiel}: \olmsverlag, 1998. English translations:
  \cite{frege-grundgesetze-furth}, \cite{frege-grundgesetze-ebert}.

\bibitem[\protect\citeauthoryear{Frege\protectedfregeindex}{1964}]{frege-grund%
gesetze-furth}
Gottlob Frege\protectedfregeindex, 1964.
\newblock {\em The Basic Laws of Arithmetic --- Exposition of the System}.
\newblock \Univ\ of California Press.
\newblock English translation of \cite[Vol\,I]{frege-grundgesetze}, with an
  introduction, by {\namefont Montgomery Furth}.

\bibitem[\protect\citeauthoryear{Frege\protectedfregeindex}{2013}]{frege-grund%
gesetze-ebert}
Gottlob Frege\protectedfregeindex, 2013.
\newblock {\em Basic Laws of Arithmetic}.
\newblock {\oxfordunipress}.
\newblock English translation of \cite{frege-grundgesetze} by {\namefont Philip
  Ebert} and {\namefont Marcus Rossberg}, with an Introduction by {\namefont
  Crispin Wright} and an appendix by {\namefont Roy T. Cook}.

\bibitem[\protect\citeauthoryear{Fried}{2012}]{fried-canossa}
Johanne{\es} Fried, 2012.
\newblock {\em Canossa -- Entlarvung einer Legende. Eine Streitschrift}.
\newblock \akademieverlag.

\bibitem[\protect\citeauthoryear{Gabbay{\protectedgabbayindex}}{1981}]{intuiti%
onisticsemantics}
Dov Gabbay{\protectedgabbayindex}, 1981.
\newblock {\em Semantical Investigations in {\heyting}'s Intuitionistic Logic}.
\newblock \kluwer.

\bibitem[\protect\citeauthoryear{Gabbay{\protectedgabbayindex} \bgroup\&\
  \egroup Woods}{2004\ff}]{handbook-of-the-history-of-logic}
Dov Gabbay{\protectedgabbayindex} and John Woods, editors, 2004\ff.
\newblock {\em Handbook of the History of Logic}.
\newblock \northholland.

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

\bibitem[\protect\citeauthoryear{Gentzen{\protectedgentzenindex}}{1935}]{gentz%
en}
Gerhard Gentzen{\protectedgentzenindex}, 1935.
\newblock {Untersuchungen \ue ber das logische Schlie\sz en}.
\newblock {\em Mathematische Zeitschrift}, 39:176--210,405--431.
\newblock Also in \cite[\PP{192}{253}]{logiktexte}. {English} translation in
  \cite{gentzen-collected}.

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

\bibitem[\protect\citeauthoryear{Giese \bgroup\&\ \egroup
  Ahrendt}{1999}]{ahrendtgiese}
Martin Giese and Wolfgang Ahrendt, 1999.
\newblock {\hilbert's \math\varepsilon}-terms in automated theorem proving.
\newblock In \cite[\PP{171}{185}]{eighthTABLEAUninetynine}.

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

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1971}]%
{heijenoort-source-book}
Jean~van Heijenoort{\protectedheijenoortindex}, 1971.
\newblock {\em From {\frege} to {\namefont G\"odel}: A Source Book in
  Mathematical Logic, 1879--1931}.
\newblock {\harvardunipress}.
\newblock {\nth 2\,\rev\ \edn\ (\nth 1\,\edn\,1967)}.

\bibitem[\protect\citeauthoryear{Hermes}{1965}]{hermesepsilon}
Hans Hermes, 1965.
\newblock {\em {Eine Termlogik mit Au\esi wahl\-opera\-tor}}.
\newblock Number~6 in LNM. {\springerverlag}.

\bibitem[\protect\citeauthoryear{Heusinger}{1997}]{heusingerepsilon}
Klaus~von Heusinger, 1997.
\newblock {\em {Salienz und Referenz --- Der Epsilonoperator in der Semantik
  der Nominalphrase und anaphorischer Pronomen}}.
\newblock Number~43 in Studia gram\-ma\-tica. \akademieverlag.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1899}]{grund%
lagen-der-geometrie}
David Hilbe{\protectedhilbertindex}rt, 1899.
\newblock {\grundlagendergeometrienoindex}.
\newblock In \cite[\PP{1}{92}]{anon-1899}. \nth 1\,\edn\ without \appendixes.
  Reprinted in \cite[\PP{436}{525}]{hilbert-2004}\bibcrit{Last edition of
  ``\grundlagendergeometrienoindex'' by \hilbert\ is
  \cite{grundlagen-der-geometrie-siebte}, which is also most complete regarding
  the appendixes. Last three editions by\/ \bernaysname\ are
  \makeaciteofthree{grundlagen-der-geometrie-neunte}{grundlagen-der-geometrie-%
zehnte}{grundlagen-der-geometrie-elfte}, which are also most complete regarding
  supplements and figures. Its first appearance as a separate book was the
  French translation \cite{principes-fondamentaux-de-la-geometrie}. Two
  substantially different {English} translations are
  \cite{foundations-of-geometry} and \cite{foundations-of-geometry-second}}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1900a}]{hilb%
ert-zahlbegriff}
David Hilbe{\protectedhilbertindex}rt, 1900a.
\newblock {\Ue ber den Zahlbegriff}.
\newblock {\em \dmvjahresberichtname}, 8:180--184.
\newblock Received \Dec\,1899. Reprinted as {Appendix\,VI} of
  \makeaciteoffive{grundlagen-der-geometrie-dritte}{grundlagen-der-geometrie-v%
ierte}{grundlagen-der-geometrie-fuenfte}{grundlagen-der-geometrie-sechste}{gru%
ndlagen-der-geometrie-siebte}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1900b}]{prin%
cipes-fondamentaux-de-la-geometrie}
David Hilbe{\protectedhilbertindex}rt, 1900b.
\newblock Les principes fondamentaux de la g{\'e}om{\'e}trie.
\newblock {\em Annales Scientifiques de l'\EcoleNormaleSuperieure},
  S\'erie\,3,\,17:103--209.
\newblock {French} translation by {\namefont L\'eonce Laugel} of special
  version of \cite{grundlagen-der-geometrie}, revised and authorized by
  \hilbert. Also in published as a separate book by the same publisher
  (\gauthiervillars).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1902}]{found%
ations-of-geometry}
David Hilbe{\protectedhilbertindex}rt, 1902.
\newblock {\em The Foundations of Geometry}.
\newblock Open Court, \Chicago.
\newblock {English} translation by {\namefont E. J. Townsend} of special
  version of \cite{grundlagen-der-geometrie}, revised and authorized by
  \hilbert, \url{http://www.gutenberg.org/etext/17384}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1903}]{grund%
lagen-der-geometrie-zweite}
David Hilbe{\protectedhilbertindex}rt, 1903.
\newblock {\em {\grundlagendergeometrienoindex. --- Zweite, durch Zus\ae tze
  vermehrte und mit f\ue nf Anh\ae ngen versehene Au\fli age. Mit zahlreichen
  in den Text gedruckten Figuren}}.
\newblock Druck und Verlag von B. G. Teubner, \Leipzig.
\newblock {\nth 2}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\ and \extd\ with five \appendixes, newly added figures, and an index of
  notion names.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1905}]{hilbe%
rt-grundlagen-logik}
David Hilbe{\protectedhilbertindex}rt, 1905.
\newblock {\Ue ber die Grundlagen der Logik und der Arithmetik}.
\newblock In \cite[\PP{174}{185}]{dritter-mathematiker}. \ Reprinted as
  {Appendix\,VII} of
  \makeaciteoffive{grundlagen-der-geometrie-dritte}{grundlagen-der-geometrie-v%
ierte}{grundlagen-der-geometrie-fuenfte}{grundlagen-der-geometrie-sechste}{gru%
ndlagen-der-geometrie-siebte}. \ {English} translation {\em On the foundations
  of logic and arithmetic} by {\namefont Beverly Woodward} with an introduction
  by \heijenoortname\ in \cite[\PP{129}{138}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1909}]{grund%
lagen-der-geometrie-dritte}
David Hilbe{\protectedhilbertindex}rt, 1909.
\newblock {\em {\grundlagendergeometrienoindex. --- Dritte, durch Zus\ae tze
  und Literaturhinweise von neuem vermehrte und mit sieben Anh\ae ngen
  versehene Au\fli age. Mit zahlreichen in den Text gedruckten Figuren.}}
\newblock Number VII in Wissenschaft und Hypothese. Druck und Verlag von B. G.
  Teubner, \Leipzig, \Berlin.
\newblock {\nth 3}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-zweite}, \extd\ with a
  bibliography and two additional \appendixes\ (now seven in total)
  (Appendix\,VI: \cite{hilbert-zahlbegriff}) (Appendix\,VII:
  \cite{hilbert-grundlagen-logik}).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1913}]{grund%
lagen-der-geometrie-vierte}
David Hilbe{\protectedhilbertindex}rt, 1913.
\newblock {\em {\grundlagendergeometrienoindex. --- Vierte, durch Zus\ae tze
  und Literaturhinweise von neuem vermehrte und mit sieben Anh\ae ngen
  versehene Au\fli age. Mit zahlreichen in den Text gedruckten Figuren.}}
\newblock Druck und Verlag von B. G. Teubner, \Leipzig, \Berlin.
\newblock {\nth 4}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-dritte}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1922}]{grund%
lagen-der-geometrie-fuenfte}
David Hilbe{\protectedhilbertindex}rt, 1922.
\newblock {\em {\grundlagendergeometrienoindex. --- F\ue nfte, durch Zus\ae tze
  und Literatur\-hinweise von neuem vermehrte und mit sieben Anh\ae ngen
  versehene Au\fli age. Mit zahl\-reichen in den Text gedruckten Figuren}}.
\newblock Verlag und Druck von B. G. Teubner, \Leipzig, \Berlin.
\newblock {\nth 5}\,\extd\,\edn\,of \cite{grundlagen-der-geometrie}. \ Contrary
  to what the sub-title may suggest, this is an anastatic reprint of
  \cite{grundlagen-der-geometrie-vierte}, extended by a very short preface on
  the changes \wrt\ \cite{grundlagen-der-geometrie-vierte}, and with
  augmentations to Appendix\,II, Appendix\,III, and \litchapref{IV},
  \litsectref{21}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1923a}]{logi%
schegrundlagen}
David Hilbe{\protectedhilbertindex}rt, 1923a.
\newblock {Die logischen Grund\-lagen der Mathematik}.
\newblock {\em {\MathematischeAnnalen}}, 88:151--165.
\newblock Received \Sep\,29, 1922. Talk given at the Deutsche
  Natur\-forscher\-gesellschaft in \Leipzig, \Sep\,1922. {English} translation
  in \cite[\PP{1134}{1148}]{ewald-1996}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1923b}]{grun%
dlagen-der-geometrie-sechste}
David Hilbe{\protectedhilbertindex}rt, 1923b.
\newblock {\em {\grundlagendergeometrienoindex. --- Sechste unver\ae nderte
  Au\fli age. Anastati\-scher Nachdruck. Mit zahlreichen in den Text gedruckten
  Figuren}}.
\newblock Verlag und Druck von B. G. Teubner, \Leipzig, \Berlin.
\newblock {\nth 6}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  anastatic reprint of \cite{grundlagen-der-geometrie-fuenfte}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1926}]{unend%
liche}
David Hilbe{\protectedhilbertindex}rt, 1926.
\newblock {\Ue ber da\es\ Unendliche --- Vortrag, gehalten am 4.\,Juni\,1925
  gelegentlich einer zur Ehrung de\es\ Andenken\es\ an \weierstrass\ von der
  West\-f\ae lischen \Math\ \Ges\ veranstalteten Mathematiker-Zusammenkunft in
  M\ue nster i. W.}
\newblock {\em {\MathematischeAnnalen}}, 95:161--190.
\newblock Received \Jun\,24, 1925. \ Reprinted as Appendix\,VIII of
  \cite{grundlagen-der-geometrie-siebte}. \ {E}nglish translation {\em On the
  infinite} by \bauermengelbergname\ with an introduction by \heijenoortname\
  in \cite[\PP{367}{392}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1928}]{grund%
lagenvortrag}
David Hilbe{\protectedhilbertindex}rt, 1928.
\newblock {Die \grundlagendermathematiknoindex\ --- Vortrag, gehalten auf
  Einladung des Mathematischen Seminars im Juli 1927 in \Hamburg}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 6:65--85.
\newblock Reprinted as Appendix\,IX of \cite{grundlagen-der-geometrie-siebte}.
  \ {E}nglish translation {\em The foundations of mathematics}\/ by
  \bauermengelbergname\protect\ and \foellesdalname\ with a short introduction
  by \heijenoortname\ in \cite[\PP{464}{479}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1930a}]{prob%
leme-grundlegung}
David Hilbe{\protectedhilbertindex}rt, 1930a.
\newblock {Probleme der Grundlegung der Mathematik}.
\newblock {\em {\MathematischeAnnalen}}, 102:1--9.
\newblock {Vortrag gehalten auf dem Internationalen Mathematiker-Kongre\sz\ in
  \Bologna, \Sep\,3, 1928}. \ Received March\,25, 1929. \ Reprinted as
  Appendix\,X of \cite{grundlagen-der-geometrie-siebte}. \ Short version in
  {\em Atti del congresso internationale dei matematici, \Bologna, 3--10
  settembre 1928}, \Vol\,1, \PP{135}{141}, Bologna, 1929.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1930b}]{grun%
dlagen-der-geometrie-siebte}
David Hilbe{\protectedhilbertindex}rt, 1930b.
\newblock {\em {\grundlagendergeometrienoindex. --- Siebente umgearbeitete und
  vermehrte Au\fli age. Mit 100 in den Text gedruckten Figuren}}.
\newblock Verlag und Druck von B. G. Teubner, \Leipzig, \Berlin.
\newblock {\nth 7}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  thoroughly revised edition of \cite{grundlagen-der-geometrie-sechste}, \extd\
  with three new \appendixes\ (now ten in total) (Appendix\,VIII:
  \cite{unendliche}) (Appendix\,IX: \cite{grundlagenvortrag}) (Appendix\,X:
  \cite{probleme-grundlegung}).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1956}]{grund%
lagen-der-geometrie-achte}
David Hilbe{\protectedhilbertindex}rt, 1956.
\newblock {\em {\grundlagendergeometrienoindex. --- Achte Au\fli age, mit
  Revisionen und Erg\ae nzungen von \Dr\ \bernaysname. Mit 124 Abbildungen}}.
\newblock B. G. Teubner Verlag\esi gesellschaft, \Stuttgart.
\newblock {\nth 8}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-siebte}, omitting \appendixes\
  VI--X, \extd\ by \bernaysname, now with 24 additional figures and 3
  additional supplements.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1962}]{grund%
lagen-der-geometrie-neunte}
David Hilbe{\protectedhilbertindex}rt, 1962.
\newblock {\em {\grundlagendergeometrienoindex. --- Neunte Au\fli age,
  revidiert und erg\ae nzt von \Dr\ \bernaysname. Mit 129 Abbildungen}}.
\newblock B. G. Teubner Verlag\esi gesellschaft, \Stuttgart.
\newblock {\nth 9}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-achte}, \extd\ by \bernaysname,
  now with 129\,figures, 5\,\appendixes, and 8\,supplements (I\,1, I\,2, II,
  III, IV\,1, IV\,2, V\,1, V\,2).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1968}]{grund%
lagen-der-geometrie-zehnte}
David Hilbe{\protectedhilbertindex}rt, 1968.
\newblock {\em {\grundlagendergeometrienoindex. --- Zehnte Au\fli age,
  revidiert und erg\ae nzt von \Dr\ \bernaysname. Mit 124 Abbildungen}}.
\newblock B. G. Teubner Verlag\esi gesellschaft, \Stuttgart.
\newblock {\nth{10}}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-neunte} by \bernaysname.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1971}]{found%
ations-of-geometry-second}
David Hilbe{\protectedhilbertindex}rt, 1971.
\newblock {\em The Foundations of Geometry}.
\newblock Open Court, \Chicago\ and La Salle (IL).
\newblock Newly translated and fundamentally different \nth 2\,\edn\,of
  \cite{foundations-of-geometry}, actually an English translation of
  \cite{grundlagen-der-geometrie-zehnte} by {\namefont Leo Unger}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{1972}]{grund%
lagen-der-geometrie-elfte}
David Hilbe{\protectedhilbertindex}rt, 1972.
\newblock {\em {\grundlagendergeometrienoindex. --- 11.\,Au\fli age. Mit
  Supplementen von \Dr\ \bernaysname}}.
\newblock B. G. Teubner Verlag\esi gesellschaft, \Stuttgart.
\newblock {\nth{11}}\,\rev\,\extd\,\edn\,of \cite{grundlagen-der-geometrie},
  \rev\,\edn\,of \cite{grundlagen-der-geometrie-zehnte} by \bernaysname.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt}{2004}]{hilbe%
rt-2004}
David Hilbe{\protectedhilbertindex}rt, 2004.
\newblock {\em {\hilbertname}'s Lectures on the Foundations of Geometry,
  1891--1902}.
\newblock {\springerverlag}.
\newblock \Ed\ by \hallettname\ and \majername.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup Ackermann\protect\ackermannindex}{1928}]{grundzuege}
David Hilbe{\protectedhilbertindex}rt and Wilhelm
  Ackermann\protect\ackermannindex, 1928.
\newblock {\em {Grundz\ue ge der theoretischen Logik}}.
\newblock Number XXVII in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 1\,\edn, the final version in a serious of three thorough
  revisions is \cite{grundzuege-vierte}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup Ackermann\protect\ackermannindex}{1938}]{grundzuege-zweite}
David Hilbe{\protectedhilbertindex}rt and Wilhelm
  Ackermann\protect\ackermannindex, 1938.
\newblock {\em {Grundz\ue ge der theoretischen Logik}}.
\newblock Number XXVII in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 2\,\edn, most thoroughly revised edition of \cite{grundzuege}.
  {English} translation is \cite{grundzuege-zweite-english}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup Ackermann\protect\ackermannindex}{1949}]{grundzuege-dritte}
David Hilbe{\protectedhilbertindex}rt and Wilhelm
  Ackermann\protect\ackermannindex, 1949.
\newblock {\em {Grundz\ue ge der theoretischen Logik}}.
\newblock Number~27 in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 3\,\edn\ of \cite{grundzuege}, thoroughly revised edition of
  \cite{grundzuege-zweite}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup Ackermann\protect\ackermannindex}{1950}]{grundzuege-zweite-english}
David Hilbe{\protectedhilbertindex}rt and Wilhelm
  Ackermann\protect\ackermannindex, 1950.
\newblock {\em {Principles of Mathematical Logic}}.
\newblock Chelsea, \NewYork.
\newblock English translation of \cite{grundzuege-zweite} by {\sc Lewis M.
  Hammond}, {\sc George G. Leckie}, and {\sc F. Steinhardt}, \ed\ and annotated
  by {\sc Robert E. Luce}. Reprinted by \AMSname\ 1999.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup Ackermann\protect\ackermannindex}{1959}]{grundzuege-vierte}
David Hilbe{\protectedhilbertindex}rt and Wilhelm
  Ackermann\protect\ackermannindex, 1959.
\newblock {\em {Grundz\ue ge der theoretischen Logik}}.
\newblock Number~27 in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 4\,\edn\ of \cite{grundzuege}, most thoroughly revised and
  \extd\ edition of \cite{grundzuege-dritte}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1934}]{grundlagen-first-edition-volume-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex},
  1934.
\newblock {\em {\grundlagendermathematiknoindex\ --- \mbox{Erster} Band}}.
\newblock Number~XL in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 1\,\edn\ (\nth 2\,\edn\ is
  \cite{grundlagen-second-edition-volume-one}). Reprinted by J.\,W.\,Edwards
  \Publ, Ann Arbor (MI), 1944. English translation is
  \makeaciteoftwo{grundlagen-german-english-edition-volume-one-one}{grundlagen%
-german-english-edition-volume-one-two}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1939}]{grundlagen-first-edition-volume-two}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex},
  1939.
\newblock {\em {\grundlagendermathematiknoindex\ --- \mbox{Zweiter} Band}}.
\newblock Number~L in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 1\,\edn\ (\nth 2\,\edn\ is
  \cite{grundlagen-second-edition-volume-two}). Reprinted by J.\,W.\,Edwards
  \Publ, Ann Arbor (MI), 1944.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1968}]{grundlagen-second-edition-volume-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex},
  1968.
\newblock {\em {\grundlagendermathematiknoindex~I}}.
\newblock Number~40 in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 2\,\rev\,\edn\,of \cite{grundlagen-first-edition-volume-one}.
  English translation is
  \makeaciteoftwo{grundlagen-german-english-edition-volume-one-one}{grundlagen%
-german-english-edition-volume-one-two}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{1970}]{grundlagen-second-edition-volume-two}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex},
  1970.
\newblock {\em {\grundlagendermathematiknoindex~II}}.
\newblock Number~50 in {\seriesgrundlehrendermathematischenwissenschaften}.
  {\springerverlag}.
\newblock \nth 2\,\rev\,\extd\,\edn\,of
  \cite{grundlagen-first-edition-volume-two}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{2017a}]{grundlagen-german-english-edition-v%
olume-one-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex},
  2017a.
\newblock {\em {\grundlagendermathematiknoindex~I --- Foundations of
  Mathematics~I, Part\,A: \whatisinVolIPartA}}.
\newblock {\springerverlag}.
\newblock First English translation and bilingual facsimile \edn\ of the \nth 2
  German \edn\ \cite{grundlagen-second-edition-volume-one}, \incl\ the
  annotation and translation of all differences of the \nth 1 German \edn\
  \cite{grundlagen-first-edition-volume-one}. \ \Ed\ by \wirthname,
  \siekmannname, \peckhausname, \michaelgabbayname, \gabbayname. \ Translated
  and commented by \wirthname\ \etalabbrev\ Thoroughly \rev\ \nth 3\,\edn\
  (\nth 1\,\edn\ \collegepublications, 2011; \nth 2\,\edn\
  \url{http://wirth.bplaced.net/p/hilbertbernays}, 2013).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays{\protectedbernaysindex}}{2017b}]{grundlagen-german-english-edition-v%
olume-one-two}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays{\protectedbernaysindex},
  2017b.
\newblock {\em {\grundlagendermathematiknoindex~I --- Foundations of
  Mathematics~I, Part\,B: \whatisinVolIPartB}}.
\newblock {\springerverlag}.
\newblock First English translation and bilingual facsimile \edn\ of the \nth 2
  German \edn\ \cite{grundlagen-second-edition-volume-one}, \incl\ the
  annotation and translation of all deleted texts of the \nth 1 German \edn\
  \cite{grundlagen-first-edition-volume-one}. \ \Ed\ by \wirthname,
  \siekmannname, \peckhausname, \michaelgabbayname, \gabbayname. \ Translated
  and commented by \wirthname\ \etalabbrev\ Thoroughly \rev\ \nth 3\,\edn\
  (\nth 1\,\edn\ \collegepublications, 2012; \nth 2\,\edn\
  \url{http://wirth.bplaced.net/p/hilbertbernays}, 2013).

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

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

\bibitem[\protect\citeauthoryear{Howard{\protectedhowardindex} \bgroup\&\
  \egroup Rubin{\protectedrubinsheindex}}{1998}]{weakaxiomofchoice}
Paul Howard{\protectedhowardindex} and Jean~E. Rubin{\protectedrubinsheindex},
  1998.
\newblock {\em Consequences of the Axiom of Choice}.
\newblock \AMSname.
\newblock \url{http://consequences.emich.edu/conseq.htm}.

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

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

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

\bibitem[\protect\citeauthoryear{Kowalski{\protectedkowalskiindex}}{1974}]{Kow%
74}
Robert~A. Kowalski{\protectedkowalskiindex}, 1974.
\newblock Predicate logic as a programming language.
\newblock In \cite[\PP{569}{574}]{IFIP-1974}.

\bibitem[\protect\citeauthoryear{Krazer}{1905}]{dritter-mathematiker}
A.~Krazer, editor, 1905.
\newblock {\em {Verhandlungen des Dritten Internationalen
  Mathematiker-Kongresses, Heidelberg, \Aug\,8--13, 1904}}. Verlag von B. G.
  Teubner, \Leipzig.

\bibitem[\protect\citeauthoryear{Lambert}{1764}]{lambert-1764}
Johann~Heinrich Lambert, 1764.
\newblock {\em {Neues Organon oder Gedanken \ue ber die Erforschung und
  Bezeichnung des Wahren und dessen Unterscheidung von Irrthum und Schein.}}
\newblock Johann Wendler, \Leipzig.
\newblock {\Vol\,I\ (Dianoiologie oder die Lehre von den Gesetzen de\es\
  Denken\es, Alethiologie oder Lehre von der Wahrheit)
  (\url{http://books.google.de/books/about/Neues_Organon_oder_Gedanken_Uber_di%
e_Erf.html?id=ViS3XCuJEw8C}) \& \Vol\,II (Semiotik oder Lehre von der
  Bezeichnung der Gedanken und Dinge, Ph{\"a}nomenologie oder Lehre von dem
  Schein)
  (\url{http://books.google.de/books/about/Neues_Organon_oder_Gedanken_%C3%BCb%
er_die_Er.html?id=X8UAAAAAcAAj})\@. \ Facsimile reprint by \olmsverlag, 1965,
  with a German introduction by \hanswernerarndtname}.

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

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

\bibitem[\protect\citeauthoryear{Meyer-Viol}{1995}]{meyervioldiss}
Wil\-fried P.~M. Meyer-Viol, 1995.
\newblock {\em Instantial Logic --- An Investigation into Reasoning with
  Instances}.
\newblock PhD thesis, \Univ\ Utrecht.
\newblock ILLC dissertation series 1995--11.

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

\bibitem[\protect\citeauthoryear{Murray}{1999}]{eighthTABLEAUninetynine}
Neil~V. Murray, editor, 1999.
\newblock {\em {\theeighthTABLEAUninetynine}}, number 1617 in Lecture Notes in
  Artificial Intelligence. {\springerverlag}.

\bibitem[\protect\citeauthoryear{Peano{\protect\peanoindex}}{1884}]{peanogenoc%
chi}
Guiseppe Peano{\protect\peanoindex}, editor, 1884.
\newblock {\em {Angelo Genocchi} --- Calcolo differenziale e principii di
  calcolo integrale}.
\newblock Fratelli Bocca, \Torino.
\newblock German translation: \cite{peanogenocchigerman}.

\bibitem[\protect\citeauthoryear{Peano{\protect\peanoindex}}{1890}]{peanoiota}
Guiseppe Peano{\protect\peanoindex}, 1890.
\newblock {D\'emonstration de l'int\'egrabilit\'e des \'equations
  diff\'erentielles ordinaires}.
\newblock {\em {\MathematischeAnnalen}}, 37:182--228.
\newblock Facsimile also in \cite[\PP{76}{122}]{asserpeano}.

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

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

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

\bibitem[\protect\citeauthoryear{Peano{\protect\peanoindex}}{1990}]{asserpeano}
Guiseppe Peano{\protect\peanoindex}, 1990.
\newblock {\em {\peanoname\ --- Arbeiten zur Analysi\es\ und zur mathematischen
  Logik}}.
\newblock Number~13 in \teubner-Archiv zur Mathe\-ma\-tik. \teubnerverlag.
\newblock With an essay by \assername\ (\ed).

\bibitem[\protect\citeauthoryear{Pinkal \bgroup\&al.\egroup
  }{2001}]{dialogprojectantrag}
Manfred Pinkal, J{\"o}rg Siek{\-}mann{\protect\siekmannindex}, and
  {\mbox{Ch}}ristoph Benz{\-}m{\ue}ller{\protectedbenzmuellerindex}, 2001.
\newblock {Teilprojekt \mbox{MI\,3: DIALOG}: Tutorieller Dialog mit einem
  Mathematik-Assistenten}.
\newblock In \oursfbshort\ \oursfbname, Proposal \Jan\,2002 - \Dez\,2004,
  \uniSBshort.

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

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

\bibitem[\protect\citeauthoryear{Rosenfeld}{1974}]{IFIP-1974}
Jack~L. Rosenfeld, editor, 1974.
\newblock {\em {\Proc\ of the Congress of the \Int\ Federation for Information
  Processing (IFIP), Stockholm (Sweden), \Aug\,5--10, 1974}}. \northholland.

\bibitem[\protect\citeauthoryear{Rubin{\protectedrubinheindex} \bgroup\&\
  \egroup Rubin{\protectedrubinsheindex}}{1985}]{axiomofchoice}
Herman Rubin{\protectedrubinheindex} and Jean~E.
  Rubin{\protectedrubinsheindex}, 1985.
\newblock {\em Equivalents of the {Axiom of Choice}}.
\newblock {\northholland}.
\newblock \nth 2\,\rev\,\edn\ (\nth 1\,\edn\,1963).

\bibitem[\protect\citeauthoryear{Russe{\protectedrussellindex}ll}{1905}]{denot%
ing}
Bertrand Russe{\protectedrussellindex}ll, 1905.
\newblock {\denotingtitle}.
\newblock {\em \mindname}, 14:479--493.

\bibitem[\protect\citeauthoryear{Russe{\protectedrussellindex}ll}{1919}]{mathe%
maticalphilosophy}
Bertrand Russe{\protectedrussellindex}ll, 1919.
\newblock {\em Introduction to Mathematical Philosophy}.
\newblock {\allenandunwin}.

\bibitem[\protect\citeauthoryear{Schmidt-Samoa{\protectedsamoaindex}}{2006}]{j%
ancl}
Tobias Schmidt-Samoa{\protectedsamoaindex}, 2006.
\newblock Flexible heuristics for simplification with conditional lemmas by
  marking formulas as forbidden, mandatory, obligatory, and generous.
\newblock {\em \janclname}, 16:209--239.
\newblock \url{http://dx.doi.org/10.3166/jancl.16.208-239}.

\bibitem[\protect\citeauthoryear{Siek{\-}mann{\protect\siekmannindex}
  \bgroup\&\ \egroup Wrightson}{1983}]{siekmannwrightson}
J{\"o}rg Siek{\-}mann{\protect\siekmannindex} and Graham Wrightson, editors,
  1983.
\newblock {\em Automation of Reasoning}.
\newblock {\springerverlag}.

\bibitem[\protect\citeauthoryear{Slater{\protectedslaterindex}}{1994}]{slater-%
intensional-logic}
B.~Hartley Slater{\protectedslaterindex}, 1994.
\newblock {\em {Intensional Logic --- an essay in analytical metaphysics}}.
\newblock Avebury Series in Philosophy. Ashgate Publ.\ Ltd (Taylor \& Francis),
  Aldershot (England).

\bibitem[\protect\citeauthoryear{Slater{\protectedslaterindex}}{2002}]{Slater_%
2002_LogicReformed}
B.~Hartley Slater{\protectedslaterindex}, 2002.
\newblock {\em Logic Reformed}.
\newblock Peter Lang AG, Bern, Switzerland.

\bibitem[\protect\citeauthoryear{Slater{\protectedslaterindex}}{2007a}]{Slater%
_2007_CompletingRussellsLogic}
B.~Hartley Slater{\protectedslaterindex}, 2007a.
\newblock Completing {\russell's logic}.
\newblock {\em \russellplain: the Journal of \russellnameplain\ Studies,
  McMaster \Univ, Hamilton (Ontario), Canada}, 27:144--158.
\newblock Also in \cite[\litchapref 3 (\PP{15}{27})]{logic-not-mathematical}.

\bibitem[\protect\citeauthoryear{Slater{\protectedslaterindex}}{2007b}]{de-mat%
hematisation-of-Logic}
B.~Hartley Slater{\protectedslaterindex}, 2007b.
\newblock {\em The De-Mathematisation of Logic}.
\newblock Poli\-metrica, Monza, Italy.
\newblock Open access publication,
  \url{wirth.bplaced.net/op/fullpaper/hilbertbernays/Slater_2007_De-Mathematis%
ation.pdf}.

\bibitem[\protect\citeauthoryear{Slater{\protectedslaterindex}}{2009}]{slater-%
handbook}
B.~Hartley Slater{\protectedslaterindex}, 2009.
\newblock {\hilbert's epsilon calculus and its successors}.
\newblock In \cite[\Vol\,5: Logic from \russell\ to \church,
  \PP{365}{448}]{handbook-of-the-history-of-logic}.

\bibitem[\protect\citeauthoryear{Slater{\protectedslaterindex}}{2011}]{logic-n%
ot-mathematical}
B.~Hartley Slater{\protectedslaterindex}, 2011.
\newblock {\em Logic is Not Mathematical}.
\newblock \collegepublications.

\bibitem[\protect\citeauthoryear{Smullyan{\protectedsmullyanindex}}{1968}]{smu%
llyan}
Raymond~M. Smullyan{\protectedsmullyanindex}, 1968.
\newblock {\em First-Order Logic}.
\newblock {\springerverlag}.
\newblock \nth 1\,\edn, \nth 2\,\extd\,\edn\ is \cite{Smullyan95}.

\bibitem[\protect\citeauthoryear{Smullyan{\protectedsmullyanindex}}{1995}]{Smu%
llyan95}
Raymond~M. Smullyan{\protectedsmullyanindex}, 1995.
\newblock {\em First-Order Logic}.
\newblock Dover Publications, New York.
\newblock \nth 2\,\extd\,\edn\ of \cite{smullyan}, with a new preface and some
  corrections of the author.

\bibitem[\protect\citeauthoryear{Strawson}{1950}]{referring}
Peter~F. Strawson, 1950.
\newblock {\referringtitle}.
\newblock {\em \mindname}, 59:320--344.

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

\bibitem[\protect\citeauthoryear{Wallen}{1990}]{wallen}
Lincoln~A. Wallen, 1990.
\newblock {\em Automated Proof Search in Non-Classical Logics --- efficient
  matrix proof methods for modal and intuitionistic logics}.
\newblock \mitpress.
\newblock Phd thesis.

\bibitem[\protect\citeauthoryear{Whitehead{\protect\whiteheadindex} \bgroup\&\
  \egroup Russe{\protectedrussellindex}ll}{1910--1913}]{PM}
Alfred~North Whitehead{\protect\whiteheadindex} and Bertrand
  Russe{\protectedrussellindex}ll, 1910--1913.
\newblock {\em Principia Mathematica}.
\newblock {\cambridgeunipress}.
\newblock {\nth 1\,\edn}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{1998}]{wirthgree%
n}
Claus-Peter Wirth{\protectedwirthindex}, 1998.
\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}.
\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{\protectedwirthindex}}{2002}]{wirthhilb%
ertepsilon}
Claus-Peter Wirth{\protectedwirthindex}, 2002.
\newblock A new indefinite semantics for {\hilbert's} epsilon.
\newblock In \cite[\PP{298}{314}]{eleventhTABLEAUtwo}. \www\url{/p/epsi}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2004}]{wirthcard%
inal}
Claus-Peter Wirth{\protectedwirthindex}, 2004.
\newblock {\DescenteInfinie\ + Deduction}.
\newblock {\em {\ljigplname}}, 12:1--96.
\newblock \www\url{/p/d}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2006}]{nonpermut}
Claus-Peter Wirth{\protectedwirthindex}, 2006.
\newblock {\em {$\lim$$+$}, {$\delta^+$}, and Non-Permutability of
  {$\beta$}-Steps}.
\newblock {SEKI-Report SR--2005--01 (ISSN 1437--4447)}. {SEKI Publications},
  Saarland Univ.
\newblock \Rev\,\edn\ \Jul\,2006 (\nth 1\,\edn\,2005), \PPcount{ii+36},
  \url{http://arxiv.org/abs/0902.3635}. Thoroughly improved version is
  \cite{wirth-jsc-non-permut}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2008}]{wirth-jal}
Claus-Peter Wirth{\protectedwirthindex}, 2008.
\newblock \hilbert's epsilon as an operator of indefinite committed choice.
\newblock {\em J. Applied Logic}, 6:287--317.
\newblock \url{http://dx.doi.org/10.1016/j.jal.2007.07.009}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2012a}]{wirth-he%
ijenoort}
Claus-Peter Wirth{\protectedwirthindex}, 2012a.
\newblock {\herbrandsfundamentaltheorem} in the eyes of {\heijenoortname}.
\newblock {\em {\logicauniversalisname}}, 6:485--520.
\newblock Received \Jan\,12, 2012. Published online \Jun\,22, 2012,
  \url{http://dx.doi.org/10.1007/s11787-012-0056-7}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2012b}]{wirth-js%
c-non-permut}
Claus-Peter Wirth{\protectedwirthindex}, 2012b.
\newblock {\math{\lim\tight+}, \math{\delta^+}, and \NonPermutability\ of
  \math\beta-Steps}.
\newblock {\em {\jscname}}, 47:1109--1135.
\newblock Received \Jan\,18, 2011. Published online \Jul\,15, 2011,
  \url{http://dx.doi.org/10.1016/j.jsc.2011.12.035}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2012c}]{wirth-hi%
lbert-seki}
Claus-Peter Wirth{\protectedwirthindex}, 2012c.
\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.
\newblock \Rev\,\edn\ \Jan\,2012, \PPcount{ii+73},
  {\url{http://arxiv.org/abs/0902.3749}}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2014}]{wirth-hei%
jenoort-SEKI}
Claus-Peter Wirth{\protectedwirthindex}, 2014.
\newblock {\em {\herbrandsfundamentaltheorem:} The Historical Facts and their
  Streamlining}.
\newblock {SEKI-Report SR--2014--01 (ISSN 1437--4447)}. {SEKI Publications}.
\newblock \PPcount{ii+47}, \url{http://arxiv.org/abs/1405.6317}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2016}]{wirth-eps%
ilon-confluent-terminating}
Claus-Peter Wirth{\protectedwirthindex}, 2016.
\newblock {\em The Explicit Definition of Quantifiers via {\hilbertsepsilon} is
  Confluent and Terminating}.
\newblock {SEKI-Report SR--2015--02 (ISSN 1437--4447)}. {SEKI Publications}.
\newblock \PPcount{ii+20}, \url{https://arxiv.org/abs/1611.06389}. To appear
  also in: IfCoLog Journal of Logics and their Applications.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}
  \bgroup\&al.\egroup }{2009}]{herbrand-handbook}
Claus-Peter Wirth{\protectedwirthindex}, J{\"o}rg Siek{\-}mann,
  {\mbox{Ch}}ristoph Benz{\-}m{\ue}ller{\protectedbenzmuellerindex}, and Serge
  Autexier{\protectedautexierindex}, 2009.
\newblock \herbrandname: Life, logic, and automated deduction.
\newblock In \cite[\Vol\,5: Logic from \russell\ to \church,
  \PP{195}{254}]{handbook-of-the-history-of-logic}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}
  \bgroup\&al.\egroup }{2014}]{SR--2009--01}
Claus-Peter Wirth{\protectedwirthindex}, J{\"o}rg Siek{\-}mann,
  {\mbox{Ch}}ristoph Benz{\-}m{\ue}ller{\protectedbenzmuellerindex}, and Serge
  Autexier{\protectedautexierindex}, 2014.
\newblock {\em Lectures on {\herbrandname} as a Logician}.
\newblock {SEKI-Report SR--2009--01 (ISSN 1437--4447)}. {SEKI Publications}.
\newblock \Rev\,\edn\ \May\,2014, \PPcount{ii+82},
  {\url{http://arxiv.org/abs/0902.4682}}.

\end{thebibliography}
