\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Abeles}{1994}]{abeles-herbrand-unification}
Francine Abeles.
\newblock {\herbrand's Fundamental Theorem} and the beginning of logic
  programming.
\newblock {\em Modern Logic}, 4:63--73, 1994.

\bibitem[\protect\citeauthoryear{Andrews{\protectedandrewsindex}}{2003}]{andre%
ws-herbrand-award}
Peter~B. Andrews{\protectedandrewsindex}.
\newblock {\herbrand\ Award} acceptance speech.
\newblock {\em J. Automated Reasoning}, 31:169--187, 2003.

\bibitem[\protect\citeauthoryear{Anellis{\protectedanellisindex}}{1991}]{anell%
is-loewenheim}
Irving~H. Anellis{\protectedanellisindex}.
\newblock The {\loewenheimskolemtheorem}, theories of quantification, and proof
  theory.
\newblock 1991.
\newblock In \cite[\PP{71}{83}]{drucker}.

\bibitem[\protect\citeauthoryear{Anellis{\protectedanellisindex}}{1992}]{anell%
is-heijenoort-long}
Irving~H.{\protectedheijenoortindex} Anellis{\protectedanellisindex}.
\newblock {\em Logic and Its History in the Work and Writings of\/
  {\heijenoortname}}.
\newblock Modern Logic Publ., Ames (IA), 1992.

\bibitem[\protect\citeauthoryear{Autexier{\protectedautexierindex}
  \bgroup\&al.\egroup }{2006}]{pds}
Serge Autexier{\protectedautexierindex}, {\mbox{Ch}}ristoph
  Benz{\-}m{\ue}ller{\protectedbenzmuellerindex}, Dominik Dietrich, Andreas
  Meier, and Claus-Peter Wirth{\protectedwirthindex}.
\newblock A generic modular data structure for proof attempts alternating on
  ideas and granularity.
\newblock 2006.
\newblock In \cite[\PP{126}{142}]{forthMKMfive}, \www\url{/p/pds}.

\bibitem[\protect\citeauthoryear{Autexier{\protectedautexierindex}}{2003}]{ser%
gediss}
Serge Autexier{\protectedautexierindex}.
\newblock {\em Hierarchical Contextual Reasoning}.
\newblock PhD thesis, \addressuniSBshort, 2003.

\bibitem[\protect\citeauthoryear{Autexier{\protectedautexierindex}}{2005}]{ser%
gecore}
Serge Autexier{\protectedautexierindex}.
\newblock The {\sc core} calculus.
\newblock 2005.
\newblock In \cite[\PP{84}{98}]{twentiethCADEfive}.

\bibitem[\protect\citeauthoryear{Baaz \bgroup\&\ \egroup
  Ferm{\"u}ller}{1995}]{baazdelta}
Matthias Baaz and {\mbox{Ch}}ristian~G. Ferm{\"u}ller.
\newblock Non-elementary speedups between different versions of tableaux.
\newblock 1995.
\newblock In \cite[\PP{217}{230}]{fourthTABLEAUninetyfive}.

\bibitem[\protect\citeauthoryear{Baaz \bgroup\&\ \egroup
  Leitsch}{1995}]{baazleitschcolllog}
Matthias Baaz and Alexander Leitsch.
\newblock Methods of functional extension.
\newblock {\em Collegium Logicum --- Annals of the {\goedelname\ Society}},
  1:87--122, 1995.

\bibitem[\protect\citeauthoryear{Baumgartner \bgroup\&al.\egroup
  }{1995}]{fourthTABLEAUninetyfive}
Peter Baumgartner, Reiner H{\"a}hnle, and Joachim Posegga, editors.
\newblock {\em {\thefourthTABLEAUninetyfive}}, number 918 in Lecture Notes in
  Artificial Intelligence. {\springerverlag}, 1995.

\bibitem[\protect\citeauthoryear{Beckert \bgroup\&al.\egroup
  }{1993}]{deltaplusplus}
Bernhard Beckert, Reiner H{\"a}hnle, and Peter~H. Schmitt.
\newblock The even more liberalized {\math\delta}-rule in free-variable
  semantic tableaus.
\newblock 1993.
\newblock In \cite[\PP{108}{119}]{goedelcolloquium1993}.

\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 \akademieverlag, 1973.
\newblock \nth 2\,\rev\,\edn\ (\nth 1\,\edn\,1971; \nth
  4\,\rev\,\rev\,\edn\,1986).

\bibitem[\protect\citeauthoryear{Bernays\protect\bernaysindex}{1957}]{bernays-%
herbrand}
Paul Bernays\protect\bernaysindex.
\newblock {\Ue ber den Zusammenhang des \herbrand schen Satzes mit den neueren
  Ergebnissen von \schuette{\protectedschuetteindex} und {\sc Stenius}}.
\newblock In {\em Proceedings of the International Congress of Mathematicians
  1954}, Groningen and Amsterdam, 1957. Noordhoff and \northholland.

\bibitem[\protect\citeauthoryear{Brady}{2000}]{brady}
Geraldine Brady.
\newblock {\em From {\protectedpeirceindex\peirce} to {\skolem}: A Neglected
  Chapter in the History of Logic}.
\newblock {\northholland}, 2000.

\bibitem[\protect\citeauthoryear{Cohen \bgroup\&\ \egroup
  Wartofsky}{1967}]{boston-studies-3}
Robert~S. Cohen and Marx~W. Wartofsky, editors.
\newblock {\em {\Proc\ of the Boston Colloquium for the Philosophy of Science,
  1964--1966}: In Memory of {\namefont Norwood Russell Hanson}}.
\newblock Number~3 in Boston Studies in the Philosophy of Science.
  \DReidelpublishing, 1967.

\bibitem[\protect\citeauthoryear{Dietrich}{2011}]{dodi-diss}
Dominik Dietrich.
\newblock {\em Assertion Level Proof Planning with Compiled Strategies}.
\newblock Optimus Verlag, Alexander Mostafa, \Goettingen, 2011.
\newblock \PhDthesis, \Dept\ Informatics, \addressuniSBshort.

\bibitem[\protect\citeauthoryear{Dreben{\protecteddrebenindex} \bgroup\&\
  \egroup Denton}{1963}]{supplement-to-herbrand}
Burton Dreben{\protecteddrebenindex} and John Denton.
\newblock A supplement to {\herbrand}.
\newblock {\em {\jslname}}, 31:393--398, 1963.

\bibitem[\protect\citeauthoryear{Dreben{\protecteddrebenindex}
  \bgroup\&al.\egroup }{1963}]{false-lemmas-in-herbrand}
Burton Dreben{\protecteddrebenindex}, Peter~B. Andrews{\protectedandrewsindex},
  and St{{\aa}}l Aanderaa.
\newblock False lemmas in {\herbrand}.
\newblock {\em {\bullamsname}}, 69:699--706, 1963.

\bibitem[\protect\citeauthoryear{Drucker}{1991}]{drucker}
Thomas Drucker, editor.
\newblock {\em Perspectives on the History of Mathematical Logic}.
\newblock {\birkhaeuser}, 1991.

\bibitem[\protect\citeauthoryear{Feferman}{1993a}]{heijenoort-life}
Anita~Burdman Feferman.
\newblock {\em Politics, Logic and Love --- The Life {of\/ \heijenoortname}}.
\newblock A K Peters, Wellesley (MA), 1993.

\bibitem[\protect\citeauthoryear{Feferma{\protectedfefermanindex}n}{1993b}]{he%
ijenoort-work}
Sol(omon) Feferma{\protectedfefermanindex}n.
\newblock {\heijenoortname's} scholarly work.
\newblock 1993.
\newblock In \cite[\PP{371}{390}]{heijenoort-life}.

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

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

\bibitem[\protect\citeauthoryear{Frege\protectedfregeindex}{1879}]{begriffssch%
rift}
Gottlob Frege\protectedfregeindex.
\newblock {\em {\Begriffsschrift, eine der arithmetischen nachgebildete
  Formelsprache de\es\ reinen Denken\es}}.
\newblock {Verlag von L. Nebert, \Halle}, 1879.
\newblock Corrected facsimile in \cite{begriffsschrift-und-andere}. \ Reprint
  of \PP{III}{VIII} and \PP{1}{54} in \cite[\PP{48}{106}]{logiktexte}. \
  {English} translation in \cite[\PP{1}{82}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Frege\protectedfregeindex}{1964}]{begriffssch%
rift-und-andere}
Gottlob Frege\protectedfregeindex.
\newblock {\em {\Begriffsschrift\ und andere Auf\-s\ae tze}}.
\newblock \wissenschaftlichebuchgesellschaftdarmstadt, 1964.
\newblock {Zweite Au\fli age, mit \husserlname s und \scholzname' Anmerkungen,
  herau\esi gegeben von {\namefont Ignacio Angelelli}}.

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

\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{G{\oe
  de{\protectedgoedelindex}l}}{1930}]{goedel-completeness}
Kurt G{\oe de{\protectedgoedelindex}l}.
\newblock {Die Vollst\ae ndigkeit der Axiome des logischen Funktionen\-kalk\ue
  ls}.
\newblock {\em {\monatsheftempname}}, 37:349--360, 1930.
\newblock With {English} translation also in \cite[\Vol\,I,
  \PP{102}{123}]{goedelcollected}.

\bibitem[\protect\citeauthoryear{G{\oe
  de{\protectedgoedelindex}l}}{1986ff.}]{goedelcollected}
Kurt G{\oe de{\protectedgoedelindex}l}.
\newblock {\em Collected Works}.
\newblock {\oxfordunipress}, 1986ff.
\newblock \Ed\ by \fefermanname, \dawsonname\protect\dawsonindex,
  \goldfarbname, \heijenoortname, \kleenename, \parsonsname, \siegname,
  \etalabbrev.

\bibitem[\protect\citeauthoryear{Goldfarb{\protectedgoldfarbindex}}{1970}]{rev%
iew-herbrand-ecrits-logiques}
Warren Goldfarb{\protectedgoldfarbindex}.
\newblock Review of \cite{herbrand-ecrits-logiques}.
\newblock {\em The Philosophical Review}, 79:576--578, 1970.

\bibitem[\protect\citeauthoryear{Goldfarb{\protectedgoldfarbindex}}{1993}]{gol%
dfarb-herbrand-goedel}
Warren Goldfarb{\protectedgoldfarbindex}.
\newblock {\herbrand's} error and {\goedel's} correction.
\newblock {\em Modern Logic}, 3:103--118, 1993.

\bibitem[\protect\citeauthoryear{Gonthier}{2008}]{four-color-theorem}
Georges Gonthier.
\newblock Formal proof --- the {\fourcolortheorem}.
\newblock {\em {\noticesamsname}}, 55:1382--1393, 2008.

\bibitem[\protect\citeauthoryear{Gottlob \bgroup\&al.\egroup
  }{1993}]{goedelcolloquium1993}
Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors.
\newblock {\em {Computational Logic and Proof Theory, \Proc\ \nth 3
  \goedelname\ Colloquium}}, number 713 in Lecture Notes in Computer Science.
  {\springerverlag}, 1993.

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1967}]%
{heijenoort-logic-calculus-language}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock Logic as a calculus and logic as a language.
\newblock {\em Synthese}, 17:324--330, 1967.
\newblock Also in \cite[\PP{440}{446}]{boston-studies-3}. Also in
  \cite[\PP{11}{16}]{heijenoort-selected-essays}.

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1968}]%
{heijenoort-tree-herbrand}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock On the relation between the falsifiability tree method and the
  {\herbrand} method in quantification theory.
\newblock Unpublished typescript, \Nov\,20, 1968, \PPcount{12};
  \heijenoortname\ Papers, 1946--1988, Archives of American Mathematics, Center
  for American History, \unitexasaustin, Box\,3.8/86-33/1. \ Copy in
  \anellisarchives, 1968.

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

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1975}]%
{heijenoort-herbrand}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock \herbrand.
\newblock Unpublished typescript, \May\,18, 1975, \PPcount{15};
  \heijenoortname\ Papers, 1946--1988, Archives of American Mathematics, Center
  for American History, \unitexasaustin, Box\,3.8/86-33/1. \ Copy in
  \anellisarchives, 1975.

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1976}]%
{heijenoort-spanish-lecture-course}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock {\em El Desarrollo de la Teoria de la Cuantifcaci\'on}.
\newblock Instituto de Investigaciones Filos\'oficas, Universidad Nacional
  Aut\'onoma de M\'exico, 1976.

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1982}]%
{heijenoort-oeuvre-herbrand}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock {L'\oefranz uvre} logique de {\herbrand} et son contexte historique.
\newblock 1982.
\newblock In \cite[\PP{57}{85}]{herbrand-symposium}. \Rev\ English translation
  is \cite{heijenoort-work-herbrand}.

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1986a}%
]{heijenoort-engels}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock {\engelsname} and mathematics.
\newblock 1986.
\newblock In \cite[\PP{123}{151}]{heijenoort-selected-essays}. Previously
  unpublished manuscript written in~1948.

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1986b}%
]{heijenoort-work-herbrand}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock {\herbrand's} work in logic and its historical context.
\newblock 1986.
\newblock In \cite[\PP{99}{121}]{heijenoort-selected-essays}. \Rev\ English
  translation of \cite{heijenoort-oeuvre-herbrand}.

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1986c}%
]{heijenoort-selected-essays}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock {\em Selected Essays}.
\newblock Bibliopolis, Napoli, copyright 1985. Also published by Librairie
  Philosophique J. Vrin, \Paris, 1986, 1986.

\bibitem[\protect\citeauthoryear{Heijenoort{\protectedheijenoortindex}}{1992}]%
{heijenoort-modern-logic}
Jean~van Heijenoort{\protectedheijenoortindex}.
\newblock Historical development of modern logic.
\newblock {\em Modern Logic}, 2:242--255, 1992.
\newblock Written in 1974.

\bibitem[\protect\citeauthoryear{Herbran{\protectedherbrandindex}d}{1930}]{her%
brand-PhD}
Jacques Herbran{\protectedherbrandindex}d.
\newblock {\em {\herbrandPhDtitle}}.
\newblock PhD thesis, Universit\'e de Paris, 1930.
\newblock {Th\`eses} pr\'esent\'ees \`a la facult\'e des Sciences de Paris pour
  obtenir le grade de docteur\`es sciences math\'ematiques --- \frenchnth 1
  \nolinebreak th\`ese: Recherches sur la th\'eorie de la d\'emonstration ---
  \frenchnth 2 \nolinebreak th\`ese: Propositions donn\'ees par la facult\'e,
  Les \'equations de Fredholm --- Soutenues le 1930 devant la commission
  d'examen --- Pr\'esident: M. \vessiot, Examinateurs: MM. {\namefont Denjoy,
  Frechet} --- Vu et approuv\'e, \Paris, le 20\,Juin\,1929, Le doyen de la
  facult\'e des Sciences, {\namefont C. Maurain} --- Vu et permis d'imprimer,
  \Paris, le 20\,Juin\,1929, Le recteur de l'Academie de \Paris, {\namefont S.
  Charlety} --- No.\,d'ordre\,2121, S\'erie\,A, No.\,de\,S\'erie\,1252 ---
  Imprimerie J. Dziewulski, Varsovie --- \Univ\ de \Paris. \ Also in Prace
  \WarsawScientificSocietyIII\ Nauk Matematyczno-Fizychnych, Nr.\,33,
  \Warszawa. \ A contorted, newly typeset reprint is
  \cite[\PP{35}{153}]{herbrand-ecrits-logiques}. \ Annotated {E}nglish
  translation {\em Investigations in Proof Theory}\/ by \goldfarbname\
  (\litchapfromtoref 1 4) and \drebenname\ and \heijenoortname\ (\litchapref 5)
  with a brief introduction by \goldfarb\ and extended notes by \goldfarb\
  \mbox{(\litnotefromtoref A C, K--M, O)}, \dreben\ (\litnotefromtoref F I),
  \dreben\ and \goldfarb\ (\litnoterefss D J N), and \dreben, \huffname, and
  \hailperinname\ (\litnoteref E) in
  \cite[\PP{44}{202}]{herbrand-logical-writings}. \ {E}nglish translation of
  \litsectref 5 with a different introduction by \heijenoort\ and some
  additional extended notes by \dreben\ also in
  \cite[\PP{525}{581}]{heijenoort-source-book}. \ \bibcrit{\herbrand's
  \PhDthesis, his cardinal work, dated \herbrandPhDdating; submitted at the
  \Univ\ of \Paris; defended at the Sorbonne \herbrandPhDdefensedate; printed
  in \WarszawaEnglish, 1930.}

\bibitem[\protect\citeauthoryear{Herbran{\protectedherbrandindex}d}{1936}]{her%
brand-1936}
Jacques Herbran{\protectedherbrandindex}d.
\newblock {\em Le D\'eveloppement Moderne de la Th\'eorie des Corps
  Alg\'ebriques --- Corps de classes et lois de r\'eciprocit\'e}.
\newblock M\'emorial des Sciences Math\'ematiques, Fascicule\,LXXV.
  {\gauthiervillars}, 1936.
\newblock \Ed\ and with an appendix by \chevalleyname.

\bibitem[\protect\citeauthoryear{Herbran{\protectedherbrandindex}d}{1968}]{her%
brand-ecrits-logiques}
Jacques Herbran{\protectedherbrandindex}d.
\newblock {\em {\'E}crits Logiques}.
\newblock Presses Universitaires de France, Paris, 1968.
\newblock Cortorted \edn~of \herbrand's logical writings by \heijenoortname.
  Review in \cite{review-herbrand-ecrits-logiques}. \hskip.2em {E}nglish
  translation is \cite{herbrand-logical-writings}.

\bibitem[\protect\citeauthoryear{Herbran{\protectedherbrandindex}d}{1971}]{her%
brand-logical-writings}
Jacques Herbran{\protectedherbrandindex}d.
\newblock {\em Logical Writings}.
\newblock {\harvardunipress}, 1971.
\newblock \Ed\ by \goldfarbname. Translation of \cite{herbrand-ecrits-logiques}
  with additional annotations, brief introductions, and extended notes by
  \goldfarb, \drebenname, and \heijenoortname. \
  \bibcrit{\textonherbrandlogicalwritings}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays\protect\bernaysindex}{1934}]{grundlagen-first-edition-volume-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays\protect\bernaysindex.
\newblock {\em {Die Grundlagen der Mathematik --- Erster Band}}.
\newblock Number~XL in {Die Grundlehren der Mathematischen Wissenschaften in
  Einzeldarstellungen}. {\springerverlag}, 1934.
\newblock \nth 1\,\edn\ (\nth 2\,\edn\ is
  \cite{grundlagen-second-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\protect\bernaysindex}{1939}]{grundlagen-first-edition-volume-two}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays\protect\bernaysindex.
\newblock {\em {Die Grundlagen der Mathematik --- Zweiter Band}}.
\newblock Number~L in {Die Grundlehren der Mathematischen Wissenschaften in
  Einzeldarstellungen}. {\springerverlag}, 1939.
\newblock \nth 1\,\edn\ (\nth 2\,\edn\ is
  \cite{grundlagen-second-edition-volume-two}).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays\protect\bernaysindex}{1968}]{grundlagen-second-edition-volume-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays\protect\bernaysindex.
\newblock {\em {Die Grundlagen der Mathematik~I}}.
\newblock Number~40 in {Die Grundlehren der Mathematischen Wissenschaften in
  Einzeldarstellungen}. {\springerverlag}, 1968.
\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\protect\bernaysindex}{1970}]{grundlagen-second-edition-volume-two}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays\protect\bernaysindex.
\newblock {\em {Die Grundlagen der Mathematik~II}}.
\newblock Number~50 in {Die Grundlehren der Mathematischen Wissenschaften in
  Einzeldarstellungen}. {\springerverlag}, 1970.
\newblock \nth 2\,\rev\,\edn\,of \cite{grundlagen-first-edition-volume-two}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays\protect\bernaysindex}{2013a}]{grundlagen-german-english-edition-volu%
me-one-one}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays\protect\bernaysindex.
\newblock {\em {Grundlagen der Mathematik~I --- Foundations of Mathematics~I,
  Part\,A: \whatisinVolIPartA}}.
\newblock \url{http://wirth.bplaced.net/p/hilbertbernays}, 2013.
\newblock Thoroughly \rev\,\nth 2\,\edn\ (\nth 1\,\edn\ \collegepublications,
  2011). 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}. Translated and commented by
  \wirthname. \Ed\ by \wirthname, \siekmannname, \michaelgabbayname,
  \gabbayname. Advisory Board: \siegname\ (chair), \anellisname, \awodeyname,
  \baazname, \buchholzname, \buldtname, \kahlename, \mancosuname, \parsonsname,
  \peckhausname, \taitname, \tappname, \zachname.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt \bgroup\&\
  \egroup
  Bernays\protect\bernaysindex}{2013b}]{grundlagen-german-english-edition-volu%
me-one-two}
David Hilbe{\protectedhilbertindex}rt and Paul Bernays\protect\bernaysindex.
\newblock {\em {Grundlagen der Mathematik~I --- Foundations of Mathematics~I,
  Part\,B: \whatisinVolIPartB}}.
\newblock \url{http://wirth.bplaced.net/p/hilbertbernays}, 2013.
\newblock Thoroughly \rev\,\nth 2\,\edn. 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}. Translated and commented by
  \wirthname. \Ed\ by \wirthname, \siekmannname, \michaelgabbayname,
  \gabbayname. Advisory Board: \siegname\ (chair), \anellisname, \awodeyname,
  \baazname, \buchholzname, \buldtname, \kahlename, \mancosuname, \parsonsname,
  \peckhausname, \taitname, \tappname, \zachname.

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

\bibitem[\protect\citeauthoryear{Kohlhase}{2006}]{forthMKMfive}
Michael Kohlhase, editor.
\newblock {\em {\theforthMKMfive}, Revised Selected Papers}, number 3863 in
  Lecture Notes in Artificial Intelligence. {\springerverlag}, 2006.

\bibitem[\protect\citeauthoryear{Kuhn}{1962}]{kuhn}
Thomas~S. Kuhn.
\newblock {\em The Structure of Scientific Revolutions}.
\newblock \chicagounipress, 1962.
\newblock \nth 1\,\edn.

\bibitem[\protect\citeauthoryear{L{\"o}wenheim{\protectedloewenheimindex}}{191%
5}]{loewenheim-1915}
Leopold L{\"o}wenheim{\protectedloewenheimindex}.
\newblock {\Ue ber M\oe glich\-keiten im Relativ\-kalk\ue l}.
\newblock {\em {\MathematischeAnnalen}}, 76:228--251, 1915.
\newblock {English} translation {\em On Possibilities in the Calculus of
  Relatives} by \bauermengelbergname\ with an introduction by \heijenoortname\
  in \cite[\PP{228}{251}]{heijenoort-source-book}.

\bibitem[\protect\citeauthoryear{Martelli \bgroup\&\ \egroup
  Montanari}{1982}]{martelli-montanari}
Alberto Martelli and Ugo Montanari.
\newblock An efficient unification algorithm.
\newblock {\em \ACM\ Transactions on Programming Languages and Systems},
  4:258--282, 1982.

\bibitem[\protect\citeauthoryear{Menzler-Trott}{2001}]{menzler-gentzen-german}
Eckart Menzler-Trott.
\newblock {\em {\gentzen's Problem -- Mathematische Logik im
  nationalsozialistischen Deutschland}}.
\newblock \birkhaeuser, 2001.
\newblock \Rev\ English translation is \cite{menzler-gentzen-english}.

\bibitem[\protect\citeauthoryear{Menzler-Trott}{2007}]{menzler-gentzen-english}
Eckart Menzler-Trott.
\newblock {\em Logic's Lost Genius --- The Life {of\/ \gentzenname}}.
\newblock \AMSname, 2007.
\newblock \Rev\ English translation of \cite{menzler-gentzen-german}.

\bibitem[\protect\citeauthoryear{Nieuwenhuis}{2005}]{twentiethCADEfive}
Robert Nieuwenhuis, editor.
\newblock {\em {\thetwentiethCADEfive}}, number 3632 in Lecture Notes in
  Artificial Intelligence. {\springerverlag}, 2005.

\bibitem[\protect\citeauthoryear{Paterson \bgroup\&\ \egroup
  Wegman}{1978}]{PatersonWegman78}
Michael~S. Paterson and Mark~N. Wegman.
\newblock Linear unification.
\newblock {\em \jcssname}, 16:158--167, 1978.

\bibitem[\protect\citeauthoryear{Peckhau{\protectedpeckhausindex}s}{2004}]{sch%
roeder-handbook}
Volker Peckhau{\protectedpeckhausindex}s.
\newblock {\schroeder's} logic.
\newblock 2004.
\newblock {\protectedschroederindex}In \cite[\Vol\,3: The Rise of Modern Logic:
  From \leibniz\ to \frege, \PP{557}{610}]{handbook-of-the-history-of-logic}.

\bibitem[\protect\citeauthoryear{Peirce\protectedpeirceindex}{1885}]{peirce-18%
85}
Charles~S. Peirce\protectedpeirceindex.
\newblock On the algebra of logic: A contribution to the philosophy of
  notation.
\newblock {\em American J. of Mathematics}, 7:180--202, 1885.
\newblock Also in \cite[\PP{162}{190}]{peirce-chrono-five}.

\bibitem[\protect\citeauthoryear{Peirce\protectedpeirceindex}{1993}]{peirce-ch%
rono-five}
Charles~S. Peirce\protectedpeirceindex.
\newblock {\em {Writings of\/ \peircename\ --- A Chronological Edition,
  \Vol\,5, 1884--1886}}.
\newblock \indianaunipress, 1993.
\newblock \Ed\ by {\namefont Christian J. W. Kloesel}.

\bibitem[\protect\citeauthoryear{Schr{\"o}der{\protectedschroederindex}}{1895}%
]{schroeder-vorlesungen-III}
Ernst Schr{\"o}der{\protectedschroederindex}.
\newblock {\em {Vorlesungen \ue ber die Algebra der Logik, \Vol\,3, Algebra der
  Logik und der Relative, Vorlesungen I-XII}}.
\newblock \teubnerverlag, \Leipzig, 1895.
\newblock {E}nglish translation of some parts in \cite{brady}.

\bibitem[\protect\citeauthoryear{Sch{\"u}tte{\protectedschuetteindex}}{1960}]{%
schuette60:_beweis}
Kurt Sch{\"u}tte{\protectedschuetteindex}.
\newblock {\em {Bewei\esi theorie}}.
\newblock Number 103 in Grundlehren der mathematischen Wissenschaften.
  {\springerverlag}, 1960.
\newblock Thoroughly revised {English} translation: \cite{schuette-1977}.

\bibitem[\protect\citeauthoryear{Sch{\"u}tte{\protectedschuetteindex}}{1977}]{%
schuette-1977}
Kurt Sch{\"u}tte{\protectedschuetteindex}.
\newblock {\em Proof theory}.
\newblock Number 225 in Grundlehren der mathematischen Wissenschaften.
  {\springerverlag}, 1977.
\newblock Translated from a thorough revision of \cite{schuette60:_beweis} by
  \crossleyname.

\bibitem[\protect\citeauthoryear{Skolem{\protectedskolemindex}}{1920}]{skolem-%
1920}
Thoralf Skolem{\protectedskolemindex}.
\newblock {Logisch-kombinatorische Untersuchungen \ue ber die Erf\ue llbarkeit
  und Bewei\esi barkeit mathematischer S\ae tze nebst einem Theorem \ue ber
  dichte Mengen}.
\newblock {\em {\skriftername, \skrifterpublisher}}, 1920/4:1--36, 1920.
\newblock Also in \cite[\PP{103}{136}]{skolem-1970}. \ {E}nglish translation of
  \litsectref 1 {\em Logico-Combinatorial Investigations in the Satisfiability
  or Provability of Mathematical Propositions: A simplified proof of a theorem
  by \loewenheimname\ and generalizations of the theorem} by
  \bauermengelbergname\ with an introduction by \heijenoortname\ in
  \cite[\PP{252}{263}]{heijenoort-source-book}. \
  \bibcrit{\loewenheimskolemtheorem\ via \skolemnormalform\ and choice of a
  sub-model}.

\bibitem[\protect\citeauthoryear{Skolem{\protectedskolemindex}}{1923}]{skolem-%
1923b}
Thoralf Skolem{\protectedskolemindex}.
\newblock {Einige Bemerkungen zur axiomatischen Begr\ue ndung der Mengenlehre}.
\newblock In {\em \Proc\ \nth 5 Scandinaviska Matematikerkongressen,
  {H}elsingfors, July\,4--7,\,1922}, pages 217--232, Helsingfors, 1923.
  Akademiska Bokhandeln.
\newblock Also in \cite[\PP{137}{152}]{skolem-1970}. \ {E}nglish translation
  {\em Some remarks on Axiomatized Set Theory} by \bauermengelbergname\ with an
  introduction by \heijenoortname\ in
  \cite[\PP{290}{301}]{heijenoort-source-book}. \ \bibcrit{The best written
  and, together with \cite{skolem-1920}, the most relevant publication on the
  \loewenheimskolemtheorem; although there is some minor gap in the proof
  according to \citet{wang-skolem}, cured in \cite{skolem-1929}. \ Includes
  \skolemsparadox\ and a proof of the \loewenheimskolemtheorem\ which does not
  require any weak forms of the \axiomofchoice, via \skolemnormalform\ and
  construction of a model without assuming the previous existence of another
  one}.

\bibitem[\protect\citeauthoryear{Skolem{\protectedskolemindex}}{1928}]{skolem-%
1928}
Thoralf Skolem{\protectedskolemindex}.
\newblock {\Ue ber die mathematische Logik (Nach einem Vortrag gehalten im
  Norwegischen Mathematischen Verein am {22.\,Oktober\,1928})}.
\newblock {\em Nordisk Matematisk Tidskrift}, 10:125--142, 1928.
\newblock Also in \cite[\PP{189}{206}]{skolem-1970}. \ {E}nglish translation
  {\em On Mathematical Logic}\/ by \bauermengelbergname\ and \foellesdalname\
  with an introduction by \drebenname\ and \heijenoortname\ in
  \cite[\PP{508}{524}]{heijenoort-source-book}. \ \bibcrit{First explicit
  occurrence of \skolemization\ and \skolem\ functions}.

\bibitem[\protect\citeauthoryear{Skolem{\protectedskolemindex}}{1929}]{skolem-%
1929}
Thoralf Skolem{\protectedskolemindex}.
\newblock {\Ue ber einige Grundlagenfragen der Mathematik}.
\newblock {\em {\skriftername, \skrifterpublisher}}, 1929/4:1--49, 1929.
\newblock Also in \cite[\PP{227}{273}]{skolem-1970}. \ \bibcrit{Detailed
  discussion of \skolemsparadox\ and the \loewenheimskolemtheorem}.

\bibitem[\protect\citeauthoryear{Skolem{\protectedskolemindex}}{1970}]{skolem-%
1970}
Thoralf Skolem{\protectedskolemindex}.
\newblock {\em Selected Works in Logic}.
\newblock Universitetsforlaget \Oslo, 1970.
\newblock \Ed\ by \fenstadname. \bibcrit{Without index, but with most funny
  spellings in the newly set titles}.

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

\bibitem[\protect\citeauthoryear{Stern}{1982}]{herbrand-symposium}
Jacques Stern, editor.
\newblock {\em {\Proc\ of the \herbrand\ Symposium, Logic Colloquium'81,
  Marseilles, France, \Jul\,1981}}.
\newblock {\northholland}, 1982.

\bibitem[\protect\citeauthoryear{Tai{\protectedtaitindex}t}{2006}]{tait-2006}
William~W. Tai{\protectedtaitindex}t.
\newblock {\goedel's} correspondence on proof theory and constructive
  mathematics.
\newblock {\em {\philosphiamathname}}, 14:76--111, 2006.

\bibitem[\protect\citeauthoryear{Taylor \bgroup\&\ \egroup
  Wiles}{1995}]{wiles-fermat-correction}
Richard Taylor and Andrew Wiles.
\newblock Ring theoretic properties of certain {\hecke} algebras.
\newblock {\em Annals of Mathematics}, 141:553--572, 1995.
\newblock Received \Oct\,7, 1994. Appendix due to \faltingsname\ received
  \Jan\,26, 1995.

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

\bibitem[\protect\citeauthoryear{Wang{\protectedwangindex}}{1970}]{wang-skolem}
Hao Wang{\protectedwangindex}.
\newblock A survey of {\skolem's} work in logic.
\newblock 1970.
\newblock {\protectedskolemindex}In \cite[\PP{17}{52}]{skolem-1970}.

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

\bibitem[\protect\citeauthoryear{Wiles}{1995}]{wiles-fermat}
Andrew Wiles.
\newblock Modular elliptic curves and {{\fermat's Last Theorem}}.
\newblock {\em Annals of Mathematics}, 141:443--551, 1995.
\newblock Received \Oct\,14, 1994.

\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}.
\newblock \herbrandname: Life, logic, and automated deduction.
\newblock 2009.
\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}.
\newblock {\em Lectures on {\herbrandname} as a Logician}.
\newblock {SEKI-Report SR--2009--01 (ISSN 1437--4447)}. {SEKI Publications},
  {DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique
  Schmidt Str.\,5, D--28359 Bremen, Germany}, 2014.
\newblock \Rev\,\edn\ \May\,2014, \PPcount{ii+82},
  {\url{http://arxiv.org/abs/0902.4682}}.

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

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2006}]{nonpermut}
Claus-Peter Wirth{\protectedwirthindex}.
\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\,\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}.
\newblock \hilbert's epsilon as an operator of indefinite committed choice.
\newblock {\em J. Applied Logic}, 6:287--317, 2008.
\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}.
\newblock {\herbrandsfundamentaltheorem} in the eyes of {\heijenoortname}.
\newblock {\em {\logicauniversalisname}}, 6:485--520, 2012.
\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}.
\newblock {\math{\lim\tight+}, \math{\delta^+}, and \NonPermutability\ of
  \math\beta-Steps}.
\newblock {\em {\jscname}}, 47:1109--1135, 2012.
\newblock Received \Jan\,18, 2011. Published online \Jul\,15, 2011,
  \url{http://dx.doi.org/10.1016/j.jsc.2011.12.035}. More funny version is
  \cite{nonpermut}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2012c}]{wirth-ma%
nifesto-ljigpl}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock Human-oriented inductive theorem proving by descente infinie --- {a
  \nolinebreak manifesto}.
\newblock {\em {\ljigplname}}, 20:1046--1063, 2012.
\newblock Received \Jul\,11, 2011. Published online \Mar\,12, 2012,
  \url{http://dx.doi.org/10.1093/jigpal/jzr048}.

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

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2013}]{SR--2011-%
-01}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock {\em {A Simplified and Improved Free-Variable Framework for
  \hilbert's epsilon as an Operator of Indefinite Committed Choice}}.
\newblock {SEKI Report SR--2011--01 (ISSN 1437--4447)}. {SEKI Publications},
  {DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique
  Schmidt Str.\,5, D--28359 Bremen, Germany}, 2013.
\newblock \Rev\,\edn\ \Jan\,2013 (\nth 1\,\edn\,2011), \PPcount{ii+65},
  {\url{http://arxiv.org/abs/1104.2444}}.

\end{thebibliography}