\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Abrahams \bgroup \em et al.\egroup
  }{1980}]{seventhPOPLeighty}
Paul~W. Abrahams, Richard~J. Lipton, and Stephen~R. Bourne, editors.
\newblock {\em Conference Record of the \nth 7\,\POPLname, Las Vegas (NV),
  1980}. \acmpress, 1980.
\newblock \url{http://dl.acm.org/citation.cfm?id=567446}.

\bibitem[\protect\citeauthoryear{Acerbi{\protect\acerbiindex}}{2000}]{plato-in%
duction}
Fabio Acerbi{\protect\acerbiindex}.
\newblock {\plato: Parmenides 149a7--c3\@. A} proof by complete induction?
\newblock {\em Archive for History of Exact Sciences}, 55:57--76, 2000.

\bibitem[\protect\citeauthoryear{Ackermann\protect\ackermannindex}{1928}]{acke%
rmann-1928a}
Wilhelm Ackermann\protect\ackermannindex.
\newblock {Zum \hilbert schen Au\fbi au der reellen Zahlen}.
\newblock {\em {\MathematischeAnnalen}}, 99:118--133, 1928.
\newblock Received \Jan\,20, 1927.

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

\bibitem[\protect\citeauthoryear{A{\"\i}t-Kaci and Nivat}{1989}]{kaci-nivat}
Hassan A{\"\i}t-Kaci and Maurice Nivat, editors.
\newblock {\em {\Proc\ of the Colloquium on Resolution of Equations in
  Algebraic Structures (CREAS), Lakeway (TX), 1987}}. \academicpress, 1989.

\bibitem[\protect\citeauthoryear{Anon}{2005}]{aamp7g-2005}
Anon.
\newblock {Advanced Architecture MicroProcessor 7 Government (AAMP7G)}
  microprocessor.
\newblock Rockwell Collins, Inc. \WWW\ only:
  \url{http://www.rockwellcollins.com/sitecore/content/Data/Products/Informati%
on_Assurance/Cryptography/AAMP7G_Microprocessor.aspx}, 2005.

\bibitem[\protect\citeauthoryear{Armando \bgroup \em et al.\egroup
  }{2008}]{fourthIJCAReight}
Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors.
\newblock {\em {\thefourthIJCAReight}}, number 5195 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 2008.

\bibitem[\protect\citeauthoryear{Aubin{\protectedaubinindex}}{1976}]{aubin-197%
6}
Raymond Aubin{\protectedaubinindex}.
\newblock {\em Mechanizing Structural Induction}.
\newblock PhD thesis, \uniEBshort, 1976.
\newblock Short version is \cite{aubin-1979}.
  \url{http://hdl.handle.net/1842/6649}.

\bibitem[\protect\citeauthoryear{Aubin{\protectedaubinindex}}{1979}]{aubin-197%
9}
Raymond Aubin{\protectedaubinindex}.
\newblock {Mechanizing Structural Induction --- Part\,I: Formal System.
  Part\,II: Strategies}.
\newblock {\em \tcsname}, 9:329--345+347--362, 1979.
\newblock Received March (Part\,I) and November (Part\,II) 1977, \rev\
  \Mar\,1978. Long version is \cite{aubin-1976}.

\bibitem[\protect\citeauthoryear{Autexier{\protectedautexierindex} \bgroup \em
  et al.\egroup }{1999}]{inkafuenf}
Serge Autexier{\protectedautexierindex}, Dieter Hutter{\protectedhutterindex},
  Heiko Mantel, and Axel Schairer.
\newblock System description: {\INKA\,5.0} -- a logical voyager.
\newblock 1999.
\newblock In \cite[\PP{207}{211}]{sixteenthCADEninetynine}.

\bibitem[\protect\citeauthoryear{Autexier{\protectedautexierindex}}{2005}]{ser%
getableau}
Serge Autexier{\protectedautexierindex}.
\newblock On the dynamic increase of multiplicities in matrix proof methods for
  classical higher-order logic.
\newblock 2005.
\newblock In \cite[\PP{48}{62}]{fourteenthTABLEAUfive}.

\bibitem[\protect\citeauthoryear{Avenhaus \bgroup \em et al.\egroup
  }{2003}]{quodlibet-cade}
J{\"u}rgen Avenhaus, Ulrich K{\"u}hler{\protectedkuehlerindex}, Tobias
  Schmidt-Samoa{\protectedsamoaindex}, and Claus-Peter
  Wirth{\protectedwirthindex}.
\newblock How to prove inductive theorems? {\QUODLIBET}!
\newblock 2003.
\newblock In \cite[\PP{328}{333}]{nineteenthCADEthree}, \www\url{/p/quodlibet}.

\bibitem[\protect\citeauthoryear{Baader}{2003}]{nineteenthCADEthree}
Franz Baader, editor.
\newblock {\em {\thenineteenthCADEthree}}, number 2741 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 2003.

\bibitem[\protect\citeauthoryear{Baaz and 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{Bachmair \bgroup \em et al.\egroup
  }{1992}]{Hotz-Festschrift}
Leo Bachmair, Harald Ganzinger, and Wolfgang~J. Paul, editors.
\newblock {\em {Informatik -- Festschrift zum 60.\,Geburt\esi tag von
  {\namefont G\ue nter Hotz}}}.
\newblock \teubnerverlag, 1992.

\bibitem[\protect\citeauthoryear{Bachmair}{1988}]{bachmair}
Leo Bachmair.
\newblock Proof by consistency in equational theories.
\newblock 1988.
\newblock In \cite[\PP{228}{233}]{lics3}.

\bibitem[\protect\citeauthoryear{Bajscy}{1993}]{ijcai13}
Ruzena Bajscy, editor.
\newblock {\em {\Proc\ \nth{13} \IJCAIname\ (\IJCAI), Chambery (France)}}.
  \morgankaufmann, 1993.
\newblock \url{http://ijcai.org/Past%20Proceedings}.

\bibitem[\protect\citeauthoryear{Barendregt}{1981}]{lambda-calculus-1st}
Hen(dri)k~P. Barendregt.
\newblock {\em The Lambda Calculus --- Its Syntax and Semantics}.
\newblock Number 103 in Studies in Logic and the Foundations of Mathematics.
  \northholland, 1981.
\newblock \nth 1\,\edn\ (final\,\rev\,\edn\ is \cite{lambda-calculus-final}).

\bibitem[\protect\citeauthoryear{Barendregt}{2012}]{lambda-calculus-final}
Hen(dri)k~P. Barendregt.
\newblock {\em The Lambda Calculus --- Its Syntax and Semantics}.
\newblock Number~40 in Studies in Logic. \collegepublications, 2012.
\newblock \nth 6\,\rev\,\edn\ (\nth 1\,\edn\ is \cite{lambda-calculus-1st}).

\bibitem[\protect\citeauthoryear{Barner{\protectedbarnerindex}}{2001a}]{fermat%
slife-english-2}
Klaus Barner{\protectedbarnerindex}.
\newblock {\fermatname\ (1601?--1665) --- His life beside mathematics}.
\newblock {\em European Mathematical Society Newsletter},
  43\,(\Dec\,2001):12--16, 2001.
\newblock Long version in German is \cite{fermatslife}.
  \url{www.ems-ph.org/journals/newsletter/pdf/2001-12-42.pdf}.

\bibitem[\protect\citeauthoryear{Barner{\protectedbarnerindex}}{2001b}]{fermat%
slife}
Klaus Barner{\protectedbarnerindex}.
\newblock {Da\es\ Leben \fermat\es}.
\newblock {\em \dmvmitteilungenname}, 3/2001:12--26, 2001.
\newblock Extensions in \cite{fermat-birth-date}. Short versions in English are
  \makeaciteoftwo{fermatslife-english-1}{fermatslife-english-2}.

\bibitem[\protect\citeauthoryear{Barner{\protectedbarnerindex}}{2001c}]{fermat%
slife-english-1}
Klaus Barner{\protectedbarnerindex}.
\newblock How old did {\fermat} become?
\newblock {\em NTM Internationale Zeitschrift f\ue r Geschichte und Ethik der
  Naturwissenschaften, Technik und Medizin, Neue Serie, ISSN\,00366978},
  9:209--228, 2001.
\newblock Long version in German is \cite{fermatslife}. New results on the
  subject in \cite{fermat-birth-date}.

\bibitem[\protect\citeauthoryear{Barner{\protectedbarnerindex}}{2007}]{fermat-%
birth-date}
Klaus Barner{\protectedbarnerindex}.
\newblock {Neue\es\ zu \fermat\es\ Geburt\esi datum}.
\newblock {\em \dmvmitteilungenname}, 15:12--14, 2007.
\newblock \bibcrit{Further support for the results of
  \cite{fermatslife-english-1}, narrowing down \fermat's birth date from 1607/8
  to \Nov\,1607}.

\bibitem[\protect\citeauthoryear{Basin and Walsh}{1996}]{rippling-calculus}
David Basin and Toby Walsh.
\newblock A calculus for and termination of rippling.
\newblock {\em \jarname}, 16:147--180, 1996.

\bibitem[\protect\citeauthoryear{Becker}{1965}]{becker-griechische}
Oscar Becker, editor.
\newblock {\em {Zur Geschichte der griechischen Mathematik}}.
\newblock \wissenschaftlichebuchgesellschaftdarmstadt, 1965.

\bibitem[\protect\citeauthoryear{Beckert}{2005}]{fourteenthTABLEAUfive}
Bernhard Beckert, editor.
\newblock {\em {\thefourteenthTABLEAUfive}}, number 3702 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 2005.

\bibitem[\protect\citeauthoryear{Bell and Thayer}{1976}]{waterfall}
Thomas~E. Bell and T.~A. Thayer.
\newblock Software requirements: Are they really a problem?
\newblock 1976.
\newblock In \cite[\PP{61}{68}]{secondICSEseventysix},
  \url{http://pdf.aminer.org/000/361/405/software_requirements_are_they_really%
_a_problem.pdf}.

\bibitem[\protect\citeauthoryear{Benz{\-}m{\ue}ller{\protectedbenzmuellerindex}
  \bgroup \em et al.\egroup }{2008}]{C26}
{\mbox{Ch}}ristoph Benz{\-}m{\ue}ller{\protectedbenzmuellerindex}, Frank
  Theiss, Lawrence~C. Paulson, and Arnaud Fietz{\-}ke.
\newblock {\LEOII} --- a cooperative automatic theorem prover for higher-order
  logic.
\newblock 2008.
\newblock In \cite[\PP{162}{170}]{fourthIJCAReight}.

\bibitem[\protect\citeauthoryear{Berka and 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{Bevers and Lewi}{1990}]{bevers&lewi}
Eddy Bevers and Johan Lewi.
\newblock Proof by consistency in conditional equational theories.
\newblock \Tech\ Report CW 102, \Dept\ \Comp\ \Sci, K. U. Leuven, 1990.
\newblock \Rev\,\Jul\,1990. Short version in
  \cite[\PP{194}{205}]{secondCTRSninety}.

\bibitem[\protect\citeauthoryear{Bevier \bgroup \em et al.\egroup
  }{1989}]{cli-1989-1}
William~R. Bevier, Warren~A. Hunt{\protectedhuntindex}, J~Strother
  Moore{\protect\mooreindex}, and William~D. Young.
\newblock An approach to systems verification.
\newblock {\em \jarname}, 5:411--428, 1989.

\bibitem[\protect\citeauthoryear{Bevier}{1989}]{bevier-1989}
William~R. Bevier.
\newblock Kit and the short stack.
\newblock {\em \jarname}, 5:519--530, 1989.

\bibitem[\protect\citeauthoryear{Bibel and
  Kowalski{\protectedkowalskiindex}}{1980}]{fifthCADEeighty}
Wolfgang Bibel and Robert~A. Kowalski{\protectedkowalskiindex}, editors.
\newblock {\em {\thefifthCADEeighty}}, number~87 in Lecture Notes in Computer
  Science. \springerverlag, 1980.

\bibitem[\protect\citeauthoryear{Biundo \bgroup \em et al.\egroup
  }{1986}]{inka}
Susanne Biundo, Birgit Hummel, Dieter Hutter{\protectedhutterindex}, and
  {\mbox{Ch}}ristoph Walther{\protectedwaltherindex}.
\newblock The {\KA} inductive theorem proving system.
\newblock 1986.
\newblock In \cite[\PP{673}{675}]{eighthCADEeightysix}.

\bibitem[\protect\citeauthoryear{Bledsoe{\protect\bledsoeindex} and
  Loveland}{1984}]{after-25-years}
W.~W. Bledsoe{\protect\bledsoeindex} and Donald~W. Loveland, editors.
\newblock {\em Automated Theorem Proving: After 25 Years}.
\newblock Number~29 in Contemporary Mathematics. \AMSname, Providence (RI),
  1984.
\newblock \Proc\ of the Special Session on Automatic Theorem Proving,
  \nth{89}\,Annual Meeting of the \AMSname, Denver (CO), \Jan\,1983.

\bibitem[\protect\citeauthoryear{Bledsoe{\protect\bledsoeindex} \bgroup \em et
  al.\egroup }{1971}]{BBH72-short}
W.~W. Bledsoe{\protect\bledsoeindex}, Robert~S. Boyer{\protect\boyerindex}, and
  William~H. Henneman.
\newblock Computer proofs of limit theorems.
\newblock 1971.
\newblock In \cite[\PP{586}{600}]{ijcai2}. Long version is \cite{BBH72}.

\bibitem[\protect\citeauthoryear{Bledsoe{\protect\bledsoeindex} \bgroup \em et
  al.\egroup }{1972}]{BBH72}
W.~W. Bledsoe{\protect\bledsoeindex}, Robert~S. Boyer{\protect\boyerindex}, and
  William~H. Henneman.
\newblock Computer proofs of limit theorems.
\newblock {\em \artificialintelligencename}, 3:27--60, 1972.
\newblock Short version is \cite{BBH72-short}.

\bibitem[\protect\citeauthoryear{Bledsoe{\protect\bledsoeindex}}{1971}]{Ble71}
W.~W. Bledsoe{\protect\bledsoeindex}.
\newblock Splitting and reduction heuristics in automatic theorem proving.
\newblock {\em \artificialintelligencename}, 2:55--77, 1971.

\bibitem[\protect\citeauthoryear{Bouajjani and
  Maler}{2009}]{twentyfirstCAVnine}
Ahmed Bouajjani and Oded Maler, editors.
\newblock {\em \Proc\ \nth{21} \Int\ \Conf\ on Computer Aided Verification
  (CAV), Grenoble (France), 2009}, volume 5643 of {\em Lecture Notes in
  Computer Science}. \springerverlag, 2009.

\bibitem[\protect\citeauthoryear{Bouhoula and Rusinowitch}{1995}]{spike}
Adel Bouhoula and Micha{\"e}l Rusinowitch.
\newblock Implicit induction in conditional theories.
\newblock {\em \jarname}, 14:189--235, 1995.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1939}]{bou%
rbaki-set-theory-results-1st-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 846 in \hermannparisseries. \hermannparis, 1939.
\newblock \nth 1\,\edn, \PPcount{VIII\,+\,50}. Review is \cite{churchbourbaki}.
  \nth 2 \rev\,\extd\,\edn\ is \cite{bourbaki-set-theory-results-2nd-edn}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1951}]{bou%
rbaki-set-theory-results-2nd-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 846-1141 in \hermannparisseries. \hermannparis, 1951.
\newblock \nth 2\,\rev\,\extd\,\edn\,of
  \cite{bourbaki-set-theory-results-1st-edn}. \nth 3 \rev\,\extd\,\edn\ is
  \cite{bourbaki-set-theory-results-3rd-edn}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1954}]{bou%
rbaki-set-theory-chapter-1-2-1st-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,I\,\&\,II}}.
\newblock Number 1212 in \hermannparisseries. \hermannparis, 1954.
\newblock \nth 1\,\edn. \nth 2\,\rev\,\edn\ is
  \cite{bourbaki-set-theory-chapter-1-2-2nd-edn}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1956}]{bou%
rbaki-set-theory-chapter-3-1st-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,III}}.
\newblock Number 1243 in \hermannparisseries. \hermannparis, 1956.
\newblock \nth 1\,\edn,
  \PPcount{II\,+\,119\,+\,4\,(mode\,d'emploi)\,+\,23\,(errata\,{no.}\,6)}. \nth
  2\,\rev\,\extd\,\edn\ is \cite{bourbaki-set-theory-chapter-3-2nd-edn}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1958a}]{bo%
urbaki-set-theory-chapter-4-1st-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,IV}}.
\newblock Number 1258 in \hermannparisseries. \hermannparis, 1958.
\newblock \nth 1\,\edn. \nth 2\,\rev\,\extd\,\edn\ is
  \cite{bourbaki-set-theory-chapter-4-2nd-edn}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1958b}]{bo%
urbaki-set-theory-results-3rd-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 1141 in \hermannparisseries. \hermannparis, 1958.
\newblock \nth 3\,\rev\,\extd\,\edn\,of
  \cite{bourbaki-set-theory-results-2nd-edn}. \nth 4 \rev\,\extd\,\edn\ is
  \cite{bourbaki-set-theory-results-4th-edn}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1960}]{bou%
rbaki-set-theory-chapter-1-2-2nd-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,I\,\&\,II}}.
\newblock Number 1212 in \hermannparisseries. \hermannparis, 1960.
\newblock \nth 2\,\rev\,\extd\,\edn\,of
  \cite{bourbaki-set-theory-chapter-1-2-1st-edn}. \nth 3\,\rev\,\edn\ is
  \cite{bourbaki-set-theory-chapter-1-2-3rd-edn}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1964}]{bou%
rbaki-set-theory-results-4th-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 1141 in \hermannparisseries. \hermannparis, 1964.
\newblock \nth 4\,\rev\,\extd\,\edn\,of
  \cite{bourbaki-set-theory-results-3rd-edn}. \nth 5 \rev\,\extd\,\edn\ is
  \cite{bourbaki-set-theory-results-5th-edn}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1966a}]{bo%
urbaki-set-theory-chapter-4-2nd-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,IV}}.
\newblock Number 1258 in \hermannparisseries. \hermannparis, 1966.
\newblock \nth 2\,\rev\,\extd\,\edn\,of
  \cite{bourbaki-set-theory-chapter-4-1st-edn}. English translation in
  \cite{bourbaki-english}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1966b}]{bo%
urbaki-set-theory-chapter-1-2-3rd-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitres\,I\,\&\,II}}.
\newblock Number 1212 in \hermannparisseries. \hermannparis, 1966.
\newblock \nth 3\,\rev\,\edn\,of
  \cite{bourbaki-set-theory-chapter-1-2-2nd-edn},
  \PPcount{VI\,+\,143\,+\,7\,(errata\,{no.}\,13)}. English translation in
  \cite{bourbaki-english}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1967}]{bou%
rbaki-set-theory-chapter-3-2nd-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,III}}.
\newblock Number 1243 in \hermannparisseries. \hermannparis, 1967.
\newblock \nth 2\,\rev\,\extd\,\edn\,of
  \cite{bourbaki-set-theory-chapter-3-1st-edn},
  \PPcount{151\,+\,7\,(errata\,{no.}\,13)}. \nth 3\,\rev\,\edn\ results from
  executing these errata. English translation in \cite{bourbaki-english}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1968a}]{bo%
urbaki-english}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em Elements of Mathematics --- Theory of Sets}.
\newblock \hermannparisseries. \hermannparis, jointly published with
  \mbox{AdiWes} International Series in Mathematics, \addisonwesley, 1968.
\newblock English translation of
  \makeaciteoffour{bourbaki-set-theory-chapter-1-2-3rd-edn}{bourbaki-set-theor%
y-chapter-3-2nd-edn}{bourbaki-set-theory-chapter-4-2nd-edn}{bourbaki-set-theor%
y-results-5th-edn}.

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1968b}]{bo%
urbaki-set-theory-results-5th-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 1141 in \hermannparisseries. \hermannparis, 1968.
\newblock \nth 5\,\rev\,\extd\,\edn\,of
  \cite{bourbaki-set-theory-results-4th-edn}. English translation in
  \cite{bourbaki-english}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1971}]{boyer-moore-1971}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock The sharing of structure in resolution programs.
\newblock Memo~47, \uniEBshort, \Dept\ of Computational Logic, 1971.
\newblock \PPcount{II\,+\,24}. Revised version is \cite{boyer-moore-1972}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1972}]{boyer-moore-1972}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock The sharing of structure in theorem-proving programs.
\newblock 1972.
\newblock In \cite[\PP{101}{116}]{machine-intelligence-7}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1973}]{boyer-moore-1973}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock Proving theorems about {LISP} functions.
\newblock 1973.
\newblock In \cite[\PP{486}{493}]{ijcai3}.
  \url{http://ijcai.org/Past%20Proceedings/IJCAI-73/PDF/053.pdf}. \Rev\
  version, \extd\ with a section ``Failures\closequotecomma is
  \cite{boyer-moore-1975}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1975}]{boyer-moore-1975}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock Proving theorems about {LISP} functions.
\newblock {\em {\jacmname}}, 22:129--144, 1975.
\newblock \Rev\,\extd\,\edn\,of \cite{boyer-moore-1973}. Received \Sep\,1973,
  \Rev\ \Apr\,1974.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex\bmfssapindex} and
  Moore{\protect\mooreindex}}{1977a}]{boyer-moore-fast-string-searching}
Robert~S. Boyer{\protect\boyerindex\bmfssapindex} and J~Strother
  Moore{\protect\mooreindex}.
\newblock A fast string searching algorithm.
\newblock {\em \commacmname}, 20:762--772, 1977.
\newblock \url{http://doi.acm.org/10.1145/359842.359859}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1977b}]{boyer-moore-1977}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock A lemma driven automatic theorem prover for recursive function
  theory.
\newblock 1977.
\newblock In \cite[\Vol\,I, \PP{511}{519}]{ijcai5}.
  \url{http://ijcai.org/Past%20Proceedings/IJCAI-77-VOL1/PDF/089.pdf}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1979}]{bm}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock {\em A Computational Logic}.
\newblock \academicpress, 1979.
\newblock \url{http://www.cs.utexas.edu/users/boyer/acl.text}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1981a}]{boyer-moore-1981-editors}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex},
  editors.
\newblock {\em The Correctness Problem in Computer Science}.
\newblock \academicpress, 1981.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1981b}]{boyer-moore-1981-authors}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock Metafunctions: Proving them correct and using them efficiently as new
  proof procedures.
\newblock 1981.
\newblock In \cite[\PP{103}{184}]{boyer-moore-1981-editors}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1984a}]{boyer-moore-turing-completeness-lisp}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock A mechanical proof of the {\turing} completeness of pure {\LISP}.
\newblock 1984.
\newblock In \cite[\PP{133}{167}]{after-25-years}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1984b}]{boyer-moore-halting-problem}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock A mechanical proof of the unsolvability of the halting problem.
\newblock {\em \jacmname}, 31:441--458, 1984.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1984c}]{boyer-moore-proof-checking-RSA}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock Proof checking the {RSA} public key encryption algorithm.
\newblock {\em {\americanmathematicalmonthlyname}}, 91:181--189, 1984.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1985}]{boyer-moore-1985}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock Program verification.
\newblock {\em \jarname}, 1:17--23, 1985.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1987}]{bmeval-1987}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock The addition of bounded quantification and partial functions to a
  computational logic and its theorem prover.
\newblock Technical Report ICSCA-CMP-52, \Inst\ for Computing Science and
  Computing Applications, \unitexasaustin, 1987.
\newblock Printed \Jan\,1987\@. Also published as
  \makeaciteoftwo{bmeval-1988}{bmeval-1989}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1988a}]{bmeval-1988}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock The addition of bounded quantification and partial functions to a
  computational logic and its theorem prover.
\newblock {\em {\jarname}}, 4:117--172, 1988.
\newblock Received \Feb\,11,\,1987. Also pubished as
  \makeaciteoftwo{bmeval-1987}{bmeval-1989}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1988b}]{boyermoore}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock {\em A Computational Logic Handbook}.
\newblock Number~23 in Perspectives in Computing. \academicpress, 1988.
\newblock \nth 2\,\rev\,\extd\,\edn\ is \cite{boyermooresecondedition}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1988c}]{boyer-moore-1988}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock Integrating decision procedures into heuristic theorem provers: A
  case study of {\index{linear arithmetic}}linear arithmetic.
\newblock 1988.
\newblock In \cite[\PP{83}{124}]{machine-intelligence-11}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1989}]{bmeval-1989}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock The addition of bounded quantification and partial functions to a
  computational logic and its theorem prover.
\newblock 1989.
\newblock In \cite[\PP{95}{145}]{broy-1989} (received \Jan\,1988). Also
  published as \makeaciteoftwo{bmeval-1987}{bmeval-1988}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1990}]{BM90}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock A theorem prover for a computational logic.
\newblock 1990.
\newblock In \cite[\PP{1}{15}]{tenthCADEninety}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Moore{\protect\mooreindex}}{1998}]{boyermooresecondedition}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex}.
\newblock {\em A Computational Logic Handbook}.
\newblock International Series in Formal Methods. \academicpress, 1998.
\newblock \nth 2\,\rev\,\extd\,\edn\,of \cite{boyermoore}, \rev\ to work with
  \NQTHM--1992, a new version of \NQTHM.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Yu}{1992}]{boyer-yu-1992}
Robert~S. Boyer{\protect\boyerindex} and Yuan Yu.
\newblock Automated correctness proofs of machine code programs for a
  commercial microprocessor.
\newblock 1992.
\newblock In \cite[416--430]{eleventhCADEninetytwo}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} and
  Yu}{1996}]{c-string-lib-1996}
Robert~S. Boyer{\protect\boyerindex} and Yuan Yu.
\newblock Automated proofs of object code for a widely used microprocessor.
\newblock {\em \jacmname}, 43:166--192, 1996.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} \bgroup \em et
  al.\egroup }{1973}]{boyer-moore-davies-1973}
Robert~S. Boyer{\protect\boyerindex}, D.~Julian~M. Davies, and J~Strother
  Moore{\protect\mooreindex}.
\newblock The 77-editor.
\newblock Memo~62, \uniEBshort, \Dept\ of Computational Logic, 1973.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} \bgroup \em et
  al.\egroup }{1976}]{boyer-moore-shostak}
Robert~S. Boyer{\protect\boyerindex}, J~Strother Moore{\protect\mooreindex},
  and Robert~E. Shostak.
\newblock Primitive recursive program transformations.
\newblock 1976.
\newblock In \cite[\PP{171}{174}]{thirdPOPLseventysix}.
  \url{http://doi.acm.org/10.1145/800168.811550}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex}}{1971}]{Boy71}
Robert~S. Boyer{\protect\boyerindex}.
\newblock {\em Locking: a restriction of resolution}.
\newblock PhD thesis, \unitexasaustin, 1971.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex}}{2012}]{boyer-2012}
Robert~S. Boyer{\protect\boyerindex}.
\newblock {\EMAIL\ to \wirthname, \Nov\,19,\hskip-.28em}.
\newblock 2012.

\bibitem[\protect\citeauthoryear{Brock and
  Hunt{\protectedhuntindex}}{1999}]{brock-hunt-1999}
Bishop Brock and Warren~A. Hunt{\protectedhuntindex}.
\newblock Formal analysis of the {Motorola CAP DSP}.
\newblock 1999.
\newblock In \cite[\PP{81}{116}]{industrial-strength-1999}.

\bibitem[\protect\citeauthoryear{Brotherston and
  Simpson}{2007}]{DBLP:conf/lics/BrotherstonS07}
James Brotherston and Alex Simpson.
\newblock Complete sequent calculi for induction and infinite descent.
\newblock 2007.
\newblock In \cite[\PP{51}{62?}]{lics22}. Thoroughly \rev\ version in
  \cite{brotherston-cut-elimination}.

\bibitem[\protect\citeauthoryear{Brotherston and
  Simpson}{2011}]{brotherston-cut-elimination}
James Brotherston and Alex Simpson.
\newblock Sequent calculi for induction and infinite descent.
\newblock {\em {\jlcname}}, 21:1177--1216, 2011.
\newblock Thoroughly \rev\ version of \cite{DBLP:conf/tableaux/Brotherston05}
  and \cite{DBLP:conf/lics/BrotherstonS07}. Received \Apr\,3, 2009. Published
  online \Sep\,30, 2010, \url{http://dx.doi.org/10.1093/logcom/exq052}.

\bibitem[\protect\citeauthoryear{Brotherston}{2005}]{DBLP:conf/tableaux/Brothe%
rston05}
James Brotherston.
\newblock Cyclic proofs for first-order logic with inductive definitions.
\newblock 2005.
\newblock In \cite[\PP{78}{92}]{fourteenthTABLEAUfive}. Thoroughly \rev\
  version in \cite{brotherston-cut-elimination}.

\bibitem[\protect\citeauthoryear{Brown}{2012}]{satallax}
Chad~E. Brown.
\newblock {\SATALLAX}: An automatic higher-order prover.
\newblock 2012.
\newblock In \cite[\PP{111}{117}]{sixthIJCARtwelve}.

\bibitem[\protect\citeauthoryear{Broy}{1989}]{broy-1989}
Manfred Broy, editor.
\newblock {\em Constructive Methods in Computing Science}, number {F\,55} in
  NATO ASI Series. \springerverlag, 1989.

\bibitem[\protect\citeauthoryear{Buch and
  Hillenbrand{\protectedhillenbrandindex}}{1996}]{waldmeister}
Armin Buch and Thomas Hillenbrand{\protectedhillenbrandindex}.
\newblock {\em {\WALDMEISTER}: Development of a High Performance
  Completion-Based Theorem Prover}.
\newblock {SEKI-Report SR--96--01 (ISSN 1860--5931)}. {SEKI Publications},
  \FBinfshort, \uniKLshort, 1996.
\newblock \url{agent.informatik.uni-kl.de/seki/1996/Buch.SR-96-01.ps.gz}.

\bibitem[\protect\citeauthoryear{Bundy{\protectedbundyindex} \bgroup \em et
  al.\egroup }{1989}]{bundy-recursion-analysis}
Alan Bundy{\protectedbundyindex}, Frank~van Harmelen, Jane Hesketh, Alan
  Smaill, and Andrew Stevens.
\newblock A rational reconstruction and extension of recursion analysis.
\newblock 1989.
\newblock In \cite[\PP{359}{365}]{ijcai11}.

\bibitem[\protect\citeauthoryear{Bundy{\protectedbundyindex} \bgroup \em et
  al.\egroup }{1990}]{oysterclam}
Alan Bundy{\protectedbundyindex}, Frank~van Harmelen, Christian Horn, and Alan
  Smaill.
\newblock The {\OYSTERCLAM} system.
\newblock 1990.
\newblock In \cite[\PP{647}{648}]{tenthCADEninety}.

\bibitem[\protect\citeauthoryear{Bundy{\protectedbundyindex} \bgroup \em et
  al.\egroup }{1991}]{rippling}
Alan Bundy{\protectedbundyindex}, Andrew Stevens, Frank~van Harmelen, Andrew
  Ireland, and Alan Smaill.
\newblock {\em Rippling: A Heuristic for Guiding Inductive Proofs}.
\newblock 1991.
\newblock \daireport{567}\@. Also in
  \artificialintelligenceprintyear{1993}{62}{185}{253}.

\bibitem[\protect\citeauthoryear{Bundy{\protectedbundyindex} \bgroup \em et
  al.\egroup }{2005}]{rippling-book}
Alan Bundy{\protectedbundyindex}, Dieter Hutter{\protectedhutterindex}, David
  Basin, and Andrew Ireland.
\newblock {\em Rippling: Meta-Level Guidance for Mathematical Reasoning}.
\newblock \cambridgeunipress, 2005.

\bibitem[\protect\citeauthoryear{Bundy{\protectedbundyindex}}{1988}]{bundy-ind%
uctive-proof-planning}
Alan Bundy{\protectedbundyindex}.
\newblock {\em The use of Explicit Plans to Guide Inductive Proofs}.
\newblock 1988.
\newblock \daireport{349}\@. Short version in
  \cite[\PP{111}{120}]{ninthCADEeightyeight}.

\bibitem[\protect\citeauthoryear{Bundy{\protectedbundyindex}}{1989}]{science-o%
f-reasoning}
Alan Bundy{\protectedbundyindex}.
\newblock {\em A Science of Reasoning}.
\newblock 1989.
\newblock \daireport{445}\@. Also in \cite[\PP{178}{198}]{honor-robinson}.

\bibitem[\protect\citeauthoryear{Bundy{\protectedbundyindex}}{1994}]{twelvethC%
ADEninetyfour}
Alan Bundy{\protectedbundyindex}, editor.
\newblock {\em {\thetwelvethCADEninetyfour}}, number 814 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 1994.

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

\bibitem[\protect\citeauthoryear{Burstall{\protectedburstallindex} \bgroup \em
  et al.\egroup }{1971}]{pop2}
Rod~M. Burstall{\protectedburstallindex}, John~S. Collins, and Robin~J.
  Popplestone.
\newblock {\em Programming in\/ {\sc POP--2}}.
\newblock \uniEBshort\ Press, 1971.

\bibitem[\protect\citeauthoryear{Burstall{\protectedburstallindex}}{1969}]{bur%
stall-1969}
Rod~M. Burstall{\protectedburstallindex}.
\newblock Proving properties of programs by structural induction.
\newblock {\em The Computer Journal}, 12:48--51, 1969.
\newblock Received \Apr\,1968, \rev\,\Aug\,1968.

\bibitem[\protect\citeauthoryear{Bussey}{1917}]{maurolycus}
W.~H. Bussey.
\newblock The origin of mathematical induction.
\newblock {\em {\americanmathematicalmonthlyname}}, XXIV:199--207, 1917.

\bibitem[\protect\citeauthoryear{Bussotti}{2006}]{From-Fermat-to-Gauss}
Paolo Bussotti.
\newblock {\em {From \fermat\ to \gauss: indefinite descent and methods of
  reduction in number theory}}.
\newblock Number~55 in Algorismus. \Dr\ Erwin Rauner Verlag, \Augsburg, 2006.

\bibitem[\protect\citeauthoryear{Cajori}{1918}]{cajori-1918}
Florian Cajori.
\newblock Origin of the name ``mathematical induction".
\newblock {\em {\americanmathematicalmonthlyname}}, 25:197--201, 1918.

\bibitem[\protect\citeauthoryear{Church}{1946}]{churchbourbaki}
Alonzo Church.
\newblock {Review of \cite{bourbaki-set-theory-results-1st-edn}}.
\newblock {\em \jslname}, 11:91, 1946.

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

\bibitem[\protect\citeauthoryear{Cohn}{1965}]{cohn-1965}
Paul~Moritz Cohn.
\newblock {\em Universal Algebra}.
\newblock Harper \& Row, \NewYork, 1965.
\newblock \nth 1\,\edn. \nth 2\,\rev\,\edn\ is \cite{cohn-1981}.

\bibitem[\protect\citeauthoryear{Cohn}{1981}]{cohn-1981}
Paul~Moritz Cohn.
\newblock {\em Universal Algebra}.
\newblock Number~6 in Mathematics and Its Applications. \DReidelpublishing,
  1981.
\newblock \nth 2\,\rev\,\edn\ (\nth 1\,\edn\ is \cite{cohn-1965}).

\bibitem[\protect\citeauthoryear{Comon}{1997}]{eighthRTAninetyseven}
Hubert Comon, editor.
\newblock {\em {\theeighthRTAninetyseven}}, number 1232 in Lecture Notes in
  Computer Science. \springerverlag, 1997.

\bibitem[\protect\citeauthoryear{Comon}{2001}]{comonAR}
Hubert Comon.
\newblock Inductionless induction.
\newblock 2001.
\newblock In \cite[\Vol\,I, \PP{913}{970}]{HandbookAR}.

\bibitem[\protect\citeauthoryear{Constable \bgroup \em et al.\egroup
  }{1985}]{nuprl-book}
Robert~L. Constable, Stuart~F. Allen, H.~M. Bromly, W.~R. Cleaveland, J.~F.
  Cremer, R.~W. Harper, Douglas~J. Howe, T.~B. Knoblock, N.~P. Mendler,
  P.~Panangaden, James~T. Sasaki, and Scott~F. Smith.
\newblock {\em Implementing Mathematics with {the\/ \NUPRL} Proof Development
  System}.
\newblock \PrenticeHall, 1985.
\newblock \url{http://www.nuprl.org/book}.

\bibitem[\protect\citeauthoryear{Cooper}{1971}]{ijcai2}
D.~C. Cooper, editor.
\newblock {\em {\Proc\ \nth 2 \IJCAIname\ (\IJCAI), \Sep\,1971, Imperial
  College, \London}}. \morgankaufmannwithoutadds, Los Altos (CA), 1971.
\newblock
  \url{http://ijcai.org/Past%20Proceedings/IJCAI-1971/CONTENT/content.htm}.

\bibitem[\protect\citeauthoryear{DAC}{2001}]{dac/2001}
{\em \Proc\ \nth{38} Design Automation Conference (DAC), Las Vegas (NV), 2001}.
  \acmpress, 2001.

\bibitem[\protect\citeauthoryear{Darlington}{1968}]{darlington-1968}
Jared~L. Darlington.
\newblock Automated theorem proving with equality substitutions and
  mathematical induction.
\newblock 1968.
\newblock In \cite[\PP{113}{127}]{machine-intelligence-3}.

\bibitem[\protect\citeauthoryear{Davis}{2009}]{davis-2009}
Jared Davis.
\newblock {\em A Self-Verifying Theorem Prover}.
\newblock PhD thesis, \unitexasaustin, 2009.

\bibitem[\protect\citeauthoryear{Dedekind{\protect\dedekindindex}}{1888}]{dede%
kind-1888}
Richard Dedekind{\protect\dedekindindex}.
\newblock {\em {Was sind und was sollen die Zahlen}}.
\newblock \vieweg, 1888.
\newblock Also in \cite[\Vol\,3, \PP{335}{391}]{dedekind-1930-32}. Also in
  \cite{dedekind-1969}.

\bibitem[\protect\citeauthoryear{Dedekind{\protect\dedekindindex}}{1930--32}]{%
dedekind-1930-32}
Richard Dedekind{\protect\dedekindindex}.
\newblock {\em {Gesammelte mathematische Werke}}.
\newblock \vieweg, 1930--32.
\newblock \Ed\ by \frickename, \noethername, and {\namefont \Oe ystein Ore}.

\bibitem[\protect\citeauthoryear{Dedekind{\protect\dedekindindex}}{1969}]{dede%
kind-1969}
Richard Dedekind{\protect\dedekindindex}.
\newblock {\em {Wa\es\ sind und wa\es\ sollen die Zahlen? Stetigkeit und
  irrationale Zahlen}}.
\newblock Friedrich Vieweg und Sohn, Braunschweig, 1969.

\bibitem[\protect\citeauthoryear{Dennis \bgroup \em et al.\egroup
  }{2005}]{proofplanningsystems}
Louise~A. Dennis, Mateja Jamnik, and Martin Pollet.
\newblock On the comparison of proof planning systems {\LAMBDACLAM, \OMEGA\
  and\/ \ISAPLANNER}.
\newblock {\em {\ENTCSname}}, 151:93--110, 2005.

\bibitem[\protect\citeauthoryear{Dershowitz and
  Jouannaud}{1990}]{term-rewriting-one}
Nachum Dershowitz and Jean-Pierre Jouannaud.
\newblock Rewrite systems.
\newblock 1990.
\newblock In \cite[\Vol\,B, \PP{243}{320}]{handbook-tcs}.

\bibitem[\protect\citeauthoryear{Dershowitz and
  Lindenstrauss}{1995}]{fourthCTRSninetyfour}
Nachum Dershowitz and Naomi Lindenstrauss, editors.
\newblock {\em {\thefourthCTRSninetyfour}}, number 968 in Lecture Notes in
  Computer Science, 1995.

\bibitem[\protect\citeauthoryear{Dershowitz}{1989}]{thirdRTAeightynine}
Nachum Dershowitz, editor.
\newblock {\em {\thethirdRTAeightynine}}, number 355 in Lecture Notes in
  Computer Science. \springerverlag, 1989.

\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{Euclid{\protect\euclidindex}}{\ca\,300\,\BC}]%
{elements}
\ignorespaces Euclid{\protect\euclidindex}, of~Alexandria.
\newblock {\em Elements}.
\newblock \ca\,300\,\BC.
\newblock Web version without the figures:
  \url{http://www.perseus.tufts.edu/hopper/text?doc=Perseus:text:1999.01.0085}.
  \ English translation: \heathname\ (\ed). {\em The Thirteen Books of\/
  \euclid's Elements}. \cambridgeunipress, 1908; web version without the
  figures:
  \url{http://www.perseus.tufts.edu/hopper/text?doc=Perseus:text:1999.01.0086}.
  English web version (\incl\ figures): {\namefont D. E. Joyce} (\ed). {\em
  \euclid's Elements}.
  \url{http://aleph0.clarku.edu/~djoyce/java/elements/elements.html}, \Dept\
  \Math\ \& \Comp\ \Sci, Clark \Univ, Worcester (MA).

\bibitem[\protect\citeauthoryear{Fermat}{1891\ff}]{fermat-oeuvres}
Pierre Fermat.
\newblock {\em \OE uvres de \fermat}.
\newblock {\gauthiervillars}, 1891\ff.
\newblock \Ed\ by {\namefont Paul Tannery}, {\namefont Charles Henry}.

\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{FOCS}{1980}]{focs21}
{\em {\Proc\ \nth{21} \FOCSname, Syracuse, 1980}}. \ieeepress, 1980.
\newblock \url{http://ieee-focs.org/}.

\bibitem[\protect\citeauthoryear{Fowler}{1994}]{Greeks-induction}
David Fowler.
\newblock Could the {G}reeks have used mathematical induction? {D}id they use
  it?
\newblock {\em \physisname}, XXXI(1):253--265, 1994.

\bibitem[\protect\citeauthoryear{Freudenthal}{1953}]{freudenthal}
Hans Freudenthal.
\newblock {Zur Geschichte der voll\-st\ae n\-digen Induktion}.
\newblock {\em Archives Internationales d'Histoire des Sciences}, 6:17--37,
  1953.

\bibitem[\protect\citeauthoryear{Fribourg}{1986}]{inductionlesshistb}
Laurent Fribourg.
\newblock A strong restriction of the inductive completion procedure.
\newblock 1986.
\newblock In \cite[\PP{105}{116}]{thirteenthICALPeightysix}. Also in
  \jscprintyear{1989}{8}{253}{276}.

\bibitem[\protect\citeauthoryear{Fries{\protectedfriesindex}}{1822}]{fries-vol%
lstaendige-induction}
Jakob~Friedrich Fries{\protectedfriesindex}.
\newblock {\em {Die mathematische Naturphilosophie nach philosophischer Methode
  bearbeitet -- Ein Versuch}}.
\newblock Christian Friedrich Winter, \Heidelberg, 1822.

\bibitem[\protect\citeauthoryear{Fritz}{1945}]{hippa}
Kurt~von Fritz.
\newblock The discovery of incommensurability by {\hippasosname}.
\newblock {\em \annalsofmathematicsname}, 46:242--264, 1945.
\newblock German translation: {\em Die Entdeckung der Inkommensurabilit\ae t
  durch \hippasosnamegerman} in \cite[\PP{271}{308}]{becker-griechische}.

\bibitem[\protect\citeauthoryear{Fuchi and Kott}{1988}]{future-generation}
Kazuhiro Fuchi and Laurent Kott, editors.
\newblock {\em {Programming of Future Generation Computers II: \Proc\ of the
  \nth 2 Franco-Japanese Symposium}}. {\northholland}, 1988.

\bibitem[\protect\citeauthoryear{Gabbay{\protectedgabbayindex} and
  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{Gabbay{\protectedgabbayindex} \bgroup \em et
  al.\egroup }{1994}]{handbooklogicailpvol2}
Dov Gabbay{\protectedgabbayindex}, {\mbox{Ch}}ristopher~John Hogger, and
  J.~Alan Robinson{\protectedrobinsonindex}, editors.
\newblock {\em Handbook of Logic in Artificial Intelligence and Logic
  Programming. {\Vol\,2}: Deduction Methodologies}.
\newblock \oxfordunipress, 1994.

\bibitem[\protect\citeauthoryear{Ganzinger and Stuber}{1992}]{GaSt}
Harald Ganzinger and J{\"u}rgen Stuber.
\newblock {\ITP\ by Consistency for First-Order Clauses}.
\newblock 1992.
\newblock In \cite[\PP{441}{462}]{Hotz-Festschrift}. Also in
  \cite[\PP{226}{241}]{thirdCTRSninetytwo}.

\bibitem[\protect\citeauthoryear{Ganzinger}{1996}]{seventhRTAninetysix}
Harald Ganzinger, editor.
\newblock {\em {\theseventhRTAninetysix}}, number 1103 in Lecture Notes in
  Computer Science. \springerverlag, 1996.

\bibitem[\protect\citeauthoryear{Ganzinger}{1999}]{sixteenthCADEninetynine}
Harald Ganzinger, editor.
\newblock {\em {\thesixteenthCADEninetynine}}, number 1632 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 1999.

\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{Geser}{1995}]{geseraxiomofchoice}
Alfons Geser.
\newblock A principle of non-wellfounded induction.
\newblock 1995.
\newblock In
  \cite[\PP{117}{124}]{Kolloquium-Programmiersprachen-und-Grundlagen-der-Progr%
ammierung}.

\bibitem[\protect\citeauthoryear{Geser}{1996}]{geser-improved-general-path-ord%
er}
Alfons Geser.
\newblock An improved general path order.
\newblock {\em \aaeccname}, 7:469--511, 1996.

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

\bibitem[\protect\citeauthoryear{G{\"o}bel}{1985}]{inductionlesshistc}
Richard G{\"o}bel.
\newblock Completion of globally finite term rewriting systems for inductive
  proofs.
\newblock 1985.
\newblock In \cite[\PP{101}{110}]{gwai9}.

\bibitem[\protect\citeauthoryear{G{\oe
  de{\protectedgoedelindex}l}}{1931}]{goedel}
Kurt G{\oe de{\protectedgoedelindex}l}.
\newblock {\Ue ber formal unentscheidbare S\ae tze der \PM\ und verwandter
  Sy\esi teme I}.
\newblock {\em {\monatsheftempname}}, 38:173--198, 1931.
\newblock With {English} translation also in \cite[\Vol\,I,
  \PP{145}{195}]{goedelcollected}. {English} translation also in
  \cite[\PP{596}{616}]{heijenoort-source-book} and in \cite{goedel-meltzer}.

\bibitem[\protect\citeauthoryear{G{\oe
  de{\protectedgoedelindex}l}}{1962}]{goedel-meltzer}
Kurt G{\oe de{\protectedgoedelindex}l}.
\newblock {\em On formally undecidable propositions of {\PM} and related
  systems}.
\newblock Basic Books, \NewYork, 1962.
\newblock English translation of \cite{goedel} by \meltzername. With an
  introduction by {\namefont R. B. Braithwaite}. \nth 2\,\edn\ by Dover
  Publications, 1992.

\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{Goguen}{1980}]{gogueninductionlessinduction}
Joseph Goguen.
\newblock How to prove algebraic inductive hypotheses without induction.
\newblock 1980.
\newblock In \cite[\PP{356}{373}]{fifthCADEeighty}.

\bibitem[\protect\citeauthoryear{Goldstein{\protectedgoldsteinindex}}{2008}]{c%
atherine-goldstein-fermat-priceton-companion-math-2008}
Catherine Goldstein{\protectedgoldsteinindex}.
\newblock {\fermatname}.
\newblock 2008.
\newblock In \cite[\litsectref{VI.12},
  \PP{740}{741}]{priceton-companion-math-2008}.

\bibitem[\protect\citeauthoryear{Gordon{\protectedgordonindex}}{2000}]{fromLCF%
toHOL}
Mike J.~C. Gordon{\protectedgordonindex}.
\newblock From {\LCF} to {\HOL}: a short history.
\newblock 2000.
\newblock In \cite[\PP{169}{186}]{honorrobinmilner}.
  \url{http://www.cl.cam.ac.uk/~mjcg/papers/HolHistory.pdf}.

\bibitem[\protect\citeauthoryear{Gore \bgroup \em et al.\egroup
  }{2001}]{firstIJCARone}
Rajeev Gore, Alexander Leitsch, and Tobias Nipkow, editors.
\newblock {\em {\thefirstIJCARone}}, number 2083 in Lecture Notes in Artificial
  Intelligence. \springerverlag, 2001.

\bibitem[\protect\citeauthoryear{Gowers \bgroup \em et al.\egroup
  }{2008}]{priceton-companion-math-2008}
Timothy Gowers, June Barrow-Green, and Imre Leader, editors.
\newblock {\em The {\Princetonnostate} Companion to Mathematics}.
\newblock \princetonunipress, 2008.

\bibitem[\protect\citeauthoryear{Graham \bgroup \em et al.\egroup
  }{1976}]{thirdPOPLseventysix}
Susan~L. Graham, Robert~M. Graham, Michael~A. Harrison, William~I. Grosky, and
  Jeffrey~D. Ullman, editors.
\newblock {\em Conference Record of the \nth 3\,\POPLname, Atlanta (GA),
  \Jan\,1976}. \acmpress, 1976.
\newblock \url{http://dl.acm.org/citation.cfm?id=800168}.

\bibitem[\protect\citeauthoryear{Gram{\-}li{\protectedgramlichindex}ch and
  Lindner}{1991}]{unicom}
Bernhard Gram{\-}li{\protectedgramlichindex}ch and Wolfgang Lindner.
\newblock {\em A Guide to {\UNICOM}, an Inductive Theorem Prover Based on
  Rewriting and Completion Techniques}.
\newblock {SEKI-Report SR--91--17 (ISSN 1860--5931)}. {SEKI Publications},
  \FBinfshort, \uniKLshort, 1991.
\newblock
  \url{http://agent.informatik.uni-kl.de/seki/1991/Lindner.SR-91-17.ps.gz}.

\bibitem[\protect\citeauthoryear{Gram{\-}li{\protectedgramlichindex}ch and
  Wirth{\protectedwirthindex}}{1996}]{gwrta}
Bernhard Gram{\-}li{\protectedgramlichindex}ch and Claus-Peter
  Wirth{\protectedwirthindex}.
\newblock Confluence of terminating conditional term rewriting systems
  revisited.
\newblock 1996.
\newblock In \cite[\PP{245}{259}]{seventhRTAninetysix}.

\bibitem[\protect\citeauthoryear{Gram{\-}li{\protectedgramlichindex}ch \bgroup
  \em et al.\egroup }{2012}]{sixthIJCARtwelve}
Bernhard Gram{\-}li{\protectedgramlichindex}ch, Dale~A. Miller, and Uli
  Sattler, editors.
\newblock {\em {\thesixthIJCARtwelve}}, number 7364 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 2012.

\bibitem[\protect\citeauthoryear{Hayes \bgroup \em et al.\egroup
  }{1988}]{machine-intelligence-11}
Jean~E. Hayes, Donald Michie{\protectedmichieindex}, and Judith Richards,
  editors.
\newblock {\em {Proceedings of the \nth{11}\,Annual Machine Intelligence
  Workshop (Machine Intelligence\,11), \Univ\ Strathclyde, \Glasgow, 1985}}.
  \clarendonpress, 1988.
\newblock
  \url{aitopics.org/sites/default/files/classic/Machine_Intelligence_11/Machin%
e_Intelligence_v.11.pdf}.

\bibitem[\protect\citeauthoryear{Heijenoort{\protect\heijenoortindex}}{1971}]{%
heijenoort-source-book}
Jean~van Heijenoort{\protect\heijenoortindex}.
\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{Herbelin}{2009}]{Coq1}
Hugo Herbelin, editor.
\newblock {\em The {\nth 1} {\COQ} Workshop}. {\Inst\ f\ue r Informatik, \Tech\
  \Univ\ \Muenchen}, 2009.
\newblock TUM-I0919,
  \url{http://www.lix.polytechnique.fr/coq/files/coq-workshop-TUM-I0919.pdf}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt and
  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}).

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt and
  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 and
  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}.

\bibitem[\protect\citeauthoryear{Hilbe{\protectedhilbertindex}rt and
  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 and
  Bernays\protect\bernaysindex}{2013}]{grundlagen-german-english-edition-volum%
e-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{Hillenbrand{\protectedhillenbrandindex} and
  L{\oe}chner{\protectedloechnerindex}}{2002}]{HL02}
Thomas Hillenbrand{\protectedhillenbrandindex} and Bernd
  L{\oe}chner{\protectedloechnerindex}.
\newblock The next {\WALDMEISTER} loop.
\newblock 2002.
\newblock In \cite[\PP{486}{500}]{eightteenthCADEtwo}.
  \url{http://www.waldmeister.org}.

\bibitem[\protect\citeauthoryear{Hinchey and
  Bowen}{1999}]{industrial-strength-1999}
Michael~G. Hinchey and Jonathan~P. Bowen, editors.
\newblock {\em Industrial-Strength Formal Methods in Practice}.
\newblock Formal Approaches to Computing and Information Technology (FACIT).
  \springerverlag, 1999.

\bibitem[\protect\citeauthoryear{Hobson and
  Love}{1913}]{5-int-congress-mathematicians-1912}
E.~W. Hobson and A.~E.~H. Love, editors.
\newblock {\em {\Proc\ \nth 5 \Int\ Congress of Mathematicians, \Cambridge,
  Aug\,22--28, 1912}}. \cambridgeunipress, 1913.
\newblock \url{http://gallica.bnf.fr/ark:/12148/bpt6k99444q}.

\bibitem[\protect\citeauthoryear{Howard and Rubin}{1998}]{weakaxiomofchoice}
Paul Howard and Jean~E. Rubin.
\newblock {\em Consequences of the Axiom of Choice}.
\newblock American Math.\ Society, 1998.

\bibitem[\protect\citeauthoryear{Hudlak \bgroup \em et al.\egroup
  }{1999}]{haskell}
Paul Hudlak, John Peterson, and Joseph~H. Fasel.
\newblock A gentle introduction to {\HASKELL}.
\newblock Web only: \url{http://www.haskell.org/tutorial}, 1999.

\bibitem[\protect\citeauthoryear{Huet and
  Hullot}{1980}]{huethullotinductionlessinduction}
G{\'e}rard Huet and Jean-Marie Hullot.
\newblock Proofs by induction in equational theories with constructors.
\newblock 1980.
\newblock In \cite[\PP{96}{107}]{focs21}. Also in
  \jcssprintyear{1982}{25}{239}{266}.

\bibitem[\protect\citeauthoryear{Huet}{1980}]{huet}
G{\'e}rard Huet.
\newblock Confluent reductions: Abstract properties and applications to term
  rewriting systems.
\newblock {\em \jacmname}, 27:797--821, 1980.

\bibitem[\protect\citeauthoryear{Hunt{\protectedhuntindex} and
  Swords}{2009}]{hunt-swords-2009}
Warren~A. Hunt{\protectedhuntindex} and Sol Swords.
\newblock Centaur technology media unit verification.
\newblock 2009.
\newblock In \cite[\PP{353}{367}]{twentyfirstCAVnine}.

\bibitem[\protect\citeauthoryear{Hunt{\protectedhuntindex}}{1985}]{hunt-1985}
Warren~A. Hunt{\protectedhuntindex}.
\newblock {\em {FM8501}: A Verified Microprocessor}.
\newblock PhD thesis, \unitexasaustin, 1985.
\newblock Also published as \cite{hunt-1994}.

\bibitem[\protect\citeauthoryear{Hunt{\protectedhuntindex}}{1989}]{hunt-1989}
Warren~A. Hunt{\protectedhuntindex}.
\newblock Microprocessor design verification.
\newblock {\em \jarname}, 5:429--460, 1989.

\bibitem[\protect\citeauthoryear{Hunt{\protectedhuntindex}}{1994}]{hunt-1994}
Warren~A. Hunt{\protectedhuntindex}.
\newblock {\em {FM8501}: A Verified Microprocessor}.
\newblock Number 795 in Lecture Notes in Artificial Intelligence.
  \springerverlag, 1994.
\newblock Originally published as \cite{hunt-1985}.

\bibitem[\protect\citeauthoryear{Hutter{\protectedhutterindex} and
  Bundy{\protectedbundyindex}}{1999}]{inductioncontest}
Dieter Hutter{\protectedhutterindex} and Alan Bundy{\protectedbundyindex}.
\newblock The design of the {CADE-16 Inductive Theorem Prover Contest}.
\newblock 1999.
\newblock In \cite[\PP{374}{377}]{sixteenthCADEninetynine}.

\bibitem[\protect\citeauthoryear{Hutter{\protectedhutterindex} and
  Sengler}{1996}]{inkanext}
Dieter Hutter{\protectedhutterindex} and Claus Sengler.
\newblock {\INKA:} the next generation.
\newblock 1996.
\newblock In \cite[\PP{288}{292}]{thirteenthCADEninetysix}.

\bibitem[\protect\citeauthoryear{Hutter{\protectedhutterindex} and
  Stephan}{2005}]{siekmann-60}
Dieter Hutter{\protectedhutterindex} and Werner Stephan, editors.
\newblock {\em Mechanizing Mathematical Reasoning: Essays in Honor of\/
  {\siekmannname} on the Occasion of His {\nth{60}\,}Birthday}.
\newblock Number 2605 in Lecture Notes in Artificial Intelligence.
  \springerverlag, 2005.

\bibitem[\protect\citeauthoryear{Hutter{\protectedhutterindex}}{1990}]{hutter-%
rippling}
Dieter Hutter{\protectedhutterindex}.
\newblock Guiding inductive proofs.
\newblock 1990.
\newblock In \cite[\PP{147}{161}]{tenthCADEninety}.

\bibitem[\protect\citeauthoryear{Ireland and
  Bundy{\protectedbundyindex}}{1994}]{failure-guide-induction}
Andrew Ireland and Alan Bundy{\protectedbundyindex}.
\newblock {\em Productive Use of Failure in Inductive Proof}.
\newblock 1994.
\newblock \daireport{716}\@. Also in: \jarprintyear{1996}{16}{79}{111}.

\bibitem[\protect\citeauthoryear{Jamnik \bgroup \em et al.\egroup
  }{2003}]{automatic-learning-proof-planning}
Mateja Jamnik, Manfred Kerber, Martin Pollet, and {\mbox{Ch}}ristoph
  Benz{\-}m{\ue}ller{\protectedbenzmuellerindex}.
\newblock Automatic learning of proof methods in proof planning.
\newblock {\em {\ljigplname}}, 11:647--673, 2003.

\bibitem[\protect\citeauthoryear{Jouannaud and
  Kounalis}{1986}]{inductionlesshista}
Jean-Pierre Jouannaud and Emmanu{\ewithtrema}l Kounalis.
\newblock Automatic proofs by induction in equational theories without
  constructors.
\newblock 1986.
\newblock In \cite[\PP{358}{366}]{lics1}. Also in
  \informationandcomputationprintyear{1989}{82}{1}{33}, 1989.

\bibitem[\protect\citeauthoryear{Kaplan and
  Jouannaud}{1988}]{firstCTRSeightyseven}
St{\'e}phane Kaplan and Jean-Pierre Jouannaud, editors.
\newblock {\em {\thefirstCTRSeightyseven}}, number 308 in Lecture Notes in
  Computer Science, 1988.

\bibitem[\protect\citeauthoryear{Kaplan and Okada}{1991}]{secondCTRSninety}
St{\'e}phane Kaplan and Mitsuhiro Okada, editors.
\newblock {\em {\thesecondCTRSninety}}, number 516 in Lecture Notes in Computer
  Science, 1991.

\bibitem[\protect\citeauthoryear{Kapur and Musser}{1986}]{kapur2}
Deepak Kapur and David~R. Musser.
\newblock Inductive reasoning with incomplete specifications.
\newblock 1986.
\newblock In \cite[\PP{367}{377}]{lics1}.

\bibitem[\protect\citeauthoryear{Kapur and Musser}{1987}]{kapur1}
Deepak Kapur and David~R. Musser.
\newblock Proof by consistency.
\newblock {\em \artificialintelligencename}, 31:125--157, 1987.

\bibitem[\protect\citeauthoryear{Kapur and
  Subramaniam}{1996}]{mutualexplicitinduction}
Deepak Kapur and Mahadevan Subramaniam.
\newblock Automating induction over mutually recursive functions.
\newblock 1996.
\newblock In \cite[\PP{117}{131}]{fifthAMASTninetysix}.

\bibitem[\protect\citeauthoryear{Kapur and Zhang}{1989}]{rrl}
Deepak Kapur and Han{\-}tao Zhang.
\newblock An overview of {Rewrite Rule Laboratory~(\/\RRL)}.
\newblock 1989.
\newblock In \cite[\PP{559}{563}]{thirdRTAeightynine}. Journal version is
  \cite{Kapur95}.

\bibitem[\protect\citeauthoryear{Kapur and Zhang}{1995}]{Kapur95}
Deepak Kapur and Han{\-}tao Zhang.
\newblock An overview of {Rewrite Rule Laboratory~(\/\RRL)}.
\newblock {\em Computers and Mathematics with Applications}, 29(2):91--114,
  1995.

\bibitem[\protect\citeauthoryear{Kapur}{1992}]{eleventhCADEninetytwo}
Deepak Kapur, editor.
\newblock {\em {\theeleventhCADEninetytwo}}, number 607 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 1992.

\bibitem[\protect\citeauthoryear{Katz}{1998}]{katz-history}
Victor~J. Katz.
\newblock {\em A History of Mathematics: An Introduction}.
\newblock \addisonwesley, 1998.
\newblock \nth 2 \edn.

\bibitem[\protect\citeauthoryear{Kaufmann{\protectedkaufmannindex} \bgroup \em
  et al.\egroup }{2000a}]{ACLTWO-CASESTUDIES}
Matt Kaufmann{\protectedkaufmannindex}, Panagiotis Manolios, and J~Strother
  Moore{\protect\mooreindex}, editors.
\newblock {\em Computer-Aided Reasoning: {\ACLTWO} Case Studies}.
\newblock Number~4 in Advances in Formal Methods. \kluwer, 2000.
\newblock With a foreword from the series editor {\namefont Mike Hinchey}.

\bibitem[\protect\citeauthoryear{Kaufmann{\protectedkaufmannindex} \bgroup \em
  et al.\egroup }{2000b}]{ACLTWO}
Matt Kaufmann{\protectedkaufmannindex}, Panagiotis Manolios, and J~Strother
  Moore{\protect\mooreindex}.
\newblock {\em Computer-Aided Reasoning: An Approach}.
\newblock Number~3 in Advances in Formal Methods. \kluwer, 2000.
\newblock With a foreword from the series editor {\namefont Mike Hinchey}.

\bibitem[\protect\citeauthoryear{Knuth and Bendix}{1970}]{KB70}
Donald~E Knuth and Peter~B. Bendix.
\newblock Simple word problems in universal algebra.
\newblock 1970.
\newblock In \cite[\PP{263}{297}]{leech-1970}.

\bibitem[\protect\citeauthoryear{Kodratoff}{1988}]{eighthECAIeightyeight}
Yves Kodratoff, editor.
\newblock {\em \Proc\ \nth 8 \ECAIname\ (ECAI)}. \pitman, 1988.

\bibitem[\protect\citeauthoryear{Kott}{1986}]{thirteenthICALPeightysix}
Laurent Kott, editor.
\newblock {\em {\nth{13} \ICALPname, Rennes (France)}}, number 226 in Lecture
  Notes in Computer Science. \springerverlag, 1986.

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

\bibitem[\protect\citeauthoryear{Kowalski{\protectedkowalskiindex}}{1988}]{kow%
alski-1988}
Robert~A. Kowalski{\protectedkowalskiindex}.
\newblock The early years of logic programming.
\newblock {\em \commacmname}, 31:38--43, 1988.

\bibitem[\protect\citeauthoryear{Kreisel}{1965}]{induction-no-cut}
Georg Kreisel.
\newblock Mathematical logic.
\newblock 1965.
\newblock {In \cite[\Vol\,III, \PP{95}{195}]{saaty}}.

\bibitem[\protect\citeauthoryear{K{\"u}chlin}{1989}]{inductionlesshistd}
Wolfgang K{\"u}chlin.
\newblock Inductive completion by ground proof transformation.
\newblock 1989.
\newblock In \cite[\Vol\,2, \PP{211}{244}]{kaci-nivat}.

\bibitem[\protect\citeauthoryear{K{\"u}hler{\protectedkuehlerindex} and
  Wirth{\protectedwirthindex}}{1996}]{kwspec}
Ulrich K{\"u}hler{\protectedkuehlerindex} and Claus-Peter
  Wirth{\protectedwirthindex}.
\newblock {\em Conditional Equational Specifications of Data Types with Partial
  Operations for Inductive Theorem Proving}.
\newblock {SEKI-Report SR--1996--11 (ISSN 1437--4447)}. {SEKI Publications},
  \FBinfshort, \uniKLshort, 1996.
\newblock \PPcount{24}, \www\url{/p/rta97}. Short version is \cite{kwspec2}.

\bibitem[\protect\citeauthoryear{K{\"u}hler{\protectedkuehlerindex} and
  Wirth{\protectedwirthindex}}{1997}]{kwspec2}
Ulrich K{\"u}hler{\protectedkuehlerindex} and Claus-Peter
  Wirth{\protectedwirthindex}.
\newblock Conditional equational specifications of data types with partial
  operations for inductive theorem proving.
\newblock 1997.
\newblock In \cite[\PP{38}{52}]{eighthRTAninetyseven}. Extended version is
  \cite{kwspec}.

\bibitem[\protect\citeauthoryear{K{\"u}hler{\protectedkuehlerindex}}{1991}]{ku%
ehler-master}
Ulrich K{\"u}hler{\protectedkuehlerindex}.
\newblock {Ein funktionaler und struktureller Vergleich verschiedener
  Induktion\esi beweiser}.
\newblock (English translation of title: ``A functional and structural
  comparsion of several inductive theorem-proving systems'' (\INKA, LP (Larch
  Prover), \NQTHM, \RRL, \UNICOM)). \PPcount{vi+143}, \Diplomarbeit,
  \FBinfshort, \uniKLshort, 1991.

\bibitem[\protect\citeauthoryear{K{\"u}hler{\protectedkuehlerindex}}{2000}]{ku%
ehlerdiss}
Ulrich K{\"u}hler{\protectedkuehlerindex}.
\newblock {\em A Tactic-Based Inductive Theorem Prover for Data Types with
  Partial Operations}.
\newblock \infixverlag, 2000.
\newblock \PhDthesis, \uniKLshort, {ISBN 1586031287}, \www\url{/p/kuehlerdiss}.

\bibitem[\protect\citeauthoryear{Lambert}{1764}]{lambert-1764}
Johann~Heinrich Lambert.
\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, 1764.
\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\ae 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{Lankford}{1980}]{inductionlessinduction1}
Dalla{\es}~S. Lankford.
\newblock Some remarks on inductionless induction.
\newblock Memo MTP-11, \Math\ \Dept, Louisiana \Tech\ \Univ, Ruston (LA), 1980.

\bibitem[\protect\citeauthoryear{Lankford}{1981}]{inductionlessinduction2}
Dalla{\es}~S. Lankford.
\newblock A simple explanation of inductionless induction.
\newblock Memo MTP-14, \Math\ \Dept, Louisiana \Tech\ \Univ, Ruston (LA), 1981.

\bibitem[\protect\citeauthoryear{Lassez and Plotkin}{1991}]{honor-robinson}
Jean-Louis Lassez and Gordon~D. Plotkin, editors.
\newblock {\em Computational Logic --- Essays in Honor of\/ {\robinsonname}}.
\newblock \mitpress, 1991.

\bibitem[\protect\citeauthoryear{Leech}{1970}]{leech-1970}
John Leech, editor.
\newblock {\em {Computational Word Problems in Abstract Algebra --- \Proc\ of a
  \Conf\ held at \Oxford, under the auspices of the Science Research Council,
  Atlas Computer Laboratory, \nth{29}\,\Aug\ to \nth 2\,\Sep\,\,1967}}.
  \pergamonpress, 1970.
\newblock With a foreword by {\namefont J. Howlett}.

\bibitem[\protect\citeauthoryear{Leeuwen}{1990}]{handbook-tcs}
Jan~van Leeuwen, editor.
\newblock {\em Handbook of Theoretical Computer \Sci}.
\newblock \mitpress, 1990.

\bibitem[\protect\citeauthoryear{LICS}{1986}]{lics1}
{\em {\Proc\ \nth 1 \LICSname, \CambridgeMassachusetts, 1986}}. \ieeepress,
  1986.
\newblock \licsarchive\url{1986}.

\bibitem[\protect\citeauthoryear{LICS}{1988}]{lics3}
{\em {\Proc\ \nth 3 \LICSname, Edinburgh, 1988}}. \ieeepress, 1988.
\newblock \licsarchive\url{1988}.

\bibitem[\protect\citeauthoryear{LICS}{2007}]{lics22}
{\em {\Proc\ \nth{22} \LICSname, \Breslau, 2007}}. \ieeepress, 2007.
\newblock \licsarchive\url{2007}.

\bibitem[\protect\citeauthoryear{L{\oe}chner{\protectedloechnerindex}}{2006}]{%
loechner-lpo}
Bernd L{\oe}chner{\protectedloechnerindex}.
\newblock Things to know when implementing {LPO}.
\newblock {\em \artificialintelligencetools}, 15:53--79, 2006.

\bibitem[\protect\citeauthoryear{Lusk and
  Overbeek}{1988}]{ninthCADEeightyeight}
Ewing Lusk and Ross Overbeek, editors.
\newblock {\em {\theninthCADEeightyeight}}, number 310 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 1988.

\bibitem[\protect\citeauthoryear{Mahoney}{1994}]{fermat-career}
Michael~Sean Mahoney.
\newblock {\em {The Mathematical Career of\/ \fermatnoblename\ 1601--1665}}.
\newblock \princetonunipress, 1994.
\newblock \nth 2\,\rev\,\edn\ (\nth 1\,\edn\,1973).

\bibitem[\protect\citeauthoryear{Marchisotto and Smit{\protect\index{Smith,
  James T.}}h}{2007}]{smith-pieri}
Elena~Anne Marchisotto and James~T. Smit{\protect\index{Smith, James T.}}h.
\newblock {\em The Legacy of {\pieriname} in Geometry and Arithmetic}.
\newblock \birkhaeuser, 2007.

\bibitem[\protect\citeauthoryear{Margaria}{1995}]{Kolloquium-Programmiersprach%
en-und-Grundlagen-der-Programmierung}
Tiziana Margaria, editor.
\newblock {\em {Kolloquium Programmiersprachen und Grundlagen der
  Programmierung}}, 1995.
\newblock \Tech\ Report MIP--9519, \Univ\ Passau.

\bibitem[\protect\citeauthoryear{McCarthy \bgroup \em et al.\egroup
  }{1965}]{LISP}
John McCarthy, Paul~W. Abrahams, D.~J. Edwards, T.~P. Hart, and M.~I. Levin.
\newblock {\em {LISP 1.5} Programmer's Manual}.
\newblock \mitpress, 1965.

\bibitem[\protect\citeauthoryear{McRobbie and
  Slaney}{1996}]{thirteenthCADEninetysix}
Michael~A. McRobbie and John~K. Slaney, editors.
\newblock {\em {\thethirteenthCADEninetysix}}, number 1104 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 1996.

\bibitem[\protect\citeauthoryear{Melis \bgroup \em et al.\egroup
  }{2008}]{proof_planning_with_multiple_strategies}
Erica Melis, Andreas Meier, and J{\"o}rg Siek{\-}mann{\protect\siekmannindex}.
\newblock Proof planning with multiple strategies.
\newblock {\em \artificialintelligencename}, 172:656--684, 2008.
\newblock Received \May\,2, 2006. Published online \Nov\,22, 2007.
  \url{http://dx.doi.org/10.1016/j.artint.2007.11.004}.

\bibitem[\protect\citeauthoryear{Meltzer{\protectedmeltzerindex} and
  Michie{\protectedmichieindex}}{1972}]{machine-intelligence-7}
Bernard Meltzer{\protectedmeltzerindex} and Donald
  Michie{\protectedmichieindex}, editors.
\newblock {\em {Proceedings of the \nth 7\,Annual Machine Intelligence Workshop
  (Machine Intelligence\,7), \EB, 1971}}. \uniEBshort\ Press, 1972.
\newblock
  \url{http://aitopics.org/sites/default/files/classic/Machine%20Intelligence%%
203/Machine%20Intelligence%20v3.pdf}.

\bibitem[\protect\citeauthoryear{Meltzer{\protectedmeltzerindex}}{1975}]{meltz%
er-1975}
Bernard Meltzer{\protectedmeltzerindex}.
\newblock {Department of A.I. -- Univ.\ of \EB}.
\newblock {\em ACM SIGART Bulletin}, 50:5, 1975.

\bibitem[\protect\citeauthoryear{Michie{\protectedmichieindex}}{1968}]{machine%
-intelligence-3}
Donald Michie{\protectedmichieindex}, editor.
\newblock {\em {Proceedings of the \nth 3\,Annual Machine Intelligence Workshop
  (Machine Intelligence\,3), \EB, 1967}}. \uniEBshort\ Press, 1968.
\newblock
  \url{http://aitopics.org/sites/default/files/classic/Machine%20Intelligence%%
203/Machine%20Intelligence%20v3.pdf}.

\bibitem[\protect\citeauthoryear{Milner}{1972}]{milner-1972}
Robin Milner.
\newblock Logic for computable functions --- description of a machine
  interpretation.
\newblock Technical Report Memo\,AIM--169, STAN--CS--72--288, \Dept\ \CS,
  Stanford University, 1972.
\newblock
  \url{ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/72/288/CS-TR-72-288.p%
df}.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex} \bgroup \em et
  al.\egroup }{1998}]{moore-lynch-kaufmann-1998}
J~Strother Moore{\protect\mooreindex}, Thomas Lynch, and Matt
  Kaufmann{\protectedkaufmannindex}.
\newblock A mechanically checked proof of the correctness of the kernel of the
  {AMD5K86} floating point division algorithm.
\newblock {\em IEEE Transactions on Computers}, 47:913--926, 1998.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex}}{1973}]{moore-1973}
J~Strother Moore{\protect\mooreindex}.
\newblock {\em Computational Logic: Structure Sharing and Proof of Program
  Properties}.
\newblock PhD thesis, \Dept\ \AI, \uniEBshort, 1973.
\newblock \url{http://hdl.handle.net/1842/2245}.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex}}{1975a}]{moore-197%
5}
J~Strother Moore{\protect\mooreindex}.
\newblock Introducing iteration into the {\protect\PURELISPTP}.
\newblock Technical Report CSL\,74--3, Xerox, Palo Alto Research Center, 3333
  Coyote Hill Rd., Palo Alto (CA), 1975.
\newblock \PPcount{ii+37}, Received \Dec\,1974, \rev\,\Mar\,1975. Short version
  is \cite{moore-1975-short}.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex}}{1975b}]{moore-197%
5-short}
J~Strother Moore{\protect\mooreindex}.
\newblock Introducing iteration into the {\protect\PURELISPTP}.
\newblock {\em \ieeetranssename}, 1:328--338, 1975.
\newblock \url{http://doi.ieeecomputersociety.org/10.1109/TSE.1975.6312857}.
  Long version is \cite{moore-1975}.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex}}{1979}]{moore-1979}
J~Strother Moore{\protect\mooreindex}.
\newblock A mechanical proof of the termination of {\takeuti's} function.
\newblock {\em Information Processing Letters}, 9:176--181, 1979.
\newblock Received \Jul\,13, 1979. \Rev\ \Sep\,5, 1979.
  \url{http://dx.doi.org/10.1016/0020-0190(79)90063-2}.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex}}{1981}]{moore-1981}
J~Strother Moore{\protect\mooreindex}.
\newblock Text editing primitives --- the {TXDT} package.
\newblock Technical Report CSL\,81--2, Xerox, Palo Alto Research Center, 3333
  Coyote Hill Rd., Palo Alto (CA), 1981.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex}}{1989a}]{moore-198%
9-2}
J~Strother Moore{\protect\mooreindex}.
\newblock A mechanically verified language implementation.
\newblock {\em \jarname}, 5:461--492, 1989.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex}}{1989b}]{moore-198%
9-1}
J~Strother Moore{\protect\mooreindex}.
\newblock System verification.
\newblock {\em \jarname}, 5:409--410, 1989.

\bibitem[\protect\citeauthoryear{Moskewicz \bgroup \em et al.\egroup
  }{2001}]{chaff}
Matthew~W. Moskewicz, Conor~F. Madigan, Ying Zhao, Lintao Zhang, and Sharad
  Malik.
\newblock {\sc Chaff}: Engineering an efficient {SAT} solver.
\newblock 2001.
\newblock In \cite[\PP{530}{535}]{dac/2001}.

\bibitem[\protect\citeauthoryear{Musser}{1980}]{musserinductionlessinduction}
David~R. Musser.
\newblock On proving inductive properties of abstract data types.
\newblock 1980.
\newblock In \cite[\PP{154}{162}]{seventhPOPLeighty}.
  \url{http://dl.acm.org/citation.cfm?id=567461}.

\bibitem[\protect\citeauthoryear{Nilsson}{1973}]{ijcai3}
Nils~J. Nilsson, editor.
\newblock {\em {\Proc\ \nth 3 \IJCAIname\ (\IJCAI), \StanfordCA}}. Stanford
  Research Institute, Publications \Dept, \StanfordCA, 1973.
\newblock
  \url{http://ijcai.org/Past%20Proceedings/IJCAI-73/CONTENT/content.htm}.

\bibitem[\protect\citeauthoryear{Padawitz}{1996}]{padawitzjsc}
Peter Padawitz.
\newblock Inductive theorem proving for design specifications.
\newblock {\em \jscname}, 21:41--99, 1996.

\bibitem[\protect\citeauthoryear{Padoa{\protectedpadoaindex}}{1913}]{padoa-191%
3}
Alessandro Padoa{\protectedpadoaindex}.
\newblock {La valeur et les r\^oles du principe d'induction math\'ematique}.
\newblock 1913.
\newblock In \cite[\PP{471}{479}]{5-int-congress-mathematicians-1912}.

\bibitem[\protect\citeauthoryear{Pascal}{1954}]{pascal}
Blaise Pascal.
\newblock {\em {\OE}uvres Compl{\`e}tes}.
\newblock Gallimard, Paris, 1954.
\newblock \Ed\ by {\namefont Jacques Chevalier}.

\bibitem[\protect\citeauthoryear{Paulson}{1996}]{Pau96}
Lawrence~C. Paulson.
\newblock {\em {\ml} for the Working Programmer}.
\newblock \cambridgeunipress, 1996.
\newblock \nth 2\,\edn\ (\nth 1\,\edn\,1991).

\bibitem[\protect\citeauthoryear{Peano{\protect\peanoindex}}{1889}]{peanonovam%
ethodo}
Guiseppe Peano{\protect\peanoindex}.
\newblock {\em Arithmetices principia, novo methodo exposita}.
\newblock Fratelli Bocca, \Torino, 1889.

\bibitem[\protect\citeauthoryear{P{\'e}ter{\protectedpeterindex}}{1951}]{peter%
-1951}
R{\'o}sza P{\'e}ter{\protectedpeterindex}.
\newblock {\em Rekursive Funktionen}.
\newblock Akad.~Kiad\'o, \Budapest, 1951.

\bibitem[\protect\citeauthoryear{Pieri{\protect\pieriindex}}{1908}]{pieri}
Mario Pieri{\protect\pieriindex}.
\newblock Sopra gli assiomi aritmetici.
\newblock {\em Il Bollettino delle seduta della Accademia Gioenia di Scienze
  Naturali in Catania}, Series\,2, 1--2:26--30, 1908.
\newblock Written \Dec\,1907. Received \Jan\,8, 1908. English translation {\em
  On the Axioms of Arithmetic}\/ in \cite[\litsectref{4.2},
  \PP{308}{313}]{smith-pieri}.

\bibitem[\protect\citeauthoryear{Plotkin \bgroup \em et al.\egroup
  }{2000}]{honorrobinmilner}
Gordon~D. Plotkin, Colin Stirling, and Mads Tofte, editors.
\newblock {\em Proof, Language, and Interaction, Essays in Honour of
  {\milnername}}.
\newblock \mitpress, 2000.

\bibitem[\protect\citeauthoryear{Presburger{\protect\presburgerindex}}{1930}]{%
presburger}
Moj{\zwithdot}esz Presburger{\protect\presburgerindex}.
\newblock {\Ue ber die Vollst\ae ndigkeit eine\es\ gewissen Sy\esi tem\es\ der
  Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation
  hervortritt}.
\newblock In {\em Sprawozdanie z I Kongresu metematyk\'ow kraj\'ow s\l
  owianskich, Warszawa 1929 (Comptes-rendus du \frenchnth 1 Congr\`es des
  Math\'ematiciens des Pays Slaves, Varsovie 1929)}, pages 92--101+395, 1930.
\newblock Remarks and {E}nglish translation in
  \cite{presburger-remarks-translation}.

\bibitem[\protect\citeauthoryear{Protzen{\protectedprotzenindex}}{1994}]{protz%
enlazy}
Martin Protzen{\protectedprotzenindex}.
\newblock Lazy generation of induction hypotheses.
\newblock 1994.
\newblock In \cite[\PP{42}{56}]{twelvethCADEninetyfour}.

\bibitem[\protect\citeauthoryear{Protzen{\protectedprotzenindex}}{1995}]{protz%
endiss}
Martin Protzen{\protectedprotzenindex}.
\newblock {\em Lazy Generation of Induction Hypotheses and Patching Faulty
  Conjectures}.
\newblock \infixverlag, 1995.
\newblock \PhDthesis.

\bibitem[\protect\citeauthoryear{Protzen{\protectedprotzenindex}}{1996}]{protz%
enpatching}
Martin Protzen{\protectedprotzenindex}.
\newblock Patching faulty conjectures.
\newblock 1996.
\newblock In \cite[\PP{77}{91}]{thirteenthCADEninetysix}.

\bibitem[\protect\citeauthoryear{Rabinovitch}{1970}]{Ravinovitch-Gershon}
Nachum~L. Rabinovitch.
\newblock Rabbi {\gersonname} and the origins of mathematical induction.
\newblock {\em Archive for History of Exact Sciences}, 6:237--248, 1970.
\newblock Received \Jan\,12, 1970.

\bibitem[\protect\citeauthoryear{Reddy}{1977}]{ijcai5}
Ray Reddy, editor.
\newblock {\em {\Proc\ \nth 5 \IJCAIname\ (\IJCAI), \CambridgeMassachusetts}}.
  \Dept\ of \CS, \CMU, \CambridgeMassachusetts, 1977.
\newblock \url{http://ijcai.org/Past%20Proceedings}.

\bibitem[\protect\citeauthoryear{Reddy}{1990}]{reddy}
Uday~S. Reddy.
\newblock Term rewriting induction.
\newblock 1990.
\newblock \cite[\PP{162}{177}]{tenthCADEninety}.

\bibitem[\protect\citeauthoryear{Riazanov and Voronkov}{2001}]{vampire01}
Alexander Riazanov and Andrei Voronkov.
\newblock Vampire~1.1 (system description).
\newblock 2001.
\newblock In \cite[\PP{376}{380}]{firstIJCARone}.

\bibitem[\protect\citeauthoryear{Robinson{\protectedrobinsonindex} and
  Voronkow}{2001}]{HandbookAR}
J.~Alan Robinson{\protectedrobinsonindex} and Andrei Voronkow, editors.
\newblock {\em Handbook of Automated Reasoning}.
\newblock {\elsevier}, 2001.

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

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

\bibitem[\protect\citeauthoryear{Rusinowitch and
  Remy}{1993}]{thirdCTRSninetytwo}
Micha{\"e}l Rusinowitch and Jean-Luc Remy, editors.
\newblock {\em {\thethirdCTRSninetytwo}}, number 656 in Lecture Notes in
  Computer Science, 1993.

\bibitem[\protect\citeauthoryear{Russinoff}{1998}]{russinoff-1998}
David~M. Russinoff.
\newblock A mechanically checked proof of {IEEE} compliance of a
  register-transfer-level specification of the {AMD-K7} floating-point
  multiplication, division, and square root instructions.
\newblock {\em London Mathematical Society Journal of Computation and
  Mathematics}, 1:148--200, 1998.

\bibitem[\protect\citeauthoryear{Saaty}{1965}]{saaty}
T.~L. Saaty, editor.
\newblock {\em Lectures on Modern Mathematics}.
\newblock \wiley, 1965.

\bibitem[\protect\citeauthoryear{Schmidt-Samoa{\protectedsamoaindex}}{2006a}]{%
samoacalculemus}
Tobias Schmidt-Samoa{\protectedsamoaindex}.
\newblock An even closer integration of {\index{linear arithmetic}}linear
  arithmetic into inductive theorem proving.
\newblock {\em {\ENTCSname}}, 151:3--20, 2006.
\newblock \www\url{/p/evencloser},
  \url{http://dx.doi.org/10.1016/j.entcs.2005.11.020}.

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

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

\bibitem[\protect\citeauthoryear{Schoenfield}{1967}]{schoenfield}
Joseph~R. Schoenfield.
\newblock {\em Mathematical Logic}.
\newblock \addisonwesley, 1967.

\bibitem[\protect\citeauthoryear{Scott{\protectedscottindex}}{1993}]{scott-LCF}
Dana~S. Scott{\protectedscottindex}.
\newblock A type-theoretical alternative to {ISWIM}, {CUCH}, {OWHY}.
\newblock {\em \tcsname}, 121:411--440, 1993.
\newblock Annotated version of a manuscript from the year\,1969.
  \url{www.cs.cmu.edu/~kw/scans/scott93tcs.pdf}.

\bibitem[\protect\citeauthoryear{Shankar{\protectedshankarindex}}{1986}]{shank%
ar-1986}
Natarajan Shankar{\protectedshankarindex}.
\newblock {\em Proof-checking Metamathematics}.
\newblock PhD thesis, \unitexasaustin, 1986.
\newblock Thoroughly revised version is \cite{shankar-1994}.

\bibitem[\protect\citeauthoryear{Shankar{\protectedshankarindex}}{1988}]{churc%
h-rosser-bm}
Natarajan Shankar{\protectedshankarindex}.
\newblock A mechanical proof of the {\churchrosser\ theorem}.
\newblock {\em \jacmname}, 35:475--522, 1988.
\newblock Received \May\,1985, \rev\,\Aug\,1987\@. See also \litchapref 6 in
  \cite{shankar-1994}.

\bibitem[\protect\citeauthoryear{Shankar{\protectedshankarindex}}{1994}]{shank%
ar-1994}
Natarajan Shankar{\protectedshankarindex}.
\newblock {\em Metamathematics, Machines, and {\goedel}'s Proof}.
\newblock \cambridgeunipress, 1994.
\newblock Originally published as \cite{shankar-1986}. Paperback reprint\,1997.

\bibitem[\protect\citeauthoryear{Siek{\-}mann{\protect\siekmannindex}}{1986}]{%
eighthCADEeightysix}
J{\"o}rg Siek{\-}mann{\protect\siekmannindex}, editor.
\newblock {\em {\theeighthCADEeightysix}}, number 230 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 1986.

\bibitem[\protect\citeauthoryear{Sridharan}{1989}]{ijcai11}
N.~S. Sridharan, editor.
\newblock {\em {\Proc\ \nth{11} \IJCAIname\ (\IJCAI), Detroit (MI)}}.
  \morgankaufmann, 1989.
\newblock \url{http://ijcai.org/Past%20Proceedings}.

\bibitem[\protect\citeauthoryear{Stansifer}{1984}]{presburger-remarks-translat%
ion}
Ryan Stansifer.
\newblock {\presburgerindex\presburger's Article on Integer Arithmetic: Remarks
  and Translation}.
\newblock Technical Report TR\,84--639, \Dept\ of \CS, Cornell \Univ, Ithaca
  (NY), 1984.
\newblock \url{http://hdl.handle.net/1813/6478}.

\bibitem[\protect\citeauthoryear{Steele}{1990}]{commonlisp}
Guy~L. Steele, {\jr}.
\newblock {\em {\COMMONLISP} --- The Language}.
\newblock \digitalpress, 1990.
\newblock \nth 2\,\edn\ (\nth 1\,\edn\,1984).

\bibitem[\protect\citeauthoryear{Steinbach}{1988}]{SR--88--12}
Joachim Steinbach.
\newblock {\em Term Orderings With Status}.
\newblock {SEKI-Report SR--88--12 (ISSN 1437--4447)}. {SEKI Publications}, FB
  Informatik, Univ. Kaiserslautern, 1988.
\newblock \PPcount{57}, \urlsreightyeighttwelve.

\bibitem[\protect\citeauthoryear{Steinbach}{1995}]{simplificationorderings}
Joachim Steinbach.
\newblock Simplification orderings --- history of results.
\newblock {\em \fundamentainformaticaename}, 24:47--87, 1995.

\bibitem[\protect\citeauthoryear{Stevens}{1988}]{stevens-rational-reconstructi%
on}
Andrew Stevens.
\newblock {\em A Rational Reconstruction of {\boyer} and {\moore}'s Technique
  for Constructing Induction Formulas}.
\newblock 1988.
\newblock \daireport{360}\@. Also in
  \cite[\PP{565}{570}]{eighthECAIeightyeight}.

\bibitem[\protect\citeauthoryear{Stickel}{1990}]{tenthCADEninety}
Mark~E. Stickel, editor.
\newblock {\em {\thetenthCADEninety}}, number 449 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 1990.

\bibitem[\protect\citeauthoryear{Stoyan}{1985}]{gwai9}
Herbert Stoyan, editor.
\newblock {\em {\nth 9 \GWAIname, Dassel (Germany), 1985}}, number 118 in
  Informatik-Fachberichte. \springerverlag, 1985.

\bibitem[\protect\citeauthoryear{Toyama}{1988}]{toyama}
Yoshihito Toyama.
\newblock Commutativity of term rewriting systems.
\newblock 1988.
\newblock In \cite[\PP{393}{407}]{future-generation}. \ Also in
  \cite{toyamadiss}.

\bibitem[\protect\citeauthoryear{Toyama}{1990}]{toyamadiss}
Yoshihito Toyama.
\newblock {\em {Term Rewriting Systems and the \churchrosser\ Property}}.
\newblock PhD thesis, Tohoku \Univ\ / Nippon Telegraph and Telephone
  Corporation, 1990.

\bibitem[\protect\citeauthoryear{Unguru}{1991}]{unguru-one}
Sabetai Unguru.
\newblock Greek mathematics and mathematical induction.
\newblock {\em \physisname}, XXVIII(2):273--289, 1991.

\bibitem[\protect\citeauthoryear{Verma}{2005?}]{simonyi-interview}
Shamit Verma.
\newblock Interview with \simonyiname.
\newblock \WWW\ only: \url{http://www.shamit.org/charles_simonyi.htm}, 2005?

\bibitem[\protect\citeauthoryear{Voicu and Li}{2009}]{voicu-li-di}
R{\u a}zvan Voicu and Mengran Li.
\newblock {\em\DescenteInfinie} proofs in {\COQ}.
\newblock 2009.
\newblock In \cite[\PP{73}{84}]{Coq1}.

\bibitem[\protect\citeauthoryear{Voronkov}{1992}]{thirdLPARninetytwo}
Andrei Voronkov, editor.
\newblock {\em \Proc\ \nth 3 \LPARname\ (\LPAR)}, number 624 in Lecture Notes
  in Artificial Intelligence. \springerverlag, 1992.

\bibitem[\protect\citeauthoryear{Voronkov}{2002}]{eightteenthCADEtwo}
Andrei Voronkov, editor.
\newblock {\em {\theeightteenthCADEtwo}}, number 2392 in Lecture Notes in
  Artificial Intelligence. \springerverlag, 2002.

\bibitem[\protect\citeauthoryear{Walther{\protectedwaltherindex}}{1988}]{walth%
ertermination}
{\mbox{Ch}}ristoph Walther{\protectedwaltherindex}.
\newblock Argument-bounded algorithms as a basis for automated termination
  proofs.
\newblock 1988.
\newblock In \cite[\PP{601}{622}]{ninthCADEeightyeight}.

\bibitem[\protect\citeauthoryear{Walther{\protectedwaltherindex}}{1992}]{walth%
erLPAR92}
{\mbox{Ch}}ristoph Walther{\protectedwaltherindex}.
\newblock Computing induction axioms.
\newblock 1992.
\newblock In \cite[\PP{381}{392}]{thirdLPARninetytwo}.

\bibitem[\protect\citeauthoryear{Walther{\protectedwaltherindex}}{1993}]{walth%
erIJCAI93}
{\mbox{Ch}}ristoph Walther{\protectedwaltherindex}.
\newblock Combining induction axioms by machine.
\newblock 1993.
\newblock In \cite[\PP{95}{101}]{ijcai13}.

\bibitem[\protect\citeauthoryear{Walther{\protectedwaltherindex}}{1994a}]{walt%
herhandbook}
{\mbox{Ch}}ristoph Walther{\protectedwaltherindex}.
\newblock Mathematical induction.
\newblock 1994.
\newblock In \cite[\PP{127}{228}]{handbooklogicailpvol2}.

\bibitem[\protect\citeauthoryear{Walther{\protectedwaltherindex}}{1994b}]{walt%
hertermination2}
{\mbox{Ch}}ristoph Walther{\protectedwaltherindex}.
\newblock On proving termination of algorithms by machine.
\newblock {\em \artificialintelligencename}, 71:101--157, 1994.

\bibitem[\protect\citeauthoryear{Wirsing and Nivat}{1996}]{fifthAMASTninetysix}
Martin Wirsing and Maurice Nivat, editors.
\newblock {\em \Proc\ \nth 5 \Int\ \Conf\ on Algebraic Methodology and Software
  Technology (AMAST), \Muenchen\ (Germany), 1996}, number 1101 in Lecture Notes
  in Computer Science. \springerverlag, 1996.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex} and
  Becker}{1995}]{wirthbecker}
Claus-Peter Wirth{\protectedwirthindex} and Klaus Becker.
\newblock Abstract notions and inference systems for proofs by mathematical
  induction.
\newblock 1995.
\newblock In \cite[\PP{353}{373}]{fourthCTRSninetyfour}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex} and
  Gram{\-}li{\protectedgramlichindex}ch}{1994a}]{wgjsc}
Claus-Peter Wirth{\protectedwirthindex} and Bernhard
  Gram{\-}li{\protectedgramlichindex}ch.
\newblock A constructor-based approach to positive/negative-conditional
  equational specifications.
\newblock {\em {\jscname}}, 17:51--90, 1994.
\newblock \url{http://dx.doi.org/10.1006/jsco.1994.1004}, \www\url{/p/jsc94}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex} and
  Gram{\-}li{\protectedgramlichindex}ch}{1994b}]{wgcade}
Claus-Peter Wirth{\protectedwirthindex} and Bernhard
  Gram{\-}li{\protectedgramlichindex}ch.
\newblock On notions of inductive validity for first-order equational clauses.
\newblock 1994.
\newblock In \cite[\PP{162}{176}]{twelvethCADEninetyfour}, \www\url{/p/cade94}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex} and
  K{\"u}hler{\protectedkuehlerindex}}{1995}]{SR--95--15}
Claus-Peter Wirth{\protectedwirthindex} and Ulrich
  K{\"u}hler{\protectedkuehlerindex}.
\newblock {\em Inductive Theorem Proving in Theories Specified by \PNC\
  Equations}.
\newblock {SEKI-Report SR--95--15 (ISSN 1437--4447)}. {SEKI Publications},
  Univ.\ Kaiserslautern, 1995.
\newblock \PPcount{iv+126}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex} \bgroup \em et
  al.\egroup }{1993}]{wgkp}
Claus-Peter Wirth{\protectedwirthindex}, Bernhard
  Gram{\-}li{\protectedgramlichindex}ch, Ulrich
  K{\"u}hler{\protectedkuehlerindex}, and Horst Prote.
\newblock {\em Constructor-Based Inductive Validity in
  Positive/Negative-Conditional Equational Specifications}.
\newblock {SEKI-Report SR--93--05~(SFB) (ISSN 1437--4447)}. {SEKI
  Publications}, \FBinfshort, \uniKLshort, 1993.
\newblock \PPcount{iv+58}, \urlsrninetythreedashzerofive. \Rev\,\extd\,\edn\ of
  \nth 1\,part is \cite{wgjsc}, \rev\,\edn\ of \nth 2\,part is \cite{wgcade}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex} \bgroup \em et
  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}{1971}]{wirth-pascal}
Niklaus Wirth.
\newblock The programming language {\Pascal}.
\newblock {\em Acta Informatica}, 1:35--63, 1971.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{1991}]{wirth-mas%
ter}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock Inductive theorem proving in theories specified by
  posi\-tive/ne\-ga\-tive-condi\-tional equations.
\newblock \Diplomarbeit, \FBinfshort, \uniKLshort, 1991.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{1997}]{wirthdiss}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock {\em Positive/Negative-Conditional Equations: A Constructor-Based
  Framework for Specification and Inductive Theorem Proving}, volume~31 of {\em
  {Schriftenreihe Forschungsergebnisse zur Informatik}}.
\newblock {Verlag Dr.\ Kova\v c, Hamburg}, 1997.
\newblock \PhDthesis, \uniKLshort, {ISBN 386064551X}, {\www\url{/p/diss}}.

\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}}{2005a}]{zombie}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock History and future of implicit and inductionless induction: Beware
  the old jade and the zombie!
\newblock 2005.
\newblock In \cite[\PP{192}{203}]{siekmann-60}, {\www\url{/p/zombie}}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2005b}]{wirthcon%
fluence}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock {\em Syntactic Confluence Criteria for Positive/Negative-Conditional
  Term Rewriting Systems}.
\newblock {SEKI-Report SR--95--09 (ISSN 1437--4447)}. {SEKI Publications},
  Univ.\ Kaiserslautern, 2005.
\newblock \Rev\,\edn\ \Oct\,2005 (\nth 1\,\edn\,1995), \PPcount{ii+188},
  \url{http://arxiv.org/abs/0902.3614}.

\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}}{2009}]{wirth-jsc}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock Shallow confluence of conditional term rewriting systems.
\newblock {\em {\jscname}}, 44:69--98, 2009.
\newblock \url{http://dx.doi.org/10.1016/j.jsc.2008.05.005}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2010a}]{swp20060%
1}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock {\em Progress in Computer-Assisted Inductive Theorem Proving by
  Human-Orientedness and Descente Infinie?}
\newblock {SEKI-Working-Paper SWP--2006--01 (ISSN 1860--5931)}. {SEKI
  Publications}, Saarland Univ., 2010.
\newblock \Rev\,\edn\,Dec\,2010 (\nth 1\,\edn\,2006), \PPcount{ii+36},
  \url{http://arxiv.org/abs/0902.3294}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2010b}]{fermatsp%
roof}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock {\em A Self-Contained and Easily Accessible Discussion of the Method
  of Descente Infinie and\/ {\fermat}'s Only Explicitly Known Proof by {\it
  Descente Infinie}}.
\newblock {SEKI-Working-Paper SWP--2006--02 (ISSN 1860--5931)}. {SEKI
  Publications}, {DFKI Bremen GmbH, Safe and Secure Cognitive Systems,
  Cartesium, Enrique Schmidt Str.\,5, D--28359 Bremen, Germany}, 2010.
\newblock \Rev\,\ed\,\Dec\,2010, \PPcount{ii+36},
  \url{http://arxiv.org/abs/0902.3623}.

\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}]{boyer-mo%
ore-2012}
Claus-Peter Wirth{\protectedwirthindex}.
\newblock {Unpublished Interview of \boyername\ and \moorename\ at \boyer's
  place in Austin (TX) on Thursday, \Oct\,7}.
\newblock 2012.

\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}}.

\bibitem[\protect\citeauthoryear{Wolff}{1728}]{wolff-rationalis}
Christian Wolff.
\newblock {\em Philosophia rationalis sive Logica, methodo scientifica
  pertractata et ad usum scientiarium atque vitae aptata}.
\newblock Rengerische Buchhandlung, \FFM\ \& \Leipzig, 1728.
\newblock \nth 1\,\edn.

\bibitem[\protect\citeauthoryear{Wolff}{1740}]{wolff-rationalis-1740}
Christian Wolff.
\newblock {\em Philosophia rationalis sive Logica, methodo scientifica
  pertractata et ad usum scientiarium atque vitae aptata}.
\newblock Rengerische Buchhandlung, \FFM\ \& \Leipzig, 1740.
\newblock \nth 3\,\extd\,\edn\ of \cite{wolff-rationalis}\@. \ Facsimile
  reprint by \olmsverlag, 1983, with a French introduction by {\namefont\jean\
  \'Ecole}.

\bibitem[\protect\citeauthoryear{Yeh and
  Ramamoorthy}{1976}]{secondICSEseventysix}
Raymond~T. Yeh and C.~V. Ramamoorthy, editors.
\newblock {\em \Proc\ \nth 2 \Int\ \Conf\ on Software Engineering, San
  Francisco (CA), \Oct\,13--15, 1976}. \ieeeCSpress, 1976.
\newblock \url{http://dl.acm.org/citation.cfm?id=800253}.

\bibitem[\protect\citeauthoryear{Young}{1989}]{young-1989}
William~D. Young.
\newblock A mechanically verified code generator.
\newblock {\em \jarname}, 5:493--518, 1989.

\bibitem[\protect\citeauthoryear{Zhang \bgroup \em et al.\egroup
  }{1988}]{ZKK88}
Han{\-}tao Zhang, Deepak Kapur, and Mukkai~S. Krishnamoorthy.
\newblock A mechanizable induction principle for equational specifications.
\newblock 1988.
\newblock In \cite[\PP{162}{181}]{ninthCADEeightyeight}.

\bibitem[\protect\citeauthoryear{Zygmunt}{1991}]{presburger-life}
Jan Zygmunt.
\newblock \presburgername: Life and work.
\newblock {\em History and Philosophy of Logic}, 12:211--223, 1991.

\end{thebibliography}