\begin{thebibliography}{}

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Anon}{2005}]{aamp7g-2005}
Anon, 2005.
\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}.

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

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Barendregt}{1981}]{lambda-calculus-1st}
Hen(dri)k~P. Barendregt, 1981.
\newblock {\em The Lambda Calculus --- Its Syntax and Semantics}.
\newblock Number 103 in Studies in Logic and the Foundations of Mathematics.
  \northholland.
\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, 2012.
\newblock {\em The Lambda Calculus --- Its Syntax and Semantics}.
\newblock Number~40 in Studies in Logic. \collegepublications.
\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}, 2001a.
\newblock {\fermatname\ (1601?--1665) --- His life beside mathematics}.
\newblock {\em European Mathematical Society Newsletter},
  43\,(\Dec\,2001):12--16.
\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}, 2001b.
\newblock {Da\es\ Leben \fermat\es}.
\newblock {\em \dmvmitteilungenname}, 3/2001:12--26.
\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}, 2001c.
\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.
\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}, 2007.
\newblock {Neue\es\ zu \fermat\es\ Geburt\esi datum}.
\newblock {\em \dmvmitteilungenname}, 15:12--14.
\newblock \bibcritemptynote{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{\protectedbasinindex} \bgroup\&\ \egroup
  Walsh}{1996}]{rippling-calculus}
David Basin{\protectedbasinindex} and Toby Walsh, 1996.
\newblock A calculus for and termination of rippling.
\newblock {\em \jarname}, 16:147--180.

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

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

\bibitem[\protect\citeauthoryear{Bell \bgroup\&\ \egroup
  Thayer}{1976}]{waterfall}
Thomas~E. Bell and T.~A. Thayer, 1976.
\newblock Software requirements: Are they really a problem?
\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\&al.\egroup }{2008}]{C26}
{\mbox{Ch}}ristoph Benz{\-}m{\ue}ller{\protectedbenzmuellerindex}, Frank
  Theiss, Lawrence~C. Paulson, and Arnaud Fietz{\-}ke, 2008.
\newblock {\LEOII} --- a cooperative automatic theorem prover for higher-order
  logic.
\newblock In \cite[\PP{162}{170}]{fourthIJCAReight}.

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

\bibitem[\protect\citeauthoryear{Bernays{\protectedbernaysindex}}{1928}]{grund%
lagenvortrag-zusatz}
Paul Bernays{\protectedbernaysindex}, 1928.
\newblock {Zusatz zu \hilbert\es\ Vortrag \glqq Die
  \grundlagendermathematiknoindex\grqq}.
\newblock {\em {\AbhandlungenmathHamburgname}}, 6:89--92.
\newblock {English} translation {\em On the Consistency of Arithmetic} in
  \cite[\PP{485}{489}]{heijenoort-source-book}.

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Bouajjani \bgroup\&\ \egroup
  Maler}{2009}]{twentyfirstCAVnine}
Ahmed Bouajjani and Oded Maler, editors, 2009.
\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}.

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

\bibitem[\protect\citeauthoryear{Bourbaki{\protectedbourbakiindex}}{1939}]{bou%
rbaki-set-theory-results-1st-edn}
Nicola{\es} Bourbaki{\protectedbourbakiindex}, 1939.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 846 in \hermannparisseries. \hermannparis.
\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}, 1951.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 846-1141 in \hermannparisseries. \hermannparis.
\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}, 1954.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,I\,\&\,II}}.
\newblock Number 1212 in \hermannparisseries. \hermannparis.
\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}, 1956.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,III}}.
\newblock Number 1243 in \hermannparisseries. \hermannparis.
\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}, 1958a.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,IV}}.
\newblock Number 1258 in \hermannparisseries. \hermannparis.
\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}, 1958b.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 1141 in \hermannparisseries. \hermannparis.
\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}, 1960.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,I\,\&\,II}}.
\newblock Number 1212 in \hermannparisseries. \hermannparis.
\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}, 1964.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 1141 in \hermannparisseries. \hermannparis.
\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}, 1966a.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,IV}}.
\newblock Number 1258 in \hermannparisseries. \hermannparis.
\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}, 1966b.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitres\,I\,\&\,II}}.
\newblock Number 1212 in \hermannparisseries. \hermannparis.
\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}, 1967.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Chapitre\,III}}.
\newblock Number 1243 in \hermannparisseries. \hermannparis.
\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}, 1968a.
\newblock {\em Elements of Mathematics --- Theory of Sets}.
\newblock \hermannparisseries. \hermannparis, jointly published with
  \mbox{AdiWes} International Series in Mathematics, \addisonwesley.
\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}, 1968b.
\newblock {\em {\'El\'ements des Math\'ematique --- Livre\,1: Th\'eorie des
  Ensembles. Fascicule De R\'esultats}}.
\newblock Number 1141 in \hermannparisseries. \hermannparis.
\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}}{1971}]{Boy71}
Robert~S. Boyer{\protect\boyerindex}, 1971.
\newblock {\em Locking: a restriction of resolution}.
\newblock PhD thesis, \unitexasaustin.

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} \bgroup\&\ \egroup
  Moore{\protect\mooreindex}}{1977}]{boyer-moore-1977}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex},
  1977.
\newblock A lemma driven automatic theorem prover for recursive function
  theory.
\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} \bgroup\&\ \egroup
  Moore{\protect\mooreindex}}{1979}]{bm}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex},
  1979.
\newblock {\em A Computational Logic}.
\newblock \academicpress.
\newblock \url{http://www.cs.utexas.edu/users/boyer/acl.text}.

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} \bgroup\&\ \egroup
  Moore{\protect\mooreindex}}{1987}]{bmeval-1987}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex},
  1987.
\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.
\newblock Printed \Jan\,1987\@. Also published as
  \makeaciteoftwo{bmeval-1988}{bmeval-1989}.

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

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

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

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} \bgroup\&\ \egroup
  Moore{\protect\mooreindex}}{1989}]{bmeval-1989}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex},
  1989.
\newblock The addition of bounded quantification and partial functions to a
  computational logic and its theorem prover.
\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} \bgroup\&\ \egroup
  Moore{\protect\mooreindex}}{1990}]{BM90}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex},
  1990.
\newblock A theorem prover for a computational logic.
\newblock In \cite[\PP{1}{15}]{tenthCADEninety}.

\bibitem[\protect\citeauthoryear{Boyer{\protect\boyerindex} \bgroup\&\ \egroup
  Moore{\protect\mooreindex}}{1998}]{boyermooresecondedition}
Robert~S. Boyer{\protect\boyerindex} and J~Strother Moore{\protect\mooreindex},
  1998.
\newblock {\em A Computational Logic Handbook}.
\newblock International Series in Formal Methods. \academicpress.
\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} \bgroup\&al.\egroup
  }{1976}]{boyer-moore-shostak}
Robert~S. Boyer{\protect\boyerindex}, J~Strother Moore{\protect\mooreindex},
  and Robert~E. Shostak, 1976.
\newblock Primitive recursive program transformations.
\newblock In \cite[\PP{171}{174}]{thirdPOPLseventysix}.
  \url{http://doi.acm.org/10.1145/800168.811550}.

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Brotherston \bgroup\&\ \egroup
  Simpson}{2011}]{brotherston-cut-elimination}
James Brotherston and Alex Simpson, 2011.
\newblock Sequent calculi for induction and infinite descent.
\newblock {\em {\jlcname}}, 21:1177--1216.
\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{Brown}{2012}]{satallax}
Chad~E. Brown, 2012.
\newblock {\SATALLAX}: An automatic higher-order prover.
\newblock In \cite[\PP{111}{117}]{sixthIJCARtwelve}.

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

\bibitem[\protect\citeauthoryear{Buch \bgroup\&\ \egroup
  Hillenbrand{\protectedhillenbrandindex}}{1996}]{waldmeister}
Armin Buch and Thomas Hillenbrand{\protectedhillenbrandindex}, 1996.
\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.
\newblock \url{agent.informatik.uni-kl.de/seki/1996/Buch.SR-96-01.ps.gz}.

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

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

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Bussotti}{2006}]{From-Fermat-to-Gauss}
Paolo Bussotti, 2006.
\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.

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Constable \bgroup\&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, 1985.
\newblock {\em Implementing Mathematics with {the\/ \NUPRL} Proof Development
  System}.
\newblock \PrenticeHall.
\newblock \url{http://www.nuprl.org/book}.

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

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

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

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

\bibitem[\protect\citeauthoryear{Dedekind{\protect\dedekindindex}}{1888}]{dede%
kind-1888}
Richard Dedekind{\protect\dedekindindex}, 1888.
\newblock {\em {\dedekindeightyeighttitle}}.
\newblock \verlagviewegundsohn.
\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}, 1930--32.
\newblock {\em {Gesammelte mathematische Werke}}.
\newblock \verlagviewegundsohn.
\newblock \Ed\ by \frickename, \noethername, and {\namefont \Oe ystein Ore}.

\bibitem[\protect\citeauthoryear{Dedekind{\protect\dedekindindex}}{1969}]{dede%
kind-1969}
Richard Dedekind{\protect\dedekindindex}, 1969.
\newblock {\em {\dedekindeightyeighttitle\ Stetigkeit und irrationale Zahlen}}.
\newblock \verlagviewegundsohn.

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Dixon \bgroup\&\ \egroup
  Fleuriot}{2003}]{DF03-CADE-19}
Lucas Dixon and Jacques Fleuriot, 2003.
\newblock {\ISAPLANNER}: A prototype proof planner in {\ISABELLE}.
\newblock In \cite[\PP{279}{283}]{nineteenthCADEthree}.

\bibitem[\protect\citeauthoryear{Eisenreich \bgroup\&\ \egroup
  Sube}{1982}]{fachwoerterbuchmathematik}
G{\"u}nther Eisenreich and Ralf Sube, 1982.
\newblock {\em {W\oe rterbuch der Mathematik: Englisch--Deutsch--Franz\oe
  sisch--Russisch}}.
\newblock VEB Verlag Technik, \Berlin.
\newblock Two volumes, also under license to Verlag Harri Deutsch, Thun
  (Switzerland), 1982. \ Reprinted in one volume as\/ {\em Langenscheidt\es\
  Fach\-w\oe rterbuch Mathematik}\/ by Langenscheidt, \Berlin, 1996.

\bibitem[\protect\citeauthoryear{Euclid{\protect\euclidindex}}{\ca\,300\,\BC}]%
{elements}
\ignorespaces Euclid{\protect\euclidindex} of~Alexandria, \ca\,300\,\BC.
\newblock {\em Elements}.
\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, 1891\ff.
\newblock {\em \OE uvres de \fermat}.
\newblock {\gauthiervillars}.
\newblock \Ed\ by {\namefont Paul Tannery}, {\namefont Charles Henry}.

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

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

\bibitem[\protect\citeauthoryear{FOCS}{1980}]{focs21}
FOCS, 1980.
\newblock {\em {\Proc\ \nth{21} \FOCSname, Syracuse, 1980}}. \ieeepress.
\newblock \url{http://ieee-focs.org/}.

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

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

\bibitem[\protect\citeauthoryear{Fribourg}{1986}]{inductionlesshistb}
Laurent Fribourg, 1986.
\newblock A strong restriction of the inductive completion procedure.
\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}, 1822.
\newblock {\em {Die mathematische Naturphilosophie nach philosophischer Methode
  bearbeitet -- Ein Versuch}}.
\newblock Christian Friedrich Winter, \Heidelberg.
\newblock Facsimlie in \cite[\Vol\,13 (1979)]{fries-saemtliche}.

\bibitem[\protect\citeauthoryear{Fries{\protectedfriesindex}}{1967\ff}]{fries-%
saemtliche}
Jakob~Friedrich Fries{\protectedfriesindex}, 1967\ff.
\newblock {\em {S\ae mtliche Schriften}}.
\newblock Scientia Verlag (Kloof Booksellers \& Scientia Verlag), Aalen
  (Germany).
\newblock 33~volumes, \ed\ by {\sc Gert K\oe nig} and {\sc Lutz Geldsetzer}.

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Geser}{1995}]{geseraxiomofchoice}
Alfons Geser, 1995.
\newblock A principle of non-wellfounded induction.
\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, 1996.
\newblock An improved general path order.
\newblock {\em \aaeccname}, 7:469--511.

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

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

\bibitem[\protect\citeauthoryear{G{\oe
  de{\protectedgoedelindex}l}}{1931}]{goedel}
Kurt G{\oe de{\protectedgoedelindex}l}, 1931.
\newblock {\Ue ber formal unentscheidbare S\ae tze der \PM\ und verwandter
  Sy\esi teme I}.
\newblock {\em {\monatsheftempname}}, 38:173--198.
\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}, 1962.
\newblock {\em On formally undecidable propositions of {\PM} and related
  systems}.
\newblock Basic Books, \NewYork.
\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}, 1986ff.
\newblock {\em Collected Works}.
\newblock {\oxfordunipress}.
\newblock \Ed\ by \fefermanname, \dawsonname\protect\dawsonindex,
  \goldfarbname, \heijenoortname, \kleenename, \parsonsname, \siegname,
  \etalabbrev.

\bibitem[\protect\citeauthoryear{Goguen}{1980}]{gogueninductionlessinduction}
Joseph Goguen, 1980.
\newblock How to prove algebraic inductive hypotheses without induction.
\newblock In \cite[\PP{356}{373}]{fifthCADEeighty}.

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

\bibitem[\protect\citeauthoryear{Goodstein{\protectedgoodsteinindex}}{1945}]{G%
oodstein_1945}
R.~L. Goodstein{\protectedgoodsteinindex}, 1945.
\newblock Function theory in an axiom-free equation calculus.
\newblock {\em Proceedings of the London Mathematical Society, Ser.\,2},
  48:401--434.

\bibitem[\protect\citeauthoryear{Goodstein{\protectedgoodsteinindex}}{1957}]{G%
oodstein_Number_Theory}
R.~L. Goodstein{\protectedgoodsteinindex}, 1957.
\newblock {\em Recursive number theory --- A development of recursive
  arithmetic in a logic-free equation calculus}.
\newblock Studies in logic and the foundations of mathematics. \northholland,
  \Amsterdam.
\newblock \nth 2\,\edn\,1965.

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

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

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

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

\bibitem[\protect\citeauthoryear{Gram{\-}li{\protectedgramlichindex}ch}{1996}]%
{gramlich-phdthesis96}
Bernhard Gram{\-}li{\protectedgramlichindex}ch, 1996.
\newblock {\em Termination and Confluence Properties of Structured Rewrite
  Systems}.
\newblock PhD thesis, \FBinfshort, \uniKLshort.
\newblock \url{www.logic.at/staff/gramlich/papers/thesis96.pdf}.
  \PPcount{x+217}.

\bibitem[\protect\citeauthoryear{Gram{\-}li{\protectedgramlichindex}ch
  \bgroup\&\ \egroup Lindner}{1991}]{unicom}
Bernhard Gram{\-}li{\protectedgramlichindex}ch and Wolfgang Lindner, 1991.
\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.
\newblock
  \url{http://agent.informatik.uni-kl.de/seki/1991/Lindner.SR-91-17.ps.gz}.

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

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

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

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

\bibitem[\protect\citeauthoryear{Herbelin}{2009}]{Coq1}
Hugo Herbelin, editor, 2009.
\newblock {\em The {\nth 1} {\COQ} Workshop}. {\Inst\ f\ue r Informatik, \Tech\
  \Univ\ \Muenchen}.
\newblock TUM-I0919,
  \url{http://www.lix.polytechnique.fr/coq/files/coq-workshop-TUM-I0919.pdf}.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Hillenbrand{\protectedhillenbrandindex}
  \bgroup\&\ \egroup L{\oe}chner{\protectedloechnerindex}}{2002}]{HL02}
Thomas Hillenbrand{\protectedhillenbrandindex} and Bernd
  L{\oe}chner{\protectedloechnerindex}, 2002.
\newblock The next {\WALDMEISTER} loop.
\newblock In \cite[\PP{486}{500}]{eightteenthCADEtwo}.
  \url{http://www.waldmeister.org}.

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

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

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Hutter{\protectedhutterindex}}{1994}]{hutter-%
cade-nancy}
Dieter Hutter{\protectedhutterindex}, 1994.
\newblock Synthesis of induction orderings for existence proofs.
\newblock In \cite[\PP{29}{41}]{twelvethCADEninetyfour}.

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

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

\bibitem[\protect\citeauthoryear{Hutter{\protectedhutterindex} \bgroup\&\
  \egroup Stephan}{2005}]{siekmann-60}
Dieter Hutter{\protectedhutterindex} and Werner Stephan, editors, 2005.
\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}.

\bibitem[\protect\citeauthoryear{IEEE WESTON}{1970}]{ieeeweston70}
IEEE WESTON, 1970.
\newblock {\em \Proc\ \ieee\ WESCON, \Aug\,1970}. \ieeepress, originally
  published by TRW software series, TRW--SS--70--01.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{K{\"u}hler{\protectedkuehlerindex}}{1991}]{ku%
ehler-master}
Ulrich K{\"u}hler{\protectedkuehlerindex}, 1991.
\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.

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

\bibitem[\protect\citeauthoryear{K{\"u}hler{\protectedkuehlerindex} \bgroup\&\
  \egroup Wirth{\protectedwirthindex}}{1996}]{kwspec}
Ulrich K{\"u}hler{\protectedkuehlerindex} and Claus-Peter
  Wirth{\protectedwirthindex}, 1996.
\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.
\newblock \PPcount{24}, \www\url{/p/rta97}. Short version is \cite{kwspec2}.

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

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

\bibitem[\protect\citeauthoryear{Lankford}{1980}]{inductionlessinduction1}
Dalla{\es}~S. Lankford, 1980.
\newblock Some remarks on inductionless induction.
\newblock Memo MTP-11, \Math\ \Dept, Louisiana \Tech\ \Univ, Ruston (LA).

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

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

\bibitem[\protect\citeauthoryear{Leech}{1970}]{leech-1970}
John Leech, editor, 1970.
\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.
\newblock With a foreword by {\namefont J. Howlett}.

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

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

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Melis \bgroup\&al.\egroup
  }{2008}]{proof_planning_with_multiple_strategies}
Erica Melis, Andreas Meier, and J{\"o}rg Siek{\-}mann{\protect\siekmannindex},
  2008.
\newblock Proof planning with multiple strategies.
\newblock {\em \artificialintelligencename}, 172:656--684.
\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}}{1975}]{meltz%
er-1975}
Bernard Meltzer{\protectedmeltzerindex}, 1975.
\newblock {Department of A.I. -- Univ.\ of \EB}.
\newblock {\em ACM SIGART Bulletin}, 50:5.

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

\bibitem[\protect\citeauthoryear{Michie{\protectedmichieindex}}{1968}]{machine%
-intelligence-3}
Donald Michie{\protectedmichieindex}, editor, 1968.
\newblock {\em {Proceedings of the \nth 3\,Annual Machine Intelligence Workshop
  (Machine Intelligence\,3), \EB, 1967}}. \uniEBshort\ Press.
\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, 1972.
\newblock Logic for computable functions --- description of a machine
  interpretation.
\newblock Technical Report Memo\,AIM--169, STAN--CS--72--288, \Dept\ \CS,
  Stanford University.
\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}}{1973}]{moore-1973}
J~Strother Moore{\protect\mooreindex}, 1973.
\newblock {\em Computational Logic: Structure Sharing and Proof of Program
  Properties}.
\newblock PhD thesis, \Dept\ \AI, \uniEBshort.
\newblock \url{http://hdl.handle.net/1842/2245}.

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex}}{1975a}]{moore-197%
5}
J~Strother Moore{\protect\mooreindex}, 1975a.
\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).
\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}, 1975b.
\newblock Introducing iteration into the {\protect\PURELISPTP}.
\newblock {\em \ieeetranssename}, 1:328--338.
\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}, 1979.
\newblock A mechanical proof of the termination of {\takeuti's} function.
\newblock {\em Information Processing Letters}, 9:176--181.
\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}, 1981.
\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).

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

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

\bibitem[\protect\citeauthoryear{Moore{\protect\mooreindex} \bgroup\&al.\egroup
  }{1998}]{moore-lynch-kaufmann-1998}
J~Strother Moore{\protect\mooreindex}, Thomas Lynch, and Matt
  Kaufmann{\protectedkaufmannindex}, 1998.
\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.

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

\bibitem[\protect\citeauthoryear{Musser}{1980}]{musserinductionlessinduction}
David~R. Musser, 1980.
\newblock On proving inductive properties of abstract data types.
\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, 1973.
\newblock {\em {\Proc\ \nth 3 \IJCAIname\ (\IJCAI), \StanfordCA}}. Stanford
  Research Institute, Publications \Dept, \StanfordCA.
\newblock
  \url{http://ijcai.org/Past%20Proceedings/IJCAI-73/CONTENT/content.htm}.

\bibitem[\protect\citeauthoryear{Odifreddi}{1990}]{odifreddi}
Piergiorgio Odifreddi, editor, 1990.
\newblock {\em Logic and Computer Science}.
\newblock \academicpress.

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

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

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

\bibitem[\protect\citeauthoryear{Paulson}{1990}]{isabellesevenhundred}
Lawrence~C. Paulson, 1990.
\newblock {\ISABELLE}: The next 700 theorem provers.
\newblock In \cite[\PP{361}{386}]{odifreddi}.

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

\bibitem[\protect\citeauthoryear{Peano{\protect\peanoindex}}{1889}]{peanonovam%
ethodo}
Guiseppe Peano{\protect\peanoindex}, 1889.
\newblock {\em {\peanonovamethodotitle}}.
\newblock Fratelli Bocca, \Torino.
\newblock Title page actually says: Ioseph Peano, Fratres Bocca, Augustae
  Taurinorum.

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

\bibitem[\protect\citeauthoryear{Pieri{\protect\pieriindex}}{1908}]{pieri}
Mario Pieri{\protect\pieriindex}, 1908.
\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.
\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\&al.\egroup
  }{2000}]{honorrobinmilner}
Gordon~D. Plotkin, Colin Stirling, and Mads Tofte, editors, 2000.
\newblock {\em Proof, Language, and Interaction, Essays in Honour of
  {\milnername}}.
\newblock \mitpress.

\bibitem[\protect\citeauthoryear{Presburger{\protect\presburgerindex}}{1930}]{%
presburger}
Moj{\zwithdot}esz Presburger{\protect\presburgerindex}, 1930.
\newblock {\presburgertitle}.
\newblock In {\em Sprawozdanie z I Kongresu metematyk\'ow kraj\'ow s\l
  owianskich, Warszawa 1929 (\presburgerproceedings, , Varsovie 1929)}, pages
  92--101+395.
\newblock Remarks and {E}nglish translation in
  \cite{presburger-remarks-translation}.

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Royce}{1970}]{waterfallfirst}
Winsten~W. Royce, 1970.
\newblock Managing the development of large software systems.
\newblock In \cite[\PP 1 9]{ieeeweston70}.

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

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

\bibitem[\protect\citeauthoryear{Russinoff}{1998}]{russinoff-1998}
David~M. Russinoff, 1998.
\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.

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

\bibitem[\protect\citeauthoryear{Schmidt-Samoa{\protectedsamoaindex}}{2006a}]{%
samoacalculemus}
Tobias Schmidt-Samoa{\protectedsamoaindex}, 2006a.
\newblock An even closer integration of {\index{linear arithmetic}}linear
  arithmetic into inductive theorem proving.
\newblock {\em {\ENTCSname}}, 151:3--20.
\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}, 2006b.
\newblock {\em Flexible Heuristic Control for Combining Automation and
  User-Interaction in Inductive Theorem Proving}.
\newblock PhD thesis, \uniKLshort.
\newblock \www\url{/p/samoadiss}.

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

\bibitem[\protect\citeauthoryear{Scott{\protectedscottindex}}{1993}]{scott-LCF}
Dana~S. Scott{\protectedscottindex}, 1993.
\newblock A type-theoretical alternative to {ISWIM}, {CUCH}, {OWHY}.
\newblock {\em \tcsname}, 121:411--440.
\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}, 1986.
\newblock {\em Proof-checking Metamathematics}.
\newblock PhD thesis, \unitexasaustin.
\newblock Thoroughly \rev\ version is \cite{shankar-1994}.

\bibitem[\protect\citeauthoryear{Shankar{\protectedshankarindex}}{1988}]{churc%
h-rosser-bm}
Natarajan Shankar{\protectedshankarindex}, 1988.
\newblock A mechanical proof of the {\churchrosser\ theorem}.
\newblock {\em \jacmname}, 35:475--522.
\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}, 1994.
\newblock {\em Metamathematics, Machines, and {\goedel}'s Proof}.
\newblock \cambridgeunipress.
\newblock Originally published as \cite{shankar-1986}. Paperback reprint\,1997.

\bibitem[\protect\citeauthoryear{Shepherdson}{1969}]{course-of-values-inductio%
n}
J.~C. Shepherdson, 1969.
\newblock Weak and strong induction.
\newblock {\em {\americanmathematicalmonthlyname}}, 76:989--1004.

\bibitem[\protect\citeauthoryear{Shoenfield{\protectedshoenfieldindex}}{1967}]%
{Shoenfield67}
Joseph~R. Shoenfield{\protectedshoenfieldindex}, 1967.
\newblock {\em Mathematical Logic}.
\newblock \addisonwesley.
\newblock \nth 1\,\edn\,1967; \nth 2\,\edn\,1973; \nth 3\,\edn\,2001, facsimile
  of \nth 2\,\edn, A K Peters, Natick (MA), copyright 1967 by the Association
  for Symbolic Logic.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\bibitem[\protect\citeauthoryear{Wirsing \bgroup\&\ \egroup
  Nivat}{1996}]{fifthAMASTninetysix}
Martin Wirsing and Maurice Nivat, editors, 1996.
\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}.

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

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{1997}]{wirthdiss}
Claus-Peter Wirth{\protectedwirthindex}, 1997.
\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}.
\newblock \PhDthesis, \uniKLshort, {ISBN 386064551X}, {\www\url{/p/diss}}.

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

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

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2005b}]{wirthcon%
fluence}
Claus-Peter Wirth{\protectedwirthindex}, 2005b.
\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.
\newblock \Rev\,\edn\ \Oct\,2005 (\nth 1\,\edn\,1995), \PPcount{ii+188},
  \url{http://arxiv.org/abs/0902.3614}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2009}]{wirth-jsc}
Claus-Peter Wirth{\protectedwirthindex}, 2009.
\newblock Shallow confluence of conditional term rewriting systems.
\newblock {\em {\jscname}}, 44:69--98.
\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}, 2010a.
\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.
\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}, 2010b.
\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}.
\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}, 2012a.
\newblock {\herbrandsfundamentaltheorem} in the eyes of {\heijenoortname}.
\newblock {\em {\logicauniversalisname}}, 6:485--520.
\newblock Received \Jan\,12, 2012. Published online \Jun\,22, 2012,
  \url{http://dx.doi.org/10.1007/s11787-012-0056-7}.

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

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2012c}]{wirth-ma%
nifesto-ljigpl}
Claus-Peter Wirth{\protectedwirthindex}, 2012c.
\newblock Human-oriented inductive theorem proving by descente infinie --- {a
  \nolinebreak manifesto}.
\newblock {\em {\ljigplname}}, 20:1046--1063.
\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}, 2012d.
\newblock {Unpublished Interview of \boyername\ and \moorename\ at \boyer's
  place in Austin (TX) on Thursday, \Oct\,7}.

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}}{2015}]{SR--2011-%
-01}
Claus-Peter Wirth{\protectedwirthindex}, 2015.
\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}.
\newblock \Rev\,\edn\ \Jun\,2015 (\nth 1\,\edn\,2011), \PPcount{ii+82},
  {\url{http://arxiv.org/abs/1104.2444}}.

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

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

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

\bibitem[\protect\citeauthoryear{Wirth{\protectedwirthindex}
  \bgroup\&al.\egroup }{1993}]{wgkp}
Claus-Peter Wirth{\protectedwirthindex}, Bernhard
  Gram{\-}li{\protectedgramlichindex}ch, Ulrich
  K{\"u}hler{\protectedkuehlerindex}, and Horst Prote, 1993.
\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.
\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\&\ \egroup
  K{\"u}hler{\protectedkuehlerindex}}{1995}]{SR--95--15}
Claus-Peter Wirth{\protectedwirthindex} and Ulrich
  K{\"u}hler{\protectedkuehlerindex}, 1995.
\newblock {\em Inductive Theorem Proving in Theories Specified by \PNC\
  Equations}.
\newblock {SEKI-Report SR--95--15 (ISSN 1437--4447)}. {SEKI Publications},
  Univ.\ Kaiserslautern.
\newblock \PPcount{iv+126}.

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

\bibitem[\protect\citeauthoryear{Wirth}{1971}]{wirth-pascal}
Niklaus Wirth, 1971.
\newblock The programming language {\Pascal}.
\newblock {\em Acta Informatica}, 1:35--63.

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

\bibitem[\protect\citeauthoryear{Wolff}{1740}]{wolff-rationalis-1740}
Christian Wolff, 1740.
\newblock {\em Philosophia rationalis sive Logica, methodo scientifica
  pertractata et ad usum scientiarium atque vitae aptata}.
\newblock Rengerische Buchhandlung, \FFM\ \& \Leipzig.
\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 \bgroup\&\ \egroup
  Ramamoorthy}{1976}]{secondICSEseventysix}
Raymond~T. Yeh and C.~V. Ramamoorthy, editors, 1976.
\newblock {\em \Proc\ \nth 2 \Int\ \Conf\ on Software Engineering, San
  Francisco (CA), \Oct\,13--15, 1976}. \ieeeCSpress.
\newblock \url{http://dl.acm.org/citation.cfm?id=800253}.

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

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

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

\end{thebibliography}