\relax 
\bibstyle{cpsnamedwithapalikesorting}
\citation{vampire01}
\citation{chaff}
\citation{waldmeister}
\citation{HL02}
\citation{C26}
\citation{satallax}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces The {\sc  Boyer}--{\sc  Moore}\ Waterfall}}{3}}
\newlabel{figure waterfall}{{1}{3}}
\@writefile{toc}{\contentsline {section}{\numberline {1}A Decisive Moment in Automated Theorem Proving}{3}}
\newlabel{section Preface}{{1}{3}}
\newlabel{note higher-order theorem provers}{{3}{3}}
\citation{moore-1973}
\citation{waterfall}
\citation{waterfallfirst}
\citation{bm}
\citation{boyer-moore-1973}
\citation{pop2}
\citation{boyer-moore-davies-1973}
\citation{moore-1981}
\citation{simonyi-interview}
\newlabel{note the Unit}{{7}{4}}
\citation{meltzer-1975}
\citation{kowalski-1988}
\newlabel{note people and departments}{{9}{5}}
\citation{boyer-moore-1971}
\citation{moore-1973}
\citation{moore-1973}
\citation{moore-1973}
\citation{moore-1973}
\citation{Kow74}
\citation{Kow74}
\citation{kowalski-1988}
\citation{Prolog}
\citation{waltherhandbook}
\citation{bundy-survey}
\@writefile{toc}{\contentsline {section}{\numberline {2}Method of Procedure and Presentation}{6}}
\citation{LISP}
\citation{boyer-moore-1973}
\citation{moore-1973}
\citation{haskell}
\citation{Pau96}
\citation{scott-LCF}
\citation{scott-LCF}
\citation{milner-1972}
\citation{fromLCFtoHOL}
\citation{wgjsc}
\citation{wirth-master}
\citation{wirth-master}
\citation{wirth-jsc}
\citation{term-rewriting-one}
\citation{wgjsc}
\citation{wirth-master}
\citation{wirth-master}
\citation{wirth-jsc}
\citation{KB70}
\citation{huet}
\citation{toyama}
\citation{firstCTRSeightyseven}
\citation{wirth-jsc}
\citation{bm}
\citation{moore-1973}
\citation{bm}
\citation{bm}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{waltherhandbook}
\citation{bundy-survey}
\citation{ACLTWO-CASESTUDIES}
\citation{ACLTWO-CASESTUDIES}
\citation{ACLTWO}
\@writefile{toc}{\contentsline {section}{\numberline {3}Organization of this Article}{9}}
\citation{cajori-1918}
\citation{hippa}
\citation{plato-induction}
\citation{elements}
\citation{freudenthal}
\citation{unguru-one}
\citation{plato-induction}
\citation{Greeks-induction}
\citation{fermatsproof}
\citation{Ravinovitch-Gershon}
\citation{katz-history}
\citation{maurolycus}
\citation{pascal}
\citation{fermat-birth-date}
\citation{catherine-goldstein-fermat-priceton-companion-math-2008}
\citation{fermatsproof}
\@writefile{toc}{\contentsline {section}{\numberline {4}Mathematical Induction}{10}}
\newlabel{section What is mathematical induction?}{{4}{10}}
\citation{wirthcardinal}
\citation{wirthcardinal}
\citation{axiomofchoice}
\citation{weakaxiomofchoice}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Well-Founded\discretionary {-}{}{}ness\ and Termination}{11}}
\newlabel{subsection Well-Foundedness and Termination}{{4.1}{11}}
\newlabel{lemma 1}{{4.1}{11}}
\citation{cohn-1965}
\citation{bourbaki-english}
\citation{bourbaki-set-theory-chapter-3-2nd-edn}
\citation{Shoenfield67}
\citation{course-of-values-induction}
\citation{bourbaki-set-theory-chapter-3-1st-edn}
\citation{bourbaki-set-theory-chapter-3-2nd-edn}
\citation{bourbaki-set-theory-chapter-3-1st-edn}
\citation{bourbaki-set-theory-chapter-3-2nd-edn}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}The Theorem of\/ {\sc  Noether}\discretionary {-}{}{}ian\ Induction}{12}}
\newlabel{subsection noetherian induction}{{4.2}{12}}
\newlabel{note complete induction}{{35}{12}}
\citation{geseraxiomofchoice}
\citation{geseraxiomofchoice}
\citation{axiomofchoice}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}An Induction Principle Stronger than {\sc  Noether}\discretionary {-}{}{}ian\ Induction?}{13}}
\newlabel{subsection Beyond Noetherian induction}{{4.3}{13}}
\citation{dedekind-1888}
\citation{wolff-rationalis-1740}
\citation{lambert-1764}
\citation{fries-vollstaendige-induction}
\citation{dedekind-1888}
\citation{dedekind-1888}
\citation{unendliche}
\citation{heijenoort-source-book}
\citation{grundlagenvortrag-zusatz}
\citation{heijenoort-source-book}
\citation{heijenoort-source-book}
\citation{hilbert-grundlagen-logik}
\citation{hilbert-grundlagen-logik}
\citation{unendliche}
\citation{grundlagenvortrag}
\citation{fachwoerterbuchmathematik}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}The Natural Numbers}{14}}
\newlabel{subsection Mathematical Induction and the Natural Numbers}{{4.4}{14}}
\newlabel{note fries}{{39}{14}}
\citation{peter-1951}
\citation{ackermann-1928a}
\citation{wirthcardinal}
\citation{pieri}
\citation{pieri}
\citation{peanonovamethodo}
\citation{padoa-1913}
\citation{smith-pieri}
\citation{pieri}
\citation{pieri}
\newlabel{note pieri standard}{{43}{15}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.5}Standard Data Types}{16}}
\newlabel{subsection Standard Data Types}{{4.5}{16}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.5.1}{\sc  Boole}an\ Values}{17}}
\newlabel{subsubsection Boolean Values}{{4.5.1}{17}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.5.2}Lists over Natural Numbers}{17}}
\citation{bm}
\citation{wirthcardinal}
\citation{grundlagen-second-edition-volume-two}
\citation{gentzen}
\citation{gwrta}
\citation{wirth-jsc}
\citation{grundlagen-second-edition-volume-two}
\citation{ackermann-consistency-of-arithmetic}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.6}The Standard High-Level Method of Mathematical Induction}{20}}
\newlabel{subsection The Standard High-Level Method of Mathematical Induction}{{4.6}{20}}
\newlabel{section items}{{4.6}{20}}
\citation{fermat-oeuvres}
\citation{fermat-career}
\citation{From-Fermat-to-Gauss}
\citation{fermatsproof}
\citation{fermatsproof}
\citation{fermat-oeuvres}
\citation{wirthcardinal}
\citation{DBLP:conf/lics/BrotherstonS07}
\citation{DBLP:conf/lics/BrotherstonS07}
\citation{brotherston-cut-elimination}
\citation{voicu-li-di}
\citation{zombie}
\citation{zombie}
\citation{swp200601}
\citation{SR--2011--01}
\citation{wirth-manifesto-ljigpl}
\citation{From-Fermat-to-Gauss}
\citation{fermatsproof}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.7}{Descente Infinie}}{21}}
\newlabel{subsection DescenteInfinie}{{4.7}{21}}
\newlabel{section example first proof of (+3)}{{4.7}{21}}
\citation{sergetableau}
\newlabel{example first proof of (+3)}{{4.2}{22}}
\newlabel{section example first proof of (less7)}{{4.7}{23}}
\newlabel{example first proof of (less7)}{{4.3}{23}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.8}Explicit Induction}{24}}
\newlabel{subsection Explicit Induction}{{4.8}{24}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.8.1}From the Theorem of\/ {\sc  Noether}\discretionary {-}{}{}ian\ Induction\ to Explicit Induction}{24}}
\citation{waltherIJCAI93}
\newlabel{section example second proof of (+3)}{{4.8.1}{25}}
\newlabel{example second proof of (+3)}{{4.4}{25}}
\citation{wirthcardinal}
\citation{church-rosser-bm}
\citation{church-rosser-bm}
\citation{lambda-calculus-final}
\newlabel{note Newman}{{65}{26}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.8.2}Theoretical Viewpoint on Explicit Induction}{27}}
\newlabel{subsubsection Theoretical Viewpoint}{{4.8.2}{27}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.8.3}Practical Viewpoint on Explicit Induction}{27}}
\newlabel{subsubsection Practical Viewpoint}{{4.8.3}{27}}
\citation{aubin-1976}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.9}Generalization}{28}}
\newlabel{subsection Generalization}{{4.9}{28}}
\newlabel{section example proof of (ack4)}{{4.9}{28}}
\citation{wirthcardinal}
\newlabel{example proof of (ack4)}{{4.5}{29}}
\citation{goedel}
\citation{gentzen}
\citation{induction-no-cut}
\citation{baazleitschcolllog}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.10}Proof-Theoretical Peculiarities of Mathematical Induction}{30}}
\newlabel{subsection Proof-Theoretical Peculiarities of Mathematical Induction}{{4.10}{30}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.11}Conclusion}{30}}
\newlabel{note no difference in practice}{{72}{30}}
\newlabel{note practice one}{{73}{30}}
\newlabel{note practice two}{{76}{30}}
\citation{wirth-jsc}
\@writefile{toc}{\contentsline {section}{\numberline {5}Recursion, Termination, and Induction}{31}}
\newlabel{section Recursive Definitions}{{5}{31}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Recursion and the Rewrite Relation on Ground Terms}{31}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Confluence}{31}}
\newlabel{subsection Confluence}{{5.2}{31}}
\citation{bm}
\citation{moore-1973}
\citation{bm}
\citation{bm}
\citation{LISP}
\newlabel{section example PLUS}{{5.2}{32}}
\newlabel{example PLUS}{{5.1}{32}}
\newlabel{note applicative}{{82}{32}}
\citation{wirth-jsc}
\citation{wirth-jsc}
\citation{bm}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Termination and Reducibility}{33}}
\newlabel{subsection Termination and Reducibility}{{5.3}{33}}
\citation{wgcade}
\citation{wirth-jsc}
\citation{Shoenfield67}
\citation{moore-1973}
\citation{moore-1973}
\citation{wgkp}
\citation{wgjsc}
\citation{wgjsc}
\citation{wgcade}
\citation{kwspec}
\citation{kwspec}
\citation{kwspec2}
\citation{wirthdiss}
\citation{wirthdiss}
\citation{wirth-jsc}
\citation{kuehlerdiss}
\citation{quodlibet-cade}
\citation{samoacalculemus}
\citation{samoacalculemus}
\citation{samoa-phd}
\citation{jancl}
\citation{wgcade}
\citation{kwspec2}
\citation{moore-1973}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}Constructor Variables}{34}}
\newlabel{subsection Constructor Variables}{{5.4}{34}}
\citation{bm}
\citation{bm}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5}Termination and General Induction Templates}{35}}
\newlabel{subsection Termination}{{5.5}{35}}
\newlabel{note on IF and COND}{{90}{35}}
\citation{waltherLPAR92}
\citation{waltherLPAR92}
\citation{waltherIJCAI93}
\citation{wirth-jsc}
\citation{wirthdiss}
\newlabel{example induction template two measured subsets constructor style}{{5.2}{37}}
\newlabel{example non-singleton measured subset constructor style}{{5.3}{37}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6}Termination of the Rewrite Relation on Ground Terms}{37}}
\citation{mutualexplicitinduction}
\citation{bm}
\citation{bm}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.7}Applicable Induction Templates for Explicit Induction}{38}}
\newlabel{note on general variables}{{95}{38}}
\newlabel{section example Applicable Induction Templates constructor style}{{5.7}{39}}
\newlabel{example Applicable Induction Templates constructor style}{{5.4}{39}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.8}Induction Schemes}{39}}
\newlabel{subsection Induction Schemes}{{5.8}{39}}
\citation{Fitting90}
\citation{Fitting90}
\citation{fitting}
\citation{wirthcardinal}
\citation{wirthcardinal}
\citation{wirth-jsc-non-permut}
\citation{SR--2011--01}
\newlabel{section example induction schemes constructor style}{{5.8}{41}}
\newlabel{example induction schemes constructor style}{{5.5}{41}}
\citation{davis-2009}
\@writefile{toc}{\contentsline {section}{\numberline {6}Automated Explicit Induction}{43}}
\newlabel{section Explicit Induction}{{6}{43}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.1}The Application Context of Automated Explicit Induction}{43}}
\newlabel{subsection The Application Context of Automated Explicit Induction}{{6.1}{43}}
\citation{burstall-1969}
\citation{burstall-1969}
\citation{darlington-1968}
\citation{Ble71}
\citation{Ble71}
\citation{bm}
\citation{boyer-moore-1973}
\citation{moore-1973}
\citation{moore-1975}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.2}The\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{44}}
\newlabel{The Pure Lisp Theorem Prover}{{6.2}{44}}
\newlabel{note burstall quotation}{{102}{44}}
\citation{moore-1973}
\citation{boyer-moore-2012}
\citation{moore-1973}
\citation{burstall-1969}
\citation{BBH72}
\citation{pop2}
\citation{moore-1973}
\citation{moore-1973}
\citation{moore-1973}
\citation{wirth-jsc}
\citation{moore-1973}
\citation{moore-1973}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.1}Simplification in the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{48}}
\newlabel{subsubsection Simplification in the pure}{{6.2.1}{48}}
\citation{moore-1973}
\citation{samoa-phd}
\citation{samoa-phd}
\citation{jancl}
\citation{moore-1973}
\citation{moore-1973}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.2}Destructor Elimination in the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{50}}
\newlabel{subsubsection Destructor Elimination in the PURE}{{6.2.2}{50}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.3}(Cross-) Fertilization in the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{50}}
\newlabel{fertilization in pure lisp theorem prover}{{6.2.3}{50}}
\newlabel{note no destructor elimination}{{119}{50}}
\citation{moore-1973}
\citation{moore-1973}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.4}Generalization in the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{51}}
\newlabel{subsubsection Generalization pure lisp theorem prover}{{6.2.4}{51}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.5}Elimination of Irrelevance in the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{51}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.6}Induction in the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{51}}
\newlabel{subsubsection Induction of pure lisp theorem prover}{{6.2.6}{51}}
\newlabel{note failure of synthesis}{{122}{51}}
\citation{moore-1973}
\newlabel{section example induction rule}{{6.2.6}{52}}
\newlabel{example induction rule}{{6.1}{52}}
\newlabel{section example merging}{{6.2.6}{53}}
\newlabel{section example second proof of (less7)}{{6.2.6}{53}}
\newlabel{example second proof of (less7)}{{6.2}{53}}
\newlabel{example merging}{{6.2}{53}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.7}Conclusion on the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{53}}
\newlabel{subsubsection Conclusion on the pure lisp theorem prover}{{6.2.7}{53}}
\citation{moore-1973}
\citation{bm}
\citation{bm}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{bm}
\citation{moore-1975}
\citation{moore-1975}
\citation{boyer-moore-1975}
\citation{boyer-2012}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{bm}
\citation{boyer-2012}
\citation{boyermoore}
\citation{bm}
\citation{moore-1973}
\citation{bm}
\citation{boyermoore}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{bm}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.3}{\sc  Thm}}{55}}
\newlabel{subsection theorem prover}{{6.3}{55}}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{bm}
\citation{wirth-pascal}
\citation{bm}
\citation{bm}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{bm}
\citation{boyermoore}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{bm}
\citation{boyermoore}
\citation{boyermoore}
\citation{boyermooresecondedition}
\newlabel{note jargon one}{{134}{56}}
\newlabel{note PACK}{{135}{56}}
\citation{bm}
\citation{bm}
\citation{bm}
\newlabel{note kaufmann non-standard}{{139}{58}}
\citation{bm}
\citation{bm}
\citation{bm}
\citation{bm}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.1}Simplification in\/ {\sc  Thm}}{59}}
\newlabel{subsubsection simplification in}{{6.3.1}{59}}
\citation{KB70}
\citation{bm}
\citation{jancl}
\citation{bm}
\citation{bm}
\citation{boyermoore}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{bm}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.2}Destructor Elimination in\/ {\sc  Thm}}{62}}
\newlabel{subsubsection Destructor Elimination in}{{6.3.2}{62}}
\newlabel{example and back}{{6.5}{62}}
\citation{bm}
\citation{bm}
\citation{bm}
\newlabel{example d l once}{{6.6}{64}}
\newlabel{example quotient and remainder}{{6.7}{64}}
\citation{bm}
\citation{bm}
\citation{bm}
\citation{bm}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.3}(Cross-) Fertilization in\/ {\sc  Thm}}{66}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.4}Generalization in\/ {\sc  Thm}}{66}}
\citation{bm}
\citation{bm}
\citation{wirthcardinal}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.5}Elimination of Irrelevance in\/ {\sc  Thm}}{67}}
\newlabel{subsubsection Elimination of Irrelevance in}{{6.3.5}{67}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.6}Induction in\/ {\sc  Thm}\ as compared to the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{68}}
\newlabel{subsubsection Induction in}{{6.3.6}{68}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.7}Induction Templates generated by Definition-Time Recursion Analysis}{68}}
\newlabel{subsubsection Induction Templates}{{6.3.7}{68}}
\citation{bm}
\citation{bm}
\citation{bm}
\newlabel{section example induction template two measured subsets}{{6.3.7}{69}}
\newlabel{example induction template two measured subsets}{{6.8}{69}}
\newlabel{example non-singleton measured subset}{{6.9}{69}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.8}Proof-Time Recursion Analysis in\/ {\sc  Thm}}{70}}
\newlabel{subsubsection Proof-Time Recursion Analysis in}{{6.3.8}{70}}
\newlabel{example Applicable Induction Templates}{{6.10}{70}}
\newlabel{example induction schemes}{{6.11}{70}}
\citation{bm}
\newlabel{example Subsumption}{{6.12}{71}}
\newlabel{note injectivity 1}{{169}{71}}
\newlabel{section example merging 2}{{6.3.8}{72}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces \footroom The induction schemes of Ex\discretionary {-}{}{}am\discretionary {-}{}{}ple\,6.13\hbox {}}}{72}}
\newlabel{figure induction schemes}{{2}{72}}
\citation{bm}
\citation{bm}
\citation{bm}
\newlabel{example merging 2}{{6.13}{73}}
\newlabel{note injectivity 2}{{170}{73}}
\citation{waltherLPAR92}
\citation{waltherLPAR92}
\citation{waltherIJCAI93}
\citation{stevens-rational-reconstruction}
\citation{bundy-recursion-analysis}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.9}Conclusion on {\sc  Thm}}{74}}
\newlabel{subsubsection Conclusion on}{{6.3.9}{74}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces Four possibilities to descend with rational representations of \nlbmath {\sqrt  2}:}}{75}}
\newlabel{figure square root}{{3}{75}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.4}{\sc  Nqthm}}{75}}
\newlabel{subsection NQTHM}{{6.4}{75}}
\citation{bm}
\citation{boyer-moore-1981-authors}
\citation{bmeval-1988}
\citation{boyermoore}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{boyer-moore-1988}
\citation{hunt-1985}
\citation{boyermooresecondedition}
\citation{presburger}
\citation{presburger-remarks-translation}
\citation{presburger-life}
\newlabel{note presburger}{{176}{76}}
\citation{shankar-1994}
\citation{shankar-1994}
\citation{moore-1989-1}
\citation{moore-1989-1}
\citation{moore-1989-2}
\citation{cli-1989-1}
\citation{hunt-1989}
\citation{young-1989}
\citation{bevier-1989}
\citation{c-string-lib-1996}
\citation{boyermoore}
\citation{commonlisp}
\citation{boyermooresecondedition}
\citation{ACLTWO}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.5}{\sc  ACL2}}{77}}
\newlabel{subsection ACLTWO}{{6.5}{77}}
\newlabel{note shankar}{{177}{77}}
\citation{brock-hunt-1999}
\citation{moore-lynch-kaufmann-1998}
\citation{russinoff-1998}
\citation{aamp7g-2005}
\citation{hunt-swords-2009}
\citation{brock-hunt-1999}
\citation{moore-lynch-kaufmann-1998}
\citation{rrl}
\citation{bm}
\citation{bm}
\citation{inkafuenf}
\citation{inductioncontest}
\citation{inka}
\citation{inkanext}
\citation{inkafuenf}
\citation{bm}
\citation{inka}
\citation{hutter-cade-nancy}
\citation{walthertermination}
\citation{walthertermination}
\citation{walthertermination2}
\citation{waltherLPAR92}
\citation{waltherLPAR92}
\citation{waltherIJCAI93}
\citation{protzenlazy}
\citation{protzenlazy}
\citation{protzendiss}
\citation{protzenpatching}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.6}Further Historically Important Explicit-Induction Systems}{79}}
\newlabel{subsection Further Most Noteworthy Explicit-Induction Systems}{{6.6}{79}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.6.1}{\sc  Rrl}}{79}}
\newlabel{section RRL}{{6.6.1}{79}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.6.2}{\sc  Inka}}{79}}
\newlabel{section INKA}{{6.6.2}{79}}
\newlabel{note induction contest}{{181}{79}}
\citation{oysterclam}
\citation{bundy-survey}
\citation{nuprl-book}
\citation{isabellesevenhundred}
\citation{DF03-CADE-19}
\citation{proofplanningsystems}
\citation{failure-guide-induction}
\citation{bundy-recursion-analysis}
\citation{bundy-survey}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.6.3}{\sc  Oyster}/{\rm  CL\kern -.36em\raise .39ex\hbox {\sc  a}\kern -.15emM}}{80}}
\citation{science-of-reasoning}
\citation{bundy-inductive-proof-planning}
\citation{proofplanningsystems}
\citation{bundy-inductive-proof-planning}
\citation{bundy-inductive-proof-planning}
\citation{science-of-reasoning}
\citation{proofplanningsystems}
\citation{dodi-diss}
\citation{proof_planning_with_multiple_strategies}
\citation{automatic-learning-proof-planning}
\citation{aubin-1976}
\citation{aubin-1976}
\citation{aubin-1976}
\citation{rippling-book}
\citation{aubin-1976}
\citation{aubin-1976}
\citation{aubin-1979}
\citation{rippling-book}
\@writefile{toc}{\contentsline {section}{\numberline {7}Alternative Approaches Besides Explicit Induction}{81}}
\newlabel{section Alternative Approaches to the Automation of Induction}{{7}{81}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Proof Planning}{81}}
\newlabel{subsection Proof Planning}{{7.1}{81}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.2}Rippling}{81}}
\newlabel{subsection Rippling}{{7.2}{81}}
\citation{hutter-rippling}
\citation{rippling}
\citation{failure-guide-induction}
\citation{rippling-calculus}
\citation{failure-guide-induction}
\citation{bm}
\citation{boyer-moore-1975}
\citation{boyer-moore-1975}
\citation{bm}
\citation{huethullotinductionlessinduction}
\citation{boyer-moore-1977}
\citation{musserinductionlessinduction}
\citation{inductionlessinduction1}
\citation{inductionlessinduction1}
\citation{gogueninductionlessinduction}
\citation{gogueninductionlessinduction}
\citation{aubin-1976}
\citation{bm}
\citation{bm}
\citation{gogueninductionlessinduction}
\citation{huethullotinductionlessinduction}
\citation{inductionlessinduction1}
\citation{musserinductionlessinduction}
\citation{inductionlesshistc}
\citation{inductionlesshista}
\citation{inductionlesshistb}
\citation{inductionlesshistd}
\citation{bachmair}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.3}Implicit Induction}{82}}
\citation{ZKK88}
\citation{rrl}
\citation{bevers&lewi}
\citation{reddy}
\citation{unicom}
\citation{GaSt}
\citation{spike}
\citation{padawitzjsc}
\citation{bachmair}
\citation{bm}
\citation{kapur1}
\citation{kapur2}
\citation{unicom}
\citation{bachmair}
\citation{KB70}
\citation{GaSt}
\citation{unicom}
\citation{GaSt}
\citation{bachmair}
\citation{wirthdiss}
\citation{kuehlerdiss}
\citation{wirthbecker}
\citation{bachmair}
\citation{SR--88--12}
\citation{SR--88--12}
\citation{simplificationorderings}
\citation{geser-improved-general-path-order}
\citation{inductionlessinduction1}
\citation{inductionlessinduction1}
\citation{inductionlessinduction2}
\citation{gogueninductionlessinduction}
\citation{protzenlazy}
\citation{comonAR}
\citation{zombie}
\citation{kuehler-master}
\citation{unicom}
\citation{kuehler-master}
\citation{kuehler-master}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.4}{\sc  Quod\discretionary {-}{}{}Libet}}{84}}
\newlabel{section QUODLIBET}{{7.4}{84}}
\citation{loechner-lpo}
\citation{wirthdiss}
\citation{kuehlerdiss}
\citation{wirth-master}
\citation{wgjsc}
\citation{wgkp}
\citation{wgcade}
\citation{wirth-jsc}
\citation{kwspec}
\citation{kwspec}
\citation{wirthconfluence}
\citation{wgcade}
\citation{kwspec}
\citation{loechner-lpo}
\citation{quodlibet-cade}
\citation{SR--95--15}
\citation{wirthdiss}
\citation{kuehlerdiss}
\citation{samoa-phd}
\citation{quodlibet-cade}
\citation{wirthcardinal}
\citation{wirthcardinal}
\citation{SR--2011--01}
\citation{kuehlerdiss}
\citation{bm}
\citation{kuehlerdiss}
\citation{wirth-pascal}
\citation{kuehlerdiss}
\citation{samoa-phd}
\citation{samoa-phd}
\citation{jancl}
\citation{samoa-phd}
\citation{samoacalculemus}
\citation{samoacalculemus}
\citation{samoa-phd}
\citation{wirth-manifesto-ljigpl}
\@writefile{toc}{\contentsline {section}{\numberline {8}Lessons Learned}{88}}
\newlabel{section Lessons Learned}{{8}{88}}
\citation{boyer-moore-2012}
\citation{gramlich-phdthesis96}
\citation{Goodstein_1945}
\citation{Goodstein_Number_Theory}
\citation{writing-mathematics}
\citation{Boy71}
\citation{boyer-moore-fast-string-searching}
\citation{boyer-moore-1977}
\citation{boyer-moore-proof-checking-RSA}
\citation{boyer-moore-turing-completeness-lisp}
\citation{boyer-moore-halting-problem}
\citation{boyer-moore-1985}
\citation{BM90}
\citation{boyer-moore-shostak}
\citation{boyer-yu-1992}
\citation{moore-1979}
\citation{herbrand-handbook}
\citation{wirth-heijenoort}
\@writefile{toc}{\contentsline {section}{\numberline {9}Conclusion}{89}}
\newlabel{section Conclusion}{{9}{89}}
\@writefile{toc}{\contentsline {section}{Acknowledgments}{89}}
\bibdata{herbrandbib}
\bibcite{seventhPOPLeighty}{\citeauthoryear {Abrahams \bgroup \&al.\egroup }{1980}}
\bibcite{plato-induction}{\citeauthoryear {Acerbi{\acerbiindex }}{2000}}
\bibcite{ackermann-1928a}{\citeauthoryear {Ackermann\ackermannindex }{1928}}
\bibcite{ackermann-consistency-of-arithmetic}{\citeauthoryear {Ackermann\ackermannindex }{1940}}
\bibcite{kaci-nivat}{\citeauthoryear {A{\"\i }t-Kaci \bgroup \&\ \egroup Nivat}{1989}}
\bibcite{anon-1899}{\citeauthoryear {Anon}{1899}}
\bibcite{aamp7g-2005}{\citeauthoryear {Anon}{2005}}
\bibcite{fourthIJCAReight}{\citeauthoryear {Armando \bgroup \&al.\egroup }{2008}}
\bibcite{aubin-1976}{\citeauthoryear {Aubin{\index {Aubin, Raymond}}}{1976}}
\citation{aubin-1979}
\bibcite{aubin-1979}{\citeauthoryear {Aubin{\index {Aubin, Raymond}}}{1979}}
\citation{aubin-1976}
\bibcite{sergetableau}{\citeauthoryear {Autexier{\index {Autexier, Serge (*1971)}}}{2005}}
\citation{fourteenthTABLEAUfive}
\bibcite{inkafuenf}{\citeauthoryear {Autexier{\index {Autexier, Serge (*1971)}} \bgroup \&al.\egroup }{1999}}
\citation{sixteenthCADEninetynine}
\bibcite{quodlibet-cade}{\citeauthoryear {Avenhaus \bgroup \&al.\egroup }{2003}}
\citation{nineteenthCADEthree}
\bibcite{nineteenthCADEthree}{\citeauthoryear {Baader}{2003}}
\bibcite{baazleitschcolllog}{\citeauthoryear {Baaz \bgroup \&\ \egroup Leitsch}{1995}}
\bibcite{bachmair}{\citeauthoryear {Bachmair}{1988}}
\citation{lics3}
\bibcite{Hotz-Festschrift}{\citeauthoryear {Bachmair \bgroup \&al.\egroup }{1992}}
\bibcite{ijcai13}{\citeauthoryear {Bajscy}{1993}}
\bibcite{lambda-calculus-1st}{\citeauthoryear {Barendregt}{1981}}
\citation{lambda-calculus-final}
\bibcite{lambda-calculus-final}{\citeauthoryear {Barendregt}{2012}}
\citation{lambda-calculus-1st}
\bibcite{fermatslife-english-2}{\citeauthoryear {Barner{\index {Barner, Klaus}}}{2001a}}
\citation{fermatslife}
\@writefile{toc}{\contentsline {section}{References}{91}}
\bibcite{fermatslife}{\citeauthoryear {Barner{\index {Barner, Klaus}}}{2001b}}
\citation{fermat-birth-date}
\citation{fermatslife-english-1}
\citation{fermatslife-english-1}
\citation{fermatslife-english-2}
\bibcite{fermatslife-english-1}{\citeauthoryear {Barner{\index {Barner, Klaus}}}{2001c}}
\citation{fermatslife}
\citation{fermat-birth-date}
\bibcite{fermat-birth-date}{\citeauthoryear {Barner{\index {Barner, Klaus}}}{2007}}
\citation{fermatslife-english-1}
\bibcite{rippling-calculus}{\citeauthoryear {Basin{\index {Basin, David}} \bgroup \&\ \egroup Walsh}{1996}}
\bibcite{becker-griechische}{\citeauthoryear {Becker}{1965}}
\bibcite{fourteenthTABLEAUfive}{\citeauthoryear {Beckert}{2005}}
\bibcite{waterfall}{\citeauthoryear {Bell \bgroup \&\ \egroup Thayer}{1976}}
\citation{secondICSEseventysix}
\bibcite{C26}{\citeauthoryear {Benz{\discretionary {-}{}{}}m{\unprotectedue }ller{\index {Benzmueller, Christoph (*1968)@{Benzm\"uller, Christoph\ (*1968)}}} \bgroup \&al.\egroup }{2008}}
\citation{fourthIJCAReight}
\bibcite{logiktexte}{\citeauthoryear {Berka \bgroup \&\ \egroup Kreiser}{1973}}
\bibcite{grundlagenvortrag-zusatz}{\citeauthoryear {Bernays{\index {Bernays, Paul (1888--1977)}}}{1928}}
\citation{heijenoort-source-book}
\bibcite{bevers&lewi}{\citeauthoryear {Bevers \bgroup \&\ \egroup Lewi}{1990}}
\citation{secondCTRSninety}
\bibcite{bevier-1989}{\citeauthoryear {Bevier}{1989}}
\bibcite{cli-1989-1}{\citeauthoryear {Bevier \bgroup \&al.\egroup }{1989}}
\bibcite{fifthCADEeighty}{\citeauthoryear {Bibel \bgroup \&\ \egroup Kowalski{\index {Kowalski, Robert A. (*1941)}}}{1980}}
\bibcite{inka}{\citeauthoryear {Biundo \bgroup \&al.\egroup }{1986}}
\citation{eighthCADEeightysix}
\bibcite{Ble71}{\citeauthoryear {Bledsoe{\bledsoeindex }}{1971}}
\bibcite{BBH72-short}{\citeauthoryear {Bledsoe{\bledsoeindex } \bgroup \&al.\egroup }{1971}}
\citation{ijcai2}
\citation{BBH72}
\bibcite{BBH72}{\citeauthoryear {Bledsoe{\bledsoeindex } \bgroup \&al.\egroup }{1972}}
\citation{BBH72-short}
\bibcite{after-25-years}{\citeauthoryear {Bledsoe{\bledsoeindex } \bgroup \&\ \egroup Loveland}{1984}}
\bibcite{twentyfirstCAVnine}{\citeauthoryear {Bouajjani \bgroup \&\ \egroup Maler}{2009}}
\bibcite{spike}{\citeauthoryear {Bouhoula \bgroup \&\ \egroup Rusinowitch}{1995}}
\bibcite{bourbaki-set-theory-results-1st-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1939}}
\citation{churchbourbaki}
\citation{bourbaki-set-theory-results-2nd-edn}
\bibcite{bourbaki-set-theory-results-2nd-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1951}}
\citation{bourbaki-set-theory-results-1st-edn}
\citation{bourbaki-set-theory-results-3rd-edn}
\bibcite{bourbaki-set-theory-chapter-1-2-1st-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1954}}
\citation{bourbaki-set-theory-chapter-1-2-2nd-edn}
\bibcite{bourbaki-set-theory-chapter-3-1st-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1956}}
\citation{bourbaki-set-theory-chapter-3-2nd-edn}
\bibcite{bourbaki-set-theory-chapter-4-1st-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1958a}}
\citation{bourbaki-set-theory-chapter-4-2nd-edn}
\bibcite{bourbaki-set-theory-results-3rd-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1958b}}
\citation{bourbaki-set-theory-results-2nd-edn}
\citation{bourbaki-set-theory-results-4th-edn}
\bibcite{bourbaki-set-theory-chapter-1-2-2nd-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1960}}
\citation{bourbaki-set-theory-chapter-1-2-1st-edn}
\citation{bourbaki-set-theory-chapter-1-2-3rd-edn}
\bibcite{bourbaki-set-theory-results-4th-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1964}}
\citation{bourbaki-set-theory-results-3rd-edn}
\citation{bourbaki-set-theory-results-5th-edn}
\bibcite{bourbaki-set-theory-chapter-4-2nd-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1966a}}
\citation{bourbaki-set-theory-chapter-4-1st-edn}
\citation{bourbaki-english}
\bibcite{bourbaki-set-theory-chapter-1-2-3rd-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1966b}}
\citation{bourbaki-set-theory-chapter-1-2-2nd-edn}
\citation{bourbaki-english}
\bibcite{bourbaki-set-theory-chapter-3-2nd-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1967}}
\citation{bourbaki-set-theory-chapter-3-1st-edn}
\citation{bourbaki-english}
\bibcite{bourbaki-english}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1968a}}
\citation{bourbaki-set-theory-chapter-1-2-3rd-edn}
\citation{bourbaki-set-theory-chapter-1-2-3rd-edn}
\citation{bourbaki-set-theory-chapter-3-2nd-edn}
\citation{bourbaki-set-theory-chapter-4-2nd-edn}
\citation{bourbaki-set-theory-results-5th-edn}
\bibcite{bourbaki-set-theory-results-5th-edn}{\citeauthoryear {Bourbaki{\index {Bourbaki, Nicolas (pseudonym)}}}{1968b}}
\citation{bourbaki-set-theory-results-4th-edn}
\citation{bourbaki-english}
\bibcite{Boy71}{\citeauthoryear {Boyer{\boyerindex }}{1971}}
\bibcite{boyer-2012}{\citeauthoryear {Boyer{\boyerindex }}{2012}}
\bibcite{boyer-moore-davies-1973}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&al.\egroup }{1973}}
\bibcite{boyer-moore-1971}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1971}}
\citation{boyer-moore-1972}
\bibcite{boyer-moore-1972}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1972}}
\citation{machine-intelligence-7}
\bibcite{boyer-moore-1973}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1973}}
\citation{ijcai3}
\citation{boyer-moore-1975}
\bibcite{boyer-moore-1975}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1975}}
\citation{boyer-moore-1973}
\bibcite{boyer-moore-fast-string-searching}{\citeauthoryear {Boyer{\boyerindex \index {Boyer--Moore fast string searching algorithm}} \bgroup \&\ \egroup Moore{\mooreindex }}{1977}}
\bibcite{boyer-moore-1977}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1977}}
\citation{ijcai5}
\bibcite{bm}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1979}}
\bibcite{boyer-moore-1981-editors}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1981a}}
\bibcite{boyer-moore-1981-authors}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1981b}}
\citation{boyer-moore-1981-editors}
\bibcite{boyer-moore-turing-completeness-lisp}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1984a}}
\citation{after-25-years}
\bibcite{boyer-moore-halting-problem}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1984b}}
\bibcite{boyer-moore-proof-checking-RSA}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1984c}}
\bibcite{boyer-moore-1985}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1985}}
\bibcite{bmeval-1987}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1987}}
\citation{bmeval-1988}
\citation{bmeval-1988}
\citation{bmeval-1989}
\bibcite{bmeval-1988}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1988a}}
\citation{bmeval-1987}
\citation{bmeval-1987}
\citation{bmeval-1989}
\bibcite{boyermoore}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1988b}}
\citation{boyermooresecondedition}
\bibcite{boyer-moore-1988}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1988c}}
\citation{machine-intelligence-11}
\bibcite{bmeval-1989}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1989}}
\citation{broy-1989}
\citation{bmeval-1987}
\citation{bmeval-1987}
\citation{bmeval-1988}
\bibcite{BM90}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1990}}
\citation{tenthCADEninety}
\bibcite{boyermooresecondedition}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Moore{\mooreindex }}{1998}}
\citation{boyermoore}
\bibcite{boyer-moore-shostak}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&al.\egroup }{1976}}
\citation{thirdPOPLseventysix}
\bibcite{boyer-yu-1992}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Yu}{1992}}
\citation{eleventhCADEninetytwo}
\bibcite{c-string-lib-1996}{\citeauthoryear {Boyer{\boyerindex } \bgroup \&\ \egroup Yu}{1996}}
\bibcite{brock-hunt-1999}{\citeauthoryear {Brock \bgroup \&\ \egroup Hunt{\index {Hunt, Warren A.}}}{1999}}
\citation{industrial-strength-1999}
\bibcite{DBLP:conf/tableaux/Brotherston05}{\citeauthoryear {Brotherston}{2005}}
\citation{fourteenthTABLEAUfive}
\citation{brotherston-cut-elimination}
\bibcite{DBLP:conf/lics/BrotherstonS07}{\citeauthoryear {Brotherston \bgroup \&\ \egroup Simpson}{2007}}
\citation{lics22}
\citation{brotherston-cut-elimination}
\bibcite{brotherston-cut-elimination}{\citeauthoryear {Brotherston \bgroup \&\ \egroup Simpson}{2011}}
\citation{DBLP:conf/tableaux/Brotherston05}
\citation{DBLP:conf/lics/BrotherstonS07}
\bibcite{satallax}{\citeauthoryear {Brown}{2012}}
\citation{sixthIJCARtwelve}
\bibcite{broy-1989}{\citeauthoryear {Broy}{1989}}
\bibcite{waldmeister}{\citeauthoryear {Buch \bgroup \&\ \egroup Hillenbrand{\index {Hillenbrand, Thomas}}}{1996}}
\bibcite{bundy-inductive-proof-planning}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}}}{1988}}
\citation{ninthCADEeightyeight}
\bibcite{science-of-reasoning}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}}}{1989}}
\citation{honor-robinson}
\bibcite{twelvethCADEninetyfour}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}}}{1994}}
\bibcite{bundy-survey}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}}}{1999}}
\citation{HandbookAR}
\bibcite{bundy-recursion-analysis}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}} \bgroup \&al.\egroup }{1989}}
\citation{ijcai11}
\bibcite{oysterclam}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}} \bgroup \&al.\egroup }{1990}}
\citation{tenthCADEninety}
\bibcite{rippling-book}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}} \bgroup \&al.\egroup }{2005}}
\bibcite{rippling}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}} \bgroup \&al.\egroup }{1991}}
\bibcite{burstall-1969}{\citeauthoryear {Burstall{\index {Burstall, Rod M. (*1934)}}}{1969}}
\bibcite{pop2}{\citeauthoryear {Burstall{\index {Burstall, Rod M. (*1934)}} \bgroup \&al.\egroup }{1971}}
\bibcite{maurolycus}{\citeauthoryear {Bussey}{1917}}
\bibcite{From-Fermat-to-Gauss}{\citeauthoryear {Bussotti}{2006}}
\bibcite{cajori-1918}{\citeauthoryear {Cajori}{1918}}
\bibcite{churchbourbaki}{\citeauthoryear {Church{\index {Church, Alonzo (1903--1995)}}}{1946}}
\citation{bourbaki-set-theory-results-1st-edn}
\bibcite{Prolog}{\citeauthoryear {Clocksin \bgroup \&\ \egroup Mellish}{2003}}
\bibcite{cohn-1965}{\citeauthoryear {Cohn}{1965}}
\citation{cohn-1981}
\bibcite{cohn-1981}{\citeauthoryear {Cohn}{1981}}
\citation{cohn-1965}
\bibcite{eighthRTAninetyseven}{\citeauthoryear {Comon}{1997}}
\bibcite{comonAR}{\citeauthoryear {Comon}{2001}}
\citation{HandbookAR}
\bibcite{nuprl-book}{\citeauthoryear {Constable \bgroup \&al.\egroup }{1985}}
\bibcite{ijcai2}{\citeauthoryear {Cooper}{1971}}
\bibcite{dac/2001}{\citeauthoryear {DAC}{2001}}
\bibcite{darlington-1968}{\citeauthoryear {Darlington}{1968}}
\citation{machine-intelligence-3}
\bibcite{davis-2009}{\citeauthoryear {Davis}{2009}}
\bibcite{dedekind-1888}{\citeauthoryear {Dedekind{\dedekindindex }}{1888}}
\citation{dedekind-1930-32}
\citation{dedekind-1969}
\bibcite{dedekind-1930-32}{\citeauthoryear {Dedekind{\dedekindindex }}{1930--32}}
\bibcite{dedekind-1969}{\citeauthoryear {Dedekind{\dedekindindex }}{1969}}
\bibcite{proofplanningsystems}{\citeauthoryear {Dennis \bgroup \&al.\egroup }{2005}}
\bibcite{thirdRTAeightynine}{\citeauthoryear {Dershowitz}{1989}}
\bibcite{term-rewriting-one}{\citeauthoryear {Dershowitz \bgroup \&\ \egroup Jouannaud}{1990}}
\citation{handbook-tcs}
\bibcite{fourthCTRSninetyfour}{\citeauthoryear {Dershowitz \bgroup \&\ \egroup Lindenstrauss}{1995}}
\bibcite{dodi-diss}{\citeauthoryear {Dietrich}{2011}}
\bibcite{DF03-CADE-19}{\citeauthoryear {Dixon \bgroup \&\ \egroup Fleuriot}{2003}}
\citation{nineteenthCADEthree}
\bibcite{fachwoerterbuchmathematik}{\citeauthoryear {Eisenreich \bgroup \&\ \egroup Sube}{1982}}
\bibcite{elements}{\citeauthoryear {Euclid{\euclidindex }}{ca.\,300\,{\sc  b.c.}}}
\bibcite{fermat-oeuvres}{\citeauthoryear {Fermat}{1891\unhbox \voidb@x \hbox {}{ff.}}}
\bibcite{Fitting90}{\citeauthoryear {Fitting}{1990}}
\citation{fitting}
\bibcite{fitting}{\citeauthoryear {Fitting}{1996}}
\citation{Fitting90}
\bibcite{focs21}{\citeauthoryear {FOCS}{1980}}
\bibcite{Greeks-induction}{\citeauthoryear {Fowler}{1994}}
\bibcite{freudenthal}{\citeauthoryear {Freudenthal}{1953}}
\bibcite{inductionlesshistb}{\citeauthoryear {Fribourg}{1986}}
\citation{thirteenthICALPeightysix}
\bibcite{fries-vollstaendige-induction}{\citeauthoryear {Fries{\index {Fries, Jakob Friedrich (1773--1843)}}}{1822}}
\citation{fries-saemtliche}
\bibcite{fries-saemtliche}{\citeauthoryear {Fries{\index {Fries, Jakob Friedrich (1773--1843)}}}{1967\unhbox \voidb@x \hbox {}{ff.}}}
\bibcite{hippa}{\citeauthoryear {Fritz}{1945}}
\citation{becker-griechische}
\bibcite{future-generation}{\citeauthoryear {Fuchi \bgroup \&\ \egroup Kott}{1988}}
\bibcite{handbooklogicailpvol2}{\citeauthoryear {Gabbay{\index {Gabbay, Dov (*1945)}} \bgroup \&al.\egroup }{1994}}
\bibcite{handbook-of-the-history-of-logic}{\citeauthoryear {Gabbay{\index {Gabbay, Dov (*1945)}} \bgroup \&\ \egroup Woods}{2004\unhbox \voidb@x \hbox {}{ff.}}}
\bibcite{seventhRTAninetysix}{\citeauthoryear {Ganzinger}{1996}}
\bibcite{sixteenthCADEninetynine}{\citeauthoryear {Ganzinger}{1999}}
\bibcite{GaSt}{\citeauthoryear {Ganzinger \bgroup \&\ \egroup Stuber}{1992}}
\citation{Hotz-Festschrift}
\citation{thirdCTRSninetytwo}
\bibcite{gentzen}{\citeauthoryear {Gentzen{\index {Gentzen, Gerhard (1909--1945)}}}{1935}}
\citation{logiktexte}
\citation{gentzen-collected}
\bibcite{gentzen-collected}{\citeauthoryear {Gentzen{\index {Gentzen, Gerhard (1909--1945)}}}{1969}}
\bibcite{geseraxiomofchoice}{\citeauthoryear {Geser}{1995}}
\citation{Kolloquium-Programmiersprachen-und-Grundlagen-der-Programmierung}
\bibcite{geser-improved-general-path-order}{\citeauthoryear {Geser}{1996}}
\bibcite{writing-mathematics}{\citeauthoryear {Gillman}{1987}}
\bibcite{inductionlesshistc}{\citeauthoryear {G{\"o}bel}{1985}}
\citation{gwai9}
\bibcite{goedel}{\citeauthoryear {G{\unprotectedoe de{\index {Goedel, Kurt@G\"odel, Kurt (1906--1978)}}l}}{1931}}
\citation{goedelcollected}
\citation{heijenoort-source-book}
\citation{goedel-meltzer}
\bibcite{goedel-meltzer}{\citeauthoryear {G{\unprotectedoe de{\index {Goedel, Kurt@G\"odel, Kurt (1906--1978)}}l}}{1962}}
\citation{goedel}
\bibcite{goedelcollected}{\citeauthoryear {G{\unprotectedoe de{\index {Goedel, Kurt@G\"odel, Kurt (1906--1978)}}l}}{1986ff.}}
\bibcite{gogueninductionlessinduction}{\citeauthoryear {Goguen}{1980}}
\citation{fifthCADEeighty}
\bibcite{catherine-goldstein-fermat-priceton-companion-math-2008}{\citeauthoryear {Goldstein{\index {Goldstein, Catherine (*1958)}}}{2008}}
\citation{priceton-companion-math-2008}
\bibcite{Goodstein_1945}{\citeauthoryear {Goodstein{\index {Goodstein, R. L. (1912--1985)}}}{1945}}
\bibcite{Goodstein_Number_Theory}{\citeauthoryear {Goodstein{\index {Goodstein, R. L. (1912--1985)}}}{1957}}
\bibcite{fromLCFtoHOL}{\citeauthoryear {Gordon{\index {Gordon, Mike J. C. (*1948)}}}{2000}}
\citation{honorrobinmilner}
\bibcite{firstIJCARone}{\citeauthoryear {Gore \bgroup \&al.\egroup }{2001}}
\bibcite{priceton-companion-math-2008}{\citeauthoryear {Gowers \bgroup \&al.\egroup }{2008}}
\bibcite{thirdPOPLseventysix}{\citeauthoryear {Graham \bgroup \&al.\egroup }{1976}}
\bibcite{gramlich-phdthesis96}{\citeauthoryear {Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (1959--2014)}}ch}{1996}}
\bibcite{unicom}{\citeauthoryear {Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (1959--2014)}}ch \bgroup \&\ \egroup Lindner}{1991}}
\bibcite{sixthIJCARtwelve}{\citeauthoryear {Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (1959--2014)}}ch \bgroup \&al.\egroup }{2012}}
\bibcite{gwrta}{\citeauthoryear {Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (1959--2014)}}ch \bgroup \&\ \egroup Wirth{\index {Wirth, Claus-Peter (*1963)}}}{1996}}
\citation{seventhRTAninetysix}
\bibcite{machine-intelligence-11}{\citeauthoryear {Hayes \bgroup \&al.\egroup }{1988}}
\bibcite{heijenoort-source-book}{\citeauthoryear {Heijenoort{\index {Heijenoort, Jean van (1912--1986)}}}{1971}}
\bibcite{Coq1}{\citeauthoryear {Herbelin}{2009}}
\bibcite{grundlagen-der-geometrie}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1899}}
\citation{anon-1899}
\citation{hilbert-2004}
\citation{grundlagen-der-geometrie-siebte}
\citation{grundlagen-der-geometrie-neunte}
\citation{grundlagen-der-geometrie-neunte}
\citation{grundlagen-der-geometrie-zehnte}
\citation{grundlagen-der-geometrie-elfte}
\citation{principes-fondamentaux-de-la-geometrie}
\citation{foundations-of-geometry}
\citation{foundations-of-geometry-second}
\bibcite{hilbert-zahlbegriff}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1900a}}
\citation{grundlagen-der-geometrie-dritte}
\citation{grundlagen-der-geometrie-dritte}
\citation{grundlagen-der-geometrie-vierte}
\citation{grundlagen-der-geometrie-fuenfte}
\citation{grundlagen-der-geometrie-sechste}
\citation{grundlagen-der-geometrie-siebte}
\bibcite{principes-fondamentaux-de-la-geometrie}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1900b}}
\citation{grundlagen-der-geometrie}
\bibcite{foundations-of-geometry}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1902}}
\citation{grundlagen-der-geometrie}
\bibcite{grundlagen-der-geometrie-zweite}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1903}}
\citation{grundlagen-der-geometrie}
\bibcite{hilbert-grundlagen-logik}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1905}}
\citation{dritter-mathematiker}
\citation{grundlagen-der-geometrie-dritte}
\citation{grundlagen-der-geometrie-dritte}
\citation{grundlagen-der-geometrie-vierte}
\citation{grundlagen-der-geometrie-fuenfte}
\citation{grundlagen-der-geometrie-sechste}
\citation{grundlagen-der-geometrie-siebte}
\citation{heijenoort-source-book}
\bibcite{grundlagen-der-geometrie-dritte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1909}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-zweite}
\citation{hilbert-zahlbegriff}
\citation{hilbert-grundlagen-logik}
\bibcite{grundlagen-der-geometrie-vierte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1913}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-dritte}
\bibcite{grundlagen-der-geometrie-fuenfte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1922}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-vierte}
\citation{grundlagen-der-geometrie-vierte}
\bibcite{grundlagen-der-geometrie-sechste}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1923}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-fuenfte}
\bibcite{unendliche}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1926}}
\citation{grundlagen-der-geometrie-siebte}
\citation{heijenoort-source-book}
\bibcite{grundlagenvortrag}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1928}}
\citation{grundlagen-der-geometrie-siebte}
\citation{heijenoort-source-book}
\bibcite{probleme-grundlegung}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1930a}}
\citation{grundlagen-der-geometrie-siebte}
\bibcite{grundlagen-der-geometrie-siebte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1930b}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-sechste}
\citation{unendliche}
\citation{grundlagenvortrag}
\citation{probleme-grundlegung}
\bibcite{grundlagen-der-geometrie-achte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1956}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-siebte}
\bibcite{grundlagen-der-geometrie-neunte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1962}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-achte}
\bibcite{grundlagen-der-geometrie-zehnte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1968}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-neunte}
\bibcite{foundations-of-geometry-second}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1971}}
\citation{foundations-of-geometry}
\citation{grundlagen-der-geometrie-zehnte}
\bibcite{grundlagen-der-geometrie-elfte}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{1972}}
\citation{grundlagen-der-geometrie}
\citation{grundlagen-der-geometrie-zehnte}
\bibcite{hilbert-2004}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt}{2004}}
\bibcite{grundlagen-first-edition-volume-two}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt \bgroup \&\ \egroup Bernays{\index {Bernays, Paul (1888--1977)}}}{1939}}
\citation{grundlagen-second-edition-volume-two}
\bibcite{grundlagen-second-edition-volume-two}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt \bgroup \&\ \egroup Bernays{\index {Bernays, Paul (1888--1977)}}}{1970}}
\citation{grundlagen-first-edition-volume-two}
\bibcite{HL02}{\citeauthoryear {Hillenbrand{\index {Hillenbrand, Thomas}} \bgroup \&\ \egroup L{\unprotectedoe }chner{\index {Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}}}{2002}}
\citation{eightteenthCADEtwo}
\bibcite{industrial-strength-1999}{\citeauthoryear {Hinchey \bgroup \&\ \egroup Bowen}{1999}}
\bibcite{5-int-congress-mathematicians-1912}{\citeauthoryear {Hobson \bgroup \&\ \egroup Love}{1913}}
\bibcite{weakaxiomofchoice}{\citeauthoryear {Howard{\index {Howard, Paul (*1943)}} \bgroup \&\ \egroup Rubin{\index {Rubin, Jean E. (1926--2002)}}}{1998}}
\bibcite{haskell}{\citeauthoryear {Hudlak \bgroup \&al.\egroup }{1999}}
\bibcite{huet}{\citeauthoryear {Huet}{1980}}
\bibcite{huethullotinductionlessinduction}{\citeauthoryear {Huet \bgroup \&\ \egroup Hullot}{1980}}
\citation{focs21}
\bibcite{hunt-1985}{\citeauthoryear {Hunt{\index {Hunt, Warren A.}}}{1985}}
\citation{hunt-1994}
\bibcite{hunt-1989}{\citeauthoryear {Hunt{\index {Hunt, Warren A.}}}{1989}}
\bibcite{hunt-1994}{\citeauthoryear {Hunt{\index {Hunt, Warren A.}}}{1994}}
\citation{hunt-1985}
\bibcite{hunt-swords-2009}{\citeauthoryear {Hunt{\index {Hunt, Warren A.}} \bgroup \&\ \egroup Swords}{2009}}
\citation{twentyfirstCAVnine}
\bibcite{hutter-rippling}{\citeauthoryear {Hutter{\index {Hutter, Dieter (*1959)}}}{1990}}
\citation{tenthCADEninety}
\bibcite{hutter-cade-nancy}{\citeauthoryear {Hutter{\index {Hutter, Dieter (*1959)}}}{1994}}
\citation{twelvethCADEninetyfour}
\bibcite{inductioncontest}{\citeauthoryear {Hutter{\index {Hutter, Dieter (*1959)}} \bgroup \&\ \egroup Bundy{\index {Bundy, Alan (*1947)}}}{1999}}
\citation{sixteenthCADEninetynine}
\bibcite{inkanext}{\citeauthoryear {Hutter{\index {Hutter, Dieter (*1959)}} \bgroup \&\ \egroup Sengler}{1996}}
\citation{thirteenthCADEninetysix}
\bibcite{siekmann-60}{\citeauthoryear {Hutter{\index {Hutter, Dieter (*1959)}} \bgroup \&\ \egroup Stephan}{2005}}
\bibcite{ieeeweston70}{\citeauthoryear {IEEE WESTON}{1970}}
\bibcite{failure-guide-induction}{\citeauthoryear {Ireland{\index {Ireland, Andrew}} \bgroup \&\ \egroup Bundy{\index {Bundy, Alan (*1947)}}}{1994}}
\bibcite{automatic-learning-proof-planning}{\citeauthoryear {Jamnik \bgroup \&al.\egroup }{2003}}
\bibcite{inductionlesshista}{\citeauthoryear {Jouannaud \bgroup \&\ \egroup Kounalis}{1986}}
\citation{lics1}
\bibcite{firstCTRSeightyseven}{\citeauthoryear {Kaplan \bgroup \&\ \egroup Jouannaud}{1988}}
\bibcite{secondCTRSninety}{\citeauthoryear {Kaplan \bgroup \&\ \egroup Okada}{1991}}
\bibcite{eleventhCADEninetytwo}{\citeauthoryear {Kapur}{1992}}
\bibcite{kapur2}{\citeauthoryear {Kapur \bgroup \&\ \egroup Musser}{1986}}
\citation{lics1}
\bibcite{kapur1}{\citeauthoryear {Kapur \bgroup \&\ \egroup Musser}{1987}}
\bibcite{mutualexplicitinduction}{\citeauthoryear {Kapur \bgroup \&\ \egroup Subramaniam}{1996}}
\citation{fifthAMASTninetysix}
\bibcite{rrl}{\citeauthoryear {Kapur \bgroup \&\ \egroup Zhang}{1989}}
\citation{thirdRTAeightynine}
\citation{Kapur95}
\bibcite{Kapur95}{\citeauthoryear {Kapur \bgroup \&\ \egroup Zhang}{1995}}
\bibcite{katz-history}{\citeauthoryear {Katz}{1998}}
\bibcite{ACLTWO-CASESTUDIES}{\citeauthoryear {Kaufmann{\index {Kaufmann, Matt (*1952)}} \bgroup \&al.\egroup }{2000a}}
\bibcite{ACLTWO}{\citeauthoryear {Kaufmann{\index {Kaufmann, Matt (*1952)}} \bgroup \&al.\egroup }{2000b}}
\bibcite{KB70}{\citeauthoryear {Knuth \bgroup \&\ \egroup Bendix}{1970}}
\citation{leech-1970}
\bibcite{eighthECAIeightyeight}{\citeauthoryear {Kodratoff}{1988}}
\bibcite{thirteenthICALPeightysix}{\citeauthoryear {Kott}{1986}}
\bibcite{Kow74}{\citeauthoryear {Kowalski{\index {Kowalski, Robert A. (*1941)}}}{1974}}
\citation{IFIP-1974}
\bibcite{kowalski-1988}{\citeauthoryear {Kowalski{\index {Kowalski, Robert A. (*1941)}}}{1988}}
\bibcite{dritter-mathematiker}{\citeauthoryear {Krazer}{1905}}
\bibcite{induction-no-cut}{\citeauthoryear {Kreisel}{1965}}
\citation{saaty}
\bibcite{inductionlesshistd}{\citeauthoryear {K{\"u}chlin}{1989}}
\citation{kaci-nivat}
\bibcite{kuehler-master}{\citeauthoryear {K{\"u}hler{\index {Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}}}{1991}}
\bibcite{kuehlerdiss}{\citeauthoryear {K{\"u}hler{\index {Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}}}{2000}}
\bibcite{kwspec}{\citeauthoryear {K{\"u}hler{\index {Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}} \bgroup \&\ \egroup Wirth{\index {Wirth, Claus-Peter (*1963)}}}{1996}}
\citation{kwspec2}
\bibcite{kwspec2}{\citeauthoryear {K{\"u}hler{\index {Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}} \bgroup \&\ \egroup Wirth{\index {Wirth, Claus-Peter (*1963)}}}{1997}}
\citation{eighthRTAninetyseven}
\citation{kwspec}
\bibcite{lambert-1764}{\citeauthoryear {Lambert}{1764}}
\bibcite{inductionlessinduction1}{\citeauthoryear {Lankford}{1980}}
\bibcite{inductionlessinduction2}{\citeauthoryear {Lankford}{1981}}
\bibcite{honor-robinson}{\citeauthoryear {Lassez \bgroup \&\ \egroup Plotkin}{1991}}
\bibcite{leech-1970}{\citeauthoryear {Leech}{1970}}
\bibcite{handbook-tcs}{\citeauthoryear {Leeuwen}{1990}}
\bibcite{lics1}{\citeauthoryear {LICS}{1986}}
\bibcite{lics3}{\citeauthoryear {LICS}{1988}}
\bibcite{lics22}{\citeauthoryear {LICS}{2007}}
\bibcite{loechner-lpo}{\citeauthoryear {L{\unprotectedoe }chner{\index {Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}}}{2006}}
\bibcite{ninthCADEeightyeight}{\citeauthoryear {Lusk \bgroup \&\ \egroup Overbeek}{1988}}
\bibcite{fermat-career}{\citeauthoryear {Mahoney}{1994}}
\bibcite{smith-pieri}{\citeauthoryear {Marchisotto \bgroup \&\ \egroup Smit{\index {Smith, James T.}}h}{2007}}
\bibcite{Kolloquium-Programmiersprachen-und-Grundlagen-der-Programmierung}{\citeauthoryear {Margaria}{1995}}
\bibcite{LISP}{\citeauthoryear {McCarthy \bgroup \&al.\egroup }{1965}}
\bibcite{thirteenthCADEninetysix}{\citeauthoryear {McRobbie \bgroup \&\ \egroup Slaney}{1996}}
\bibcite{proof_planning_with_multiple_strategies}{\citeauthoryear {Melis \bgroup \&al.\egroup }{2008}}
\bibcite{meltzer-1975}{\citeauthoryear {Meltzer{\index {Meltzer, Bernard (1916(?)--2008)}}}{1975}}
\bibcite{machine-intelligence-7}{\citeauthoryear {Meltzer{\index {Meltzer, Bernard (1916(?)--2008)}} \bgroup \&\ \egroup Michie{\index {Michie, Donald (1923--2007)}}}{1972}}
\bibcite{machine-intelligence-3}{\citeauthoryear {Michie{\index {Michie, Donald (1923--2007)}}}{1968}}
\bibcite{milner-1972}{\citeauthoryear {Milner}{1972}}
\bibcite{moore-1973}{\citeauthoryear {Moore{\mooreindex }}{1973}}
\bibcite{moore-1975}{\citeauthoryear {Moore{\mooreindex }}{1975a}}
\citation{moore-1975-short}
\bibcite{moore-1975-short}{\citeauthoryear {Moore{\mooreindex }}{1975b}}
\citation{moore-1975}
\bibcite{moore-1979}{\citeauthoryear {Moore{\mooreindex }}{1979}}
\bibcite{moore-1981}{\citeauthoryear {Moore{\mooreindex }}{1981}}
\bibcite{moore-1989-2}{\citeauthoryear {Moore{\mooreindex }}{1989a}}
\bibcite{moore-1989-1}{\citeauthoryear {Moore{\mooreindex }}{1989b}}
\bibcite{moore-lynch-kaufmann-1998}{\citeauthoryear {Moore{\mooreindex } \bgroup \&al.\egroup }{1998}}
\bibcite{chaff}{\citeauthoryear {Moskewicz \bgroup \&al.\egroup }{2001}}
\citation{dac/2001}
\bibcite{musserinductionlessinduction}{\citeauthoryear {Musser}{1980}}
\citation{seventhPOPLeighty}
\bibcite{ijcai3}{\citeauthoryear {Nilsson}{1973}}
\bibcite{odifreddi}{\citeauthoryear {Odifreddi}{1990}}
\bibcite{padawitzjsc}{\citeauthoryear {Padawitz}{1996}}
\bibcite{padoa-1913}{\citeauthoryear {Padoa{\index {Padoa, Alessandro (1868--1937)}}}{1913}}
\citation{5-int-congress-mathematicians-1912}
\bibcite{pascal}{\citeauthoryear {Pascal}{1954}}
\bibcite{isabellesevenhundred}{\citeauthoryear {Paulson}{1990}}
\citation{odifreddi}
\bibcite{Pau96}{\citeauthoryear {Paulson}{1996}}
\bibcite{peanonovamethodo}{\citeauthoryear {Peano{\peanoindex }}{1889}}
\bibcite{peter-1951}{\citeauthoryear {P{\'e}ter{\index {P\'eter, R\'osza (1905--1977)}}}{1951}}
\bibcite{pieri}{\citeauthoryear {Pieri{\pieriindex }}{1908}}
\citation{smith-pieri}
\bibcite{honorrobinmilner}{\citeauthoryear {Plotkin \bgroup \&al.\egroup }{2000}}
\bibcite{presburger}{\citeauthoryear {Presburger{\presburgerindex }}{1930}}
\citation{presburger-remarks-translation}
\bibcite{protzenlazy}{\citeauthoryear {Protzen{\index {Protzen, Martin (*1962)}}}{1994}}
\citation{twelvethCADEninetyfour}
\bibcite{protzendiss}{\citeauthoryear {Protzen{\index {Protzen, Martin (*1962)}}}{1995}}
\bibcite{protzenpatching}{\citeauthoryear {Protzen{\index {Protzen, Martin (*1962)}}}{1996}}
\citation{thirteenthCADEninetysix}
\bibcite{Ravinovitch-Gershon}{\citeauthoryear {Rabinovitch}{1970}}
\bibcite{ijcai5}{\citeauthoryear {Reddy}{1977}}
\bibcite{reddy}{\citeauthoryear {Reddy}{1990}}
\citation{tenthCADEninety}
\bibcite{vampire01}{\citeauthoryear {Riazanov \bgroup \&\ \egroup Voronkov}{2001}}
\citation{firstIJCARone}
\bibcite{HandbookAR}{\citeauthoryear {Robinson{\index {Robinson, J. Alan (*1930(?))}} \bgroup \&\ \egroup Voronkow}{2001}}
\bibcite{IFIP-1974}{\citeauthoryear {Rosenfeld}{1974}}
\bibcite{waterfallfirst}{\citeauthoryear {Royce}{1970}}
\citation{ieeeweston70}
\bibcite{axiomofchoice}{\citeauthoryear {Rubin{\index {Rubin, Herman (*1926)}} \bgroup \&\ \egroup Rubin{\index {Rubin, Jean E. (1926--2002)}}}{1985}}
\bibcite{thirdCTRSninetytwo}{\citeauthoryear {Rusinowitch \bgroup \&\ \egroup Remy}{1993}}
\bibcite{russinoff-1998}{\citeauthoryear {Russinoff}{1998}}
\bibcite{saaty}{\citeauthoryear {Saaty}{1965}}
\bibcite{samoacalculemus}{\citeauthoryear {Schmidt-Samoa{\index {Schmidt-Samoa, Tobias (*1973)}}}{2006a}}
\bibcite{samoa-phd}{\citeauthoryear {Schmidt-Samoa{\index {Schmidt-Samoa, Tobias (*1973)}}}{2006b}}
\bibcite{jancl}{\citeauthoryear {Schmidt-Samoa{\index {Schmidt-Samoa, Tobias (*1973)}}}{2006c}}
\bibcite{scott-LCF}{\citeauthoryear {Scott{\index {Scott, Dana S. (*1932)}}}{1993}}
\bibcite{shankar-1986}{\citeauthoryear {Shankar{\index {Shankar, Natarajan}}}{1986}}
\citation{shankar-1994}
\bibcite{church-rosser-bm}{\citeauthoryear {Shankar{\index {Shankar, Natarajan}}}{1988}}
\citation{shankar-1994}
\bibcite{shankar-1994}{\citeauthoryear {Shankar{\index {Shankar, Natarajan}}}{1994}}
\citation{shankar-1986}
\bibcite{course-of-values-induction}{\citeauthoryear {Shepherdson}{1969}}
\bibcite{Shoenfield67}{\citeauthoryear {Shoenfield{\index {Shoenfield, Joseph R. (1927--2000)}}}{1967}}
\bibcite{eighthCADEeightysix}{\citeauthoryear {Siek{\discretionary {-}{}{}}mann{\siekmannindex }}{1986}}
\bibcite{ijcai11}{\citeauthoryear {Sridharan}{1989}}
\bibcite{presburger-remarks-translation}{\citeauthoryear {Stansifer}{1984}}
\bibcite{commonlisp}{\citeauthoryear {Steele}{1990}}
\bibcite{SR--88--12}{\citeauthoryear {Steinbach}{1988}}
\bibcite{simplificationorderings}{\citeauthoryear {Steinbach}{1995}}
\bibcite{stevens-rational-reconstruction}{\citeauthoryear {Stevens}{1988}}
\citation{eighthECAIeightyeight}
\bibcite{tenthCADEninety}{\citeauthoryear {Stickel}{1990}}
\bibcite{gwai9}{\citeauthoryear {Stoyan}{1985}}
\bibcite{toyama}{\citeauthoryear {Toyama}{1988}}
\citation{future-generation}
\citation{toyamadiss}
\bibcite{toyamadiss}{\citeauthoryear {Toyama}{1990}}
\bibcite{unguru-one}{\citeauthoryear {Unguru}{1991}}
\bibcite{simonyi-interview}{\citeauthoryear {Verma}{2005?}}
\bibcite{voicu-li-di}{\citeauthoryear {Voicu \bgroup \&\ \egroup Li}{2009}}
\citation{Coq1}
\bibcite{thirdLPARninetytwo}{\citeauthoryear {Voronkov}{1992}}
\bibcite{eightteenthCADEtwo}{\citeauthoryear {Voronkov}{2002}}
\bibcite{walthertermination}{\citeauthoryear {Walther{\index {Walther, Christoph (*1950)}}}{1988}}
\citation{ninthCADEeightyeight}
\bibcite{waltherLPAR92}{\citeauthoryear {Walther{\index {Walther, Christoph (*1950)}}}{1992}}
\citation{thirdLPARninetytwo}
\bibcite{waltherIJCAI93}{\citeauthoryear {Walther{\index {Walther, Christoph (*1950)}}}{1993}}
\citation{ijcai13}
\bibcite{waltherhandbook}{\citeauthoryear {Walther{\index {Walther, Christoph (*1950)}}}{1994a}}
\citation{handbooklogicailpvol2}
\bibcite{walthertermination2}{\citeauthoryear {Walther{\index {Walther, Christoph (*1950)}}}{1994b}}
\bibcite{fifthAMASTninetysix}{\citeauthoryear {Wirsing \bgroup \&\ \egroup Nivat}{1996}}
\bibcite{wirth-master}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{1991}}
\bibcite{wirthdiss}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{1997}}
\bibcite{wirthcardinal}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2004}}
\bibcite{zombie}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2005a}}
\citation{siekmann-60}
\bibcite{wirthconfluence}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2005b}}
\bibcite{wirth-jsc}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2009}}
\bibcite{swp200601}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2010a}}
\bibcite{fermatsproof}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2010b}}
\bibcite{wirth-heijenoort}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2012a}}
\bibcite{wirth-jsc-non-permut}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2012b}}
\bibcite{wirth-manifesto-ljigpl}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2012c}}
\bibcite{boyer-moore-2012}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2012d}}
\bibcite{SR--2011--01}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2015}}
\bibcite{wirthbecker}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} \bgroup \&\ \egroup Becker}{1995}}
\citation{fourthCTRSninetyfour}
\bibcite{wgjsc}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} \bgroup \&\ \egroup Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (1959--2014)}}ch}{1994a}}
\bibcite{wgcade}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} \bgroup \&\ \egroup Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (1959--2014)}}ch}{1994b}}
\citation{twelvethCADEninetyfour}
\bibcite{wgkp}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} \bgroup \&al.\egroup }{1993}}
\citation{wgjsc}
\citation{wgcade}
\bibcite{SR--95--15}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} \bgroup \&\ \egroup K{\"u}hler{\index {Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}}}{1995}}
\bibcite{herbrand-handbook}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} \bgroup \&al.\egroup }{2009}}
\citation{handbook-of-the-history-of-logic}
\bibcite{wirth-pascal}{\citeauthoryear {Wirth}{1971}}
\bibcite{wolff-rationalis}{\citeauthoryear {Wolff}{1728}}
\bibcite{wolff-rationalis-1740}{\citeauthoryear {Wolff}{1740}}
\citation{wolff-rationalis}
\bibcite{secondICSEseventysix}{\citeauthoryear {Yeh \bgroup \&\ \egroup Ramamoorthy}{1976}}
\bibcite{young-1989}{\citeauthoryear {Young}{1989}}
\bibcite{ZKK88}{\citeauthoryear {Zhang \bgroup \&al.\egroup }{1988}}
\citation{ninthCADEeightyeight}
\bibcite{presburger-life}{\citeauthoryear {Zygmunt}{1991}}
\@writefile{toc}{\contentsline {section}{Index}{108}}