\relax 
\bibstyle{named}
\citation{vampire01}
\citation{waldmeister}
\citation{HL02}
\citation{chaff}
\citation{C26}
\citation{satallax}
\newlabel{1-fp}{{1}{1}}
\@writefile{toc}{\contentsline {Chapter}{{\unhbox \voidb@x \hbox {\MakeTextUppercase  {{{J\nobreakspace  {}Strother {Moore}}, {Clau\unprotectedes -Peter\ {Wirth}}}}}\\ {{Automation\nobreakspace  {}of Mathematical\nobreakspace  {}Induction as\nobreakspace  {}part\nobreakspace  {}of\nobreakspace  {}the\nobreakspace  {}History\nobreakspace  {}of\nobreakspace  {}Logic}}}}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}\MakeTextUppercase  {A Snapshot of a Decisive Moment in History}}{1}}
\@writefile{ptc1}{\contentsline {Psection}{\numberline {1}A Snapshot of a Decisive Moment in History}{1}}
\newlabel{section Preface}{{1}{1}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces The {Boyer}--{Moore}\ Waterfall}}{1}}
\newlabel{figure waterfall}{{1}{1}}
\newlabel{note higher-order theorem provers}{{3}{1}}
\citation{waterfall}
\citation{bm}
\citation{moore-1973}
\citation{boyer-moore-1973}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces {Ro\discretionary {-}{}{}bert\ S. {Boyer}}\ (1971) (l.)\ and {J\nobreakspace  {}Strother {Moore}}\ (1972?) (r.)}}{2}}
\citation{meltzer-1975}
\citation{kowalski-1988}
\newlabel{note people and departments}{{7}{3}}
\citation{boyer-moore-1971}
\citation{moore-1973}
\citation{moore-1973}
\citation{Kow74}
\citation{Kow74}
\citation{kowalski-1988}
\citation{Prolog}
\citation{pop2}
\citation{boyer-moore-davies-1973}
\citation{moore-1981}
\citation{simonyi-interview}
\citation{waltherhandbook}
\citation{bundy-survey}
\@writefile{toc}{\contentsline {section}{\numberline {2}\MakeTextUppercase  {Method of Procedure and Presentation}}{5}}
\@writefile{ptc1}{\contentsline {Psection}{\numberline {2}Method of Procedure and Presentation}{5}}
\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}\MakeTextUppercase  {Organization of this Article}}{8}}
\@writefile{ptc1}{\contentsline {Psection}{\numberline {3}Organization of this Article}{8}}
\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}
\@writefile{toc}{\contentsline {section}{\numberline {4}\MakeTextUppercase  {Mathematical Induction}}{9}}
\@writefile{ptc1}{\contentsline {Psection}{\numberline {4}Mathematical Induction}{9}}
\newlabel{section What is mathematical induction?}{{4}{9}}
\citation{fermat-birth-date}
\citation{catherine-goldstein-fermat-priceton-companion-math-2008}
\citation{fermatsproof}
\citation{wirthcardinal}
\citation{wirthcardinal}
\citation{axiomofchoice}
\citation{weakaxiomofchoice}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}Well-Founded\discretionary {-}{}{}ness\ and Termination}{10}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.1}Well-Founded\discretionary {-}{}{}ness\ and Termination}{10}}
\newlabel{subsection Well-Foundedness and Termination}{{4.1}{10}}
\newlabel{lemma 1}{{1}{10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}The Theorem of\/ {Noether}\discretionary {-}{}{}ian\ Induction}{10}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.2}The Theorem of\/ {Noether}\discretionary {-}{}{}ian\ Induction}{10}}
\newlabel{subsection noetherian induction}{{4.2}{10}}
\citation{cohn-1965}
\citation{bourbaki-english}
\citation{bourbaki-set-theory-chapter-3-2nd-edn}
\citation{schoenfield}
\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}
\citation{geseraxiomofchoice}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}An Induction Principle Stronger than {Noether}\discretionary {-}{}{}ian\ Induction?}{11}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.3}An Induction Principle Stronger than {Noether}\discretionary {-}{}{}ian\ Induction?}{11}}
\newlabel{subsection Beyond Noetherian induction}{{4.3}{11}}
\newlabel{note complete induction}{{34}{11}}
\citation{geseraxiomofchoice}
\citation{axiomofchoice}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}The Natural Numbers}{12}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.4}The Natural Numbers}{12}}
\newlabel{subsection Mathematical Induction and the Natural Numbers}{{4.4}{12}}
\citation{dedekind-1888}
\citation{wolff-rationalis-1740}
\citation{lambert-1764}
\citation{fries-vollstaendige-induction}
\citation{heijenoort-source-book}
\citation{grundlagen-german-english-edition-volume-one-one}
\citation{peter-1951}
\citation{ackermann-1928a}
\newlabel{note fries}{{38}{13}}
\citation{wirthcardinal}
\citation{pieri}
\citation{pieri}
\citation{peanonovamethodo}
\citation{padoa-1913}
\citation{smith-pieri}
\citation{pieri}
\citation{pieri}
\newlabel{note pieri standard}{{42}{14}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.5}Standard Data Types}{15}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.5}Standard Data Types}{15}}
\newlabel{subsection Standard Data Types}{{4.5}{15}}
\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}{18}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.6}The Standard High-Level Method of Mathematical Induction}{18}}
\newlabel{subsection The Standard High-Level Method of Mathematical Induction}{{4.6}{18}}
\newlabel{section items}{{4.6}{18}}
\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}{\it  Descente Infinie}}{19}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.7}{\it  Descente Infinie}}{19}}
\newlabel{subsection DescenteInfinie}{{4.7}{19}}
\citation{sergetableau}
\newlabel{section example first proof of (+3)}{{4.7}{20}}
\newlabel{example first proof of (+3)}{{2}{20}}
\newlabel{section example first proof of (less7)}{{4.7}{21}}
\newlabel{example first proof of (less7)}{{3}{21}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.8}Explicit Induction}{22}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.8}Explicit Induction}{22}}
\newlabel{subsection Explicit Induction}{{4.8}{22}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.8.1}From the Theorem of\/ {Noether}\discretionary {-}{}{}ian\ Induction\ to Explicit Induction}{22}}
\newlabel{section example second proof of (+3)}{{4.8.1}{23}}
\newlabel{example second proof of (+3)}{{4}{23}}
\citation{waltherIJCAI93}
\citation{wirthcardinal}
\citation{church-rosser-bm}
\citation{church-rosser-bm}
\citation{lambda-calculus-final}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.8.2}Theoretical Viewpoint on Explicit Induction}{25}}
\newlabel{subsubsection Theoretical Viewpoint}{{4.8.2}{25}}
\newlabel{note Newman}{{64}{25}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {4.8.3}Practical Viewpoint on Explicit Induction}{26}}
\newlabel{subsubsection Practical Viewpoint}{{4.8.3}{26}}
\citation{aubin-1976}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.9}Generalization}{27}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.9}Generalization}{27}}
\newlabel{subsection Generalization}{{4.9}{27}}
\newlabel{section example proof of (ack4)}{{4.9}{27}}
\citation{wirthcardinal}
\newlabel{example proof of (ack4)}{{5}{28}}
\citation{goedel}
\citation{gentzen}
\citation{induction-no-cut}
\citation{baazleitschcolllog}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.10}Proof-Theoretical Peculiarities of Mathematical Induction}{29}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.10}Proof-Theoretical Peculiarities of Mathematical Induction}{29}}
\newlabel{subsection Proof-Theoretical Peculiarities of Mathematical Induction}{{4.10}{29}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.11}Conclusion}{29}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {4.11}Conclusion}{29}}
\newlabel{note practice one}{{72}{29}}
\newlabel{note practice two}{{75}{29}}
\citation{wirth-jsc}
\@writefile{toc}{\contentsline {section}{\numberline {5}\MakeTextUppercase  {Recursion, Termination, and Induction}}{30}}
\@writefile{ptc1}{\contentsline {Psection}{\numberline {5}Recursion, Termination, and Induction}{30}}
\newlabel{section Recursive Definitions}{{5}{30}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}Recursion and the Rewrite Relation on Ground Terms}{30}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {5.1}Recursion and the Rewrite Relation on Ground Terms}{30}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}Confluence}{30}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {5.2}Confluence}{30}}
\newlabel{subsection Confluence}{{5.2}{30}}
\citation{bm}
\citation{moore-1973}
\citation{bm}
\citation{LISP}
\citation{bm}
\newlabel{section example PLUS}{{5.2}{31}}
\newlabel{example PLUS}{{6}{31}}
\newlabel{note applicative}{{81}{31}}
\citation{wirth-jsc}
\citation{wirth-jsc}
\citation{bm}
\citation{wgcade}
\citation{wirth-jsc}
\citation{schoenfield}
\citation{moore-1973}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}Termination and Reducibility}{32}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {5.3}Termination and Reducibility}{32}}
\newlabel{subsection Termination and Reducibility}{{5.3}{32}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.4}Constructor Variables}{32}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {5.4}Constructor Variables}{32}}
\newlabel{subsection Constructor Variables}{{5.4}{32}}
\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}
\citation{bm}
\citation{bm}
\citation{waltherLPAR92}
\citation{waltherLPAR92}
\citation{waltherIJCAI93}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.5}Termination and General Induction Templates}{34}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {5.5}Termination and General Induction Templates}{34}}
\newlabel{subsection Termination}{{5.5}{34}}
\newlabel{note on IF and COND}{{89}{34}}
\newlabel{example induction template two measured subsets constructor style}{{7}{35}}
\newlabel{example non-singleton measured subset constructor style}{{8}{35}}
\citation{wirthdiss}
\citation{wirth-jsc}
\citation{wirthdiss}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.6}Termination of the Rewrite Relation on Ground Terms}{36}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {5.6}Termination of the Rewrite Relation on Ground Terms}{36}}
\newlabel{note on general variables}{{94}{36}}
\citation{mutualexplicitinduction}
\citation{bm}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.7}Applicable Induction Templates for Explicit Induction}{37}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {5.7}Applicable Induction Templates for Explicit Induction}{37}}
\newlabel{section example Applicable Induction Templates constructor style}{{5.7}{38}}
\newlabel{example Applicable Induction Templates constructor style}{{9}{38}}
\@writefile{toc}{\contentsline {subsection}{\numberline {5.8}Induction Schemes}{38}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {5.8}Induction Schemes}{38}}
\newlabel{subsection Induction Schemes}{{5.8}{38}}
\citation{bm}
\citation{fitting}
\citation{Fitting90}
\citation{wirthcardinal}
\citation{wirthcardinal}
\citation{wirth-jsc-non-permut}
\citation{SR--2011--01}
\newlabel{section example induction schemes constructor style}{{5.8}{40}}
\newlabel{example induction schemes constructor style}{{10}{40}}
\citation{davis-2009}
\@writefile{toc}{\contentsline {section}{\numberline {6}\MakeTextUppercase  {Automated Explicit Induction}}{41}}
\@writefile{ptc1}{\contentsline {Psection}{\numberline {6}Automated Explicit Induction}{41}}
\newlabel{section Explicit Induction}{{6}{41}}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.1}The Application Context of Automated Explicit Induction}{41}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {6.1}The Application Context of Automated Explicit Induction}{41}}
\newlabel{subsection The Application Context of Automated Explicit Induction}{{6.1}{41}}
\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}}{42}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {6.2}The\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{42}}
\newlabel{The Pure Lisp Theorem Prover}{{6.2}{42}}
\newlabel{note burstall quotation}{{102}{42}}
\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}}{45}}
\newlabel{subsubsection Simplification in the pure}{{6.2.1}{45}}
\citation{moore-1973}
\citation{samoa-phd}
\citation{samoa-phd}
\citation{jancl}
\newlabel{note no destructor elimination}{{119}{47}}
\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}}{48}}
\newlabel{subsubsection Destructor Elimination in the PURE}{{6.2.2}{48}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.3}(Cross-) Fertilization in the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{48}}
\newlabel{fertilization in pure lisp theorem prover}{{6.2.3}{48}}
\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}}{49}}
\newlabel{subsubsection Generalization pure lisp theorem prover}{{6.2.4}{49}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.5}Elimination of Irrelevance in the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.6}Induction in the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{49}}
\newlabel{subsubsection Induction of pure lisp theorem prover}{{6.2.6}{49}}
\newlabel{note failure of synthesis}{{122}{49}}
\citation{moore-1973}
\newlabel{section example induction rule}{{6.2.6}{50}}
\newlabel{example induction rule}{{11}{50}}
\newlabel{section example merging}{{6.2.6}{51}}
\newlabel{section example second proof of (less7)}{{6.2.6}{51}}
\newlabel{example second proof of (less7)}{{12}{51}}
\newlabel{example merging}{{12}{51}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.2.7}Conclusion on the\/ {\sc  Pure {\sc  LISP}\ Theo\discretionary {-}{}{}rem Pro\discretionary {-}{}{}ver}}{51}}
\newlabel{subsubsection Conclusion on the pure lisp theorem prover}{{6.2.7}{51}}
\citation{moore-1973}
\citation{bm}
\citation{bm}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.3}{\sc  Thm}}{52}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {6.3}{\sc  Thm}}{52}}
\newlabel{subsection theorem prover}{{6.3}{52}}
\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}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{bm}
\citation{wirth-pascal}
\citation{bm}
\citation{bm}
\citation{boyermoore}
\citation{boyermooresecondedition}
\newlabel{note jargon one}{{134}{54}}
\citation{bm}
\citation{boyermoore}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{bm}
\citation{boyermoore}
\citation{boyermoore}
\citation{boyermooresecondedition}
\newlabel{note PACK}{{135}{55}}
\citation{bm}
\citation{bm}
\citation{bm}
\citation{bm}
\citation{bm}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.1}Simplification in\/ {\sc  Thm}}{57}}
\newlabel{subsubsection simplification in}{{6.3.1}{57}}
\newlabel{note kaufmann non-standard}{{139}{57}}
\citation{bm}
\citation{bm}
\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}}{61}}
\newlabel{subsubsection Destructor Elimination in}{{6.3.2}{61}}
\newlabel{example and back}{{15}{61}}
\citation{bm}
\citation{bm}
\newlabel{example d l once}{{16}{62}}
\citation{bm}
\newlabel{example quotient and remainder}{{17}{63}}
\citation{bm}
\citation{bm}
\citation{bm}
\citation{bm}
\citation{bm}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.3}(Cross-) Fertilization in\/ {\sc  Thm}}{65}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.4}Generalization in\/ {\sc  Thm}}{65}}
\citation{bm}
\citation{wirthcardinal}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.5}Elimination of Irrelevance in\/ {\sc  Thm}}{66}}
\newlabel{subsubsection Elimination of Irrelevance in}{{6.3.5}{66}}
\@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}}{67}}
\newlabel{subsubsection Induction in}{{6.3.6}{67}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.7}Induction Templates generated by Definition-Time Recursion Analysis}{67}}
\newlabel{subsubsection Induction Templates}{{6.3.7}{67}}
\citation{bm}
\citation{bm}
\citation{bm}
\newlabel{section example induction template two measured subsets}{{6.3.7}{68}}
\newlabel{example induction template two measured subsets}{{18}{68}}
\newlabel{example non-singleton measured subset}{{19}{68}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.3.8}Proof-Time Recursion Analysis in\/ {\sc  Thm}}{69}}
\newlabel{subsubsection Proof-Time Recursion Analysis in}{{6.3.8}{69}}
\newlabel{example Applicable Induction Templates}{{20}{69}}
\newlabel{example induction schemes}{{21}{69}}
\citation{bm}
\newlabel{example Subsumption}{{22}{70}}
\newlabel{note injectivity 1}{{168}{70}}
\newlabel{section example merging 2}{{6.3.8}{71}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces \footroom The induction schemes of Ex\discretionary {-}{}{}am\discretionary {-}{}{}ple\,23\hbox {}}}{71}}
\newlabel{figure induction schemes}{{3}{71}}
\citation{bm}
\citation{bm}
\citation{bm}
\newlabel{example merging 2}{{23}{72}}
\newlabel{note injectivity 2}{{169}{72}}
\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}}{73}}
\newlabel{subsubsection Conclusion on}{{6.3.9}{73}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces Four possibilities to descend with rational representations of \nlbmath {\sqrt  2}:}}{74}}
\newlabel{figure square root}{{4}{74}}
\citation{bm}
\citation{boyer-moore-1981-authors}
\citation{bmeval-1988}
\citation{boyermoore}
\citation{boyermoore}
\citation{boyermooresecondedition}
\citation{presburger}
\citation{presburger-remarks-translation}
\citation{presburger-life}
\citation{boyer-moore-1988}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.4}{\sc  Nqthm}}{75}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {6.4}{\sc  Nqthm}}{75}}
\newlabel{subsection NQTHM}{{6.4}{75}}
\newlabel{note presburger}{{175}{75}}
\citation{hunt-1985}
\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{boyermooresecondedition}
\citation{boyermoore}
\citation{commonlisp}
\@writefile{toc}{\contentsline {subsection}{\numberline {6.5}{\sc  ACL2}}{76}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {6.5}{\sc  ACL2}}{76}}
\newlabel{subsection ACLTWO}{{6.5}{76}}
\newlabel{note shankar}{{176}{76}}
\citation{boyermooresecondedition}
\citation{ACLTWO}
\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{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}{78}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {6.6}Further Historically Important Explicit-Induction Systems}{78}}
\newlabel{subsection Further Most Noteworthy Explicit-Induction Systems}{{6.6}{78}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.6.1}{\sc  Rrl}}{78}}
\newlabel{section RRL}{{6.6.1}{78}}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.6.2}{\sc  Inka}}{78}}
\newlabel{section INKA}{{6.6.2}{78}}
\citation{inkafuenf}
\citation{inka}
\citation{inkanext}
\citation{inkafuenf}
\citation{inductioncontest}
\citation{bm}
\citation{inkafuenf}
\citation{bm}
\citation{inka}
\citation{inkanext}
\citation{oysterclam}
\citation{bundy-survey}
\citation{nuprl-book}
\@writefile{toc}{\contentsline {subsubsection}{\numberline {6.6.3}{\sc  Oyster}/{\rm  CL\kern -.36em\raise .39ex\hbox {\sc  a}\kern -.15emM}}{79}}
\newlabel{note induction contest}{{180}{79}}
\citation{failure-guide-induction}
\citation{bundy-recursion-analysis}
\citation{bundy-survey}
\citation{science-of-reasoning}
\citation{bundy-inductive-proof-planning}
\citation{proofplanningsystems}
\@writefile{toc}{\contentsline {section}{\numberline {7}\MakeTextUppercase  {Alternative Approaches Besides Explicit Induction}}{80}}
\@writefile{ptc1}{\contentsline {Psection}{\numberline {7}Alternative Approaches Besides Explicit Induction}{80}}
\newlabel{section Alternative Approaches to the Automation of Induction}{{7}{80}}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.1}Proof Planning}{80}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {7.1}Proof Planning}{80}}
\newlabel{subsection Proof Planning}{{7.1}{80}}
\citation{science-of-reasoning}
\citation{science-of-reasoning}
\citation{bundy-inductive-proof-planning}
\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{aubin-1976}
\citation{aubin-1976}
\citation{rippling-book}
\citation{aubin-1976}
\citation{aubin-1976}
\citation{aubin-1979}
\citation{rippling-book}
\citation{hutter-rippling}
\citation{rippling}
\citation{failure-guide-induction}
\citation{rippling-calculus}
\citation{failure-guide-induction}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.2}Rippling}{81}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {7.2}Rippling}{81}}
\newlabel{subsection Rippling}{{7.2}{81}}
\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}
\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}
\@writefile{toc}{\contentsline {subsection}{\numberline {7.3}Implicit Induction}{82}}
\@writefile{ptc1}{\contentsline {Psubsection}{\numberline {7.3}Implicit Induction}{82}}
\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}}
\@writefile{ptc1}{\contentsline {Psubsection}{\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}\MakeTextUppercase  {Lessons Learned}}{88}}
\@writefile{ptc1}{\contentsline {Psection}{\numberline {8}Lessons Learned}{88}}
\newlabel{section Lessons Learned}{{8}{88}}
\citation{boyer-moore-2012}
\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}\MakeTextUppercase  {Conclusion}}{89}}
\@writefile{ptc1}{\contentsline {Psection}{\numberline {9}Conclusion}{89}}
\newlabel{section Conclusion}{{9}{89}}
\bibdata{herbrandbib}
\bibcite{seventhPOPLeighty}{\citeauthoryear {Abrahams \bgroup \em  et 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 and Nivat}{1989}}
\bibcite{aamp7g-2005}{\citeauthoryear {Anon}{2005}}
\bibcite{fourthIJCAReight}{\citeauthoryear {Armando \bgroup \em  et 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{inkafuenf}{\citeauthoryear {Autexier{\index {Autexier, Serge (*1971)}} \bgroup \em  et al.\egroup }{1999}}
\citation{sixteenthCADEninetynine}
\bibcite{sergetableau}{\citeauthoryear {Autexier{\index {Autexier, Serge (*1971)}}}{2005}}
\citation{fourteenthTABLEAUfive}
\bibcite{quodlibet-cade}{\citeauthoryear {Avenhaus \bgroup \em  et al.\egroup }{2003}}
\citation{nineteenthCADEthree}
\bibcite{nineteenthCADEthree}{\citeauthoryear {Baader}{2003}}
\bibcite{baazleitschcolllog}{\citeauthoryear {Baaz and Leitsch}{1995}}
\bibcite{Hotz-Festschrift}{\citeauthoryear {Bachmair \bgroup \em  et al.\egroup }{1992}}
\bibcite{bachmair}{\citeauthoryear {Bachmair}{1988}}
\citation{lics3}
\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}
\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 and Walsh}{1996}}
\bibcite{becker-griechische}{\citeauthoryear {Becker}{1965}}
\bibcite{fourteenthTABLEAUfive}{\citeauthoryear {Beckert}{2005}}
\bibcite{waterfall}{\citeauthoryear {Bell and Thayer}{1976}}
\citation{secondICSEseventysix}
\bibcite{C26}{\citeauthoryear {Benz{\discretionary {-}{}{}}m{\unprotectedue }ller{\index {Benzmueller, Christoph (*1968)@{Benzm\"uller, Christoph\ (*1968)}}} \bgroup \em  et al.\egroup }{2008}}
\citation{fourthIJCAReight}
\bibcite{logiktexte}{\citeauthoryear {Berka and Kreiser}{1973}}
\bibcite{bevers&lewi}{\citeauthoryear {Bevers and Lewi}{1990}}
\citation{secondCTRSninety}
\bibcite{cli-1989-1}{\citeauthoryear {Bevier \bgroup \em  et al.\egroup }{1989}}
\bibcite{bevier-1989}{\citeauthoryear {Bevier}{1989}}
\bibcite{fifthCADEeighty}{\citeauthoryear {Bibel and Kowalski{\index {Kowalski, Robert A. (*1941)}}}{1980}}
\bibcite{inka}{\citeauthoryear {Biundo \bgroup \em  et al.\egroup }{1986}}
\citation{eighthCADEeightysix}
\bibcite{after-25-years}{\citeauthoryear {Bledsoe{\bledsoeindex } and Loveland}{1984}}
\bibcite{BBH72-short}{\citeauthoryear {Bledsoe{\bledsoeindex } \bgroup \em  et al.\egroup }{1971}}
\citation{ijcai2}
\citation{BBH72}
\bibcite{BBH72}{\citeauthoryear {Bledsoe{\bledsoeindex } \bgroup \em  et al.\egroup }{1972}}
\citation{BBH72-short}
\bibcite{Ble71}{\citeauthoryear {Bledsoe{\bledsoeindex }}{1971}}
\bibcite{twentyfirstCAVnine}{\citeauthoryear {Bouajjani and Maler}{2009}}
\bibcite{spike}{\citeauthoryear {Bouhoula and 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{boyer-moore-1971}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1971}}
\citation{boyer-moore-1972}
\bibcite{boyer-moore-1972}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1972}}
\citation{machine-intelligence-7}
\bibcite{boyer-moore-1973}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1973}}
\citation{ijcai3}
\citation{boyer-moore-1975}
\bibcite{boyer-moore-1975}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1975}}
\citation{boyer-moore-1973}
\bibcite{boyer-moore-fast-string-searching}{\citeauthoryear {Boyer{\boyerindex \index {Boyer--Moore fast string searching algorithm}} and Moore{\mooreindex }}{1977a}}
\bibcite{boyer-moore-1977}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1977b}}
\citation{ijcai5}
\bibcite{bm}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1979}}
\bibcite{boyer-moore-1981-editors}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1981a}}
\bibcite{boyer-moore-1981-authors}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1981b}}
\citation{boyer-moore-1981-editors}
\bibcite{boyer-moore-turing-completeness-lisp}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1984a}}
\citation{after-25-years}
\bibcite{boyer-moore-halting-problem}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1984b}}
\bibcite{boyer-moore-proof-checking-RSA}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1984c}}
\bibcite{boyer-moore-1985}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1985}}
\bibcite{bmeval-1987}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1987}}
\citation{bmeval-1988}
\citation{bmeval-1988}
\citation{bmeval-1989}
\bibcite{bmeval-1988}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1988a}}
\citation{bmeval-1987}
\citation{bmeval-1987}
\citation{bmeval-1989}
\bibcite{boyermoore}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1988b}}
\citation{boyermooresecondedition}
\bibcite{boyer-moore-1988}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1988c}}
\citation{machine-intelligence-11}
\bibcite{bmeval-1989}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1989}}
\citation{broy-1989}
\citation{bmeval-1987}
\citation{bmeval-1987}
\citation{bmeval-1988}
\bibcite{BM90}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1990}}
\citation{tenthCADEninety}
\bibcite{boyermooresecondedition}{\citeauthoryear {Boyer{\boyerindex } and Moore{\mooreindex }}{1998}}
\citation{boyermoore}
\bibcite{boyer-yu-1992}{\citeauthoryear {Boyer{\boyerindex } and Yu}{1992}}
\citation{eleventhCADEninetytwo}
\bibcite{c-string-lib-1996}{\citeauthoryear {Boyer{\boyerindex } and Yu}{1996}}
\bibcite{boyer-moore-davies-1973}{\citeauthoryear {Boyer{\boyerindex } \bgroup \em  et al.\egroup }{1973}}
\bibcite{boyer-moore-shostak}{\citeauthoryear {Boyer{\boyerindex } \bgroup \em  et al.\egroup }{1976}}
\citation{thirdPOPLseventysix}
\bibcite{Boy71}{\citeauthoryear {Boyer{\boyerindex }}{1971}}
\bibcite{boyer-2012}{\citeauthoryear {Boyer{\boyerindex }}{2012}}
\bibcite{brock-hunt-1999}{\citeauthoryear {Brock and Hunt{\index {Hunt, Warren A.}}}{1999}}
\citation{industrial-strength-1999}
\bibcite{DBLP:conf/lics/BrotherstonS07}{\citeauthoryear {Brotherston and Simpson}{2007}}
\citation{lics22}
\citation{brotherston-cut-elimination}
\bibcite{brotherston-cut-elimination}{\citeauthoryear {Brotherston and Simpson}{2011}}
\citation{DBLP:conf/tableaux/Brotherston05}
\citation{DBLP:conf/lics/BrotherstonS07}
\bibcite{DBLP:conf/tableaux/Brotherston05}{\citeauthoryear {Brotherston}{2005}}
\citation{fourteenthTABLEAUfive}
\citation{brotherston-cut-elimination}
\bibcite{satallax}{\citeauthoryear {Brown}{2012}}
\citation{sixthIJCARtwelve}
\bibcite{broy-1989}{\citeauthoryear {Broy}{1989}}
\bibcite{waldmeister}{\citeauthoryear {Buch and Hillenbrand{\index {Hillenbrand, Thomas}}}{1996}}
\bibcite{bundy-recursion-analysis}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}} \bgroup \em  et al.\egroup }{1989}}
\citation{ijcai11}
\bibcite{oysterclam}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}} \bgroup \em  et al.\egroup }{1990}}
\citation{tenthCADEninety}
\bibcite{rippling}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}} \bgroup \em  et al.\egroup }{1991}}
\bibcite{rippling-book}{\citeauthoryear {Bundy{\index {Bundy, Alan (*1947)}} \bgroup \em  et al.\egroup }{2005}}
\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{pop2}{\citeauthoryear {Burstall{\index {Burstall, Rod M. (*1934)}} \bgroup \em  et al.\egroup }{1971}}
\bibcite{burstall-1969}{\citeauthoryear {Burstall{\index {Burstall, Rod M. (*1934)}}}{1969}}
\bibcite{maurolycus}{\citeauthoryear {Bussey}{1917}}
\bibcite{From-Fermat-to-Gauss}{\citeauthoryear {Bussotti}{2006}}
\bibcite{cajori-1918}{\citeauthoryear {Cajori}{1918}}
\bibcite{churchbourbaki}{\citeauthoryear {Church}{1946}}
\citation{bourbaki-set-theory-results-1st-edn}
\bibcite{Prolog}{\citeauthoryear {Clocksin and 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 \em  et 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 \em  et al.\egroup }{2005}}
\bibcite{term-rewriting-one}{\citeauthoryear {Dershowitz and Jouannaud}{1990}}
\citation{handbook-tcs}
\bibcite{fourthCTRSninetyfour}{\citeauthoryear {Dershowitz and Lindenstrauss}{1995}}
\bibcite{thirdRTAeightynine}{\citeauthoryear {Dershowitz}{1989}}
\bibcite{dodi-diss}{\citeauthoryear {Dietrich}{2011}}
\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}}
\bibcite{hippa}{\citeauthoryear {Fritz}{1945}}
\citation{becker-griechische}
\bibcite{future-generation}{\citeauthoryear {Fuchi and Kott}{1988}}
\bibcite{handbook-of-the-history-of-logic}{\citeauthoryear {Gabbay{\index {Gabbay, Dov (*1945)}} and Woods}{2004\unhbox \voidb@x \hbox {}{ff.}}}
\bibcite{handbooklogicailpvol2}{\citeauthoryear {Gabbay{\index {Gabbay, Dov (*1945)}} \bgroup \em  et al.\egroup }{1994}}
\bibcite{GaSt}{\citeauthoryear {Ganzinger and Stuber}{1992}}
\citation{Hotz-Festschrift}
\citation{thirdCTRSninetytwo}
\bibcite{seventhRTAninetysix}{\citeauthoryear {Ganzinger}{1996}}
\bibcite{sixteenthCADEninetynine}{\citeauthoryear {Ganzinger}{1999}}
\bibcite{gentzen}{\citeauthoryear {Gentzen}{1935}}
\citation{logiktexte}
\citation{gentzen-collected}
\bibcite{gentzen-collected}{\citeauthoryear {Gentzen}{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{fromLCFtoHOL}{\citeauthoryear {Gordon{\index {Gordon, Mike J. C. (*1948)}}}{2000}}
\citation{honorrobinmilner}
\bibcite{firstIJCARone}{\citeauthoryear {Gore \bgroup \em  et al.\egroup }{2001}}
\bibcite{priceton-companion-math-2008}{\citeauthoryear {Gowers \bgroup \em  et al.\egroup }{2008}}
\bibcite{thirdPOPLseventysix}{\citeauthoryear {Graham \bgroup \em  et al.\egroup }{1976}}
\bibcite{unicom}{\citeauthoryear {Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (*1959)}}ch and Lindner}{1991}}
\bibcite{gwrta}{\citeauthoryear {Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (*1959)}}ch and Wirth{\index {Wirth, Claus-Peter (*1963)}}}{1996}}
\citation{seventhRTAninetysix}
\bibcite{sixthIJCARtwelve}{\citeauthoryear {Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (*1959)}}ch \bgroup \em  et al.\egroup }{2012}}
\bibcite{machine-intelligence-11}{\citeauthoryear {Hayes \bgroup \em  et al.\egroup }{1988}}
\bibcite{heijenoort-source-book}{\citeauthoryear {Heijenoort{\heijenoortindex }}{1971}}
\bibcite{Coq1}{\citeauthoryear {Herbelin}{2009}}
\bibcite{grundlagen-first-edition-volume-one}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt and Bernays\bernaysindex }{1934}}
\citation{grundlagen-second-edition-volume-one}
\bibcite{grundlagen-first-edition-volume-two}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt and Bernays\bernaysindex }{1939}}
\citation{grundlagen-second-edition-volume-two}
\bibcite{grundlagen-second-edition-volume-one}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt and Bernays\bernaysindex }{1968}}
\citation{grundlagen-first-edition-volume-one}
\bibcite{grundlagen-second-edition-volume-two}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt and Bernays\bernaysindex }{1970}}
\citation{grundlagen-first-edition-volume-two}
\bibcite{grundlagen-german-english-edition-volume-one-one}{\citeauthoryear {Hilbe{\index {Hilbert, David (1862--1943)}}rt and Bernays\bernaysindex }{2013}}
\citation{grundlagen-second-edition-volume-one}
\citation{grundlagen-first-edition-volume-one}
\bibcite{HL02}{\citeauthoryear {Hillenbrand{\index {Hillenbrand, Thomas}} and L{\unprotectedoe }chner{\index {Loechner, Bernd (*1967)@{L\"ochner, Bernd (*1967)}}}}{2002}}
\citation{eightteenthCADEtwo}
\bibcite{industrial-strength-1999}{\citeauthoryear {Hinchey and Bowen}{1999}}
\bibcite{5-int-congress-mathematicians-1912}{\citeauthoryear {Hobson and Love}{1913}}
\bibcite{weakaxiomofchoice}{\citeauthoryear {Howard and Rubin}{1998}}
\bibcite{haskell}{\citeauthoryear {Hudlak \bgroup \em  et al.\egroup }{1999}}
\bibcite{huethullotinductionlessinduction}{\citeauthoryear {Huet and Hullot}{1980}}
\citation{focs21}
\bibcite{huet}{\citeauthoryear {Huet}{1980}}
\bibcite{hunt-swords-2009}{\citeauthoryear {Hunt{\index {Hunt, Warren A.}} and Swords}{2009}}
\citation{twentyfirstCAVnine}
\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{inductioncontest}{\citeauthoryear {Hutter{\index {Hutter, Dieter (*1959)}} and Bundy{\index {Bundy, Alan (*1947)}}}{1999}}
\citation{sixteenthCADEninetynine}
\bibcite{inkanext}{\citeauthoryear {Hutter{\index {Hutter, Dieter (*1959)}} and Sengler}{1996}}
\citation{thirteenthCADEninetysix}
\bibcite{siekmann-60}{\citeauthoryear {Hutter{\index {Hutter, Dieter (*1959)}} and Stephan}{2005}}
\bibcite{hutter-rippling}{\citeauthoryear {Hutter{\index {Hutter, Dieter (*1959)}}}{1990}}
\citation{tenthCADEninety}
\bibcite{failure-guide-induction}{\citeauthoryear {Ireland and Bundy{\index {Bundy, Alan (*1947)}}}{1994}}
\bibcite{automatic-learning-proof-planning}{\citeauthoryear {Jamnik \bgroup \em  et al.\egroup }{2003}}
\bibcite{inductionlesshista}{\citeauthoryear {Jouannaud and Kounalis}{1986}}
\citation{lics1}
\bibcite{firstCTRSeightyseven}{\citeauthoryear {Kaplan and Jouannaud}{1988}}
\bibcite{secondCTRSninety}{\citeauthoryear {Kaplan and Okada}{1991}}
\bibcite{kapur2}{\citeauthoryear {Kapur and Musser}{1986}}
\citation{lics1}
\bibcite{kapur1}{\citeauthoryear {Kapur and Musser}{1987}}
\bibcite{mutualexplicitinduction}{\citeauthoryear {Kapur and Subramaniam}{1996}}
\citation{fifthAMASTninetysix}
\bibcite{rrl}{\citeauthoryear {Kapur and Zhang}{1989}}
\citation{thirdRTAeightynine}
\citation{Kapur95}
\bibcite{Kapur95}{\citeauthoryear {Kapur and Zhang}{1995}}
\bibcite{eleventhCADEninetytwo}{\citeauthoryear {Kapur}{1992}}
\bibcite{katz-history}{\citeauthoryear {Katz}{1998}}
\bibcite{ACLTWO-CASESTUDIES}{\citeauthoryear {Kaufmann{\index {Kaufmann, Matt (*1952)}} \bgroup \em  et al.\egroup }{2000a}}
\bibcite{ACLTWO}{\citeauthoryear {Kaufmann{\index {Kaufmann, Matt (*1952)}} \bgroup \em  et al.\egroup }{2000b}}
\bibcite{KB70}{\citeauthoryear {Knuth and 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{induction-no-cut}{\citeauthoryear {Kreisel}{1965}}
\citation{saaty}
\bibcite{inductionlesshistd}{\citeauthoryear {K{\"u}chlin}{1989}}
\citation{kaci-nivat}
\bibcite{kwspec}{\citeauthoryear {K{\"u}hler{\index {Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}} and Wirth{\index {Wirth, Claus-Peter (*1963)}}}{1996}}
\citation{kwspec2}
\bibcite{kwspec2}{\citeauthoryear {K{\"u}hler{\index {Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}} and Wirth{\index {Wirth, Claus-Peter (*1963)}}}{1997}}
\citation{eighthRTAninetyseven}
\citation{kwspec}
\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{lambert-1764}{\citeauthoryear {Lambert}{1764}}
\bibcite{inductionlessinduction1}{\citeauthoryear {Lankford}{1980}}
\bibcite{inductionlessinduction2}{\citeauthoryear {Lankford}{1981}}
\bibcite{honor-robinson}{\citeauthoryear {Lassez and 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 and Overbeek}{1988}}
\bibcite{fermat-career}{\citeauthoryear {Mahoney}{1994}}
\bibcite{smith-pieri}{\citeauthoryear {Marchisotto and Smit{\index {Smith, James T.}}h}{2007}}
\bibcite{Kolloquium-Programmiersprachen-und-Grundlagen-der-Programmierung}{\citeauthoryear {Margaria}{1995}}
\bibcite{LISP}{\citeauthoryear {McCarthy \bgroup \em  et al.\egroup }{1965}}
\bibcite{thirteenthCADEninetysix}{\citeauthoryear {McRobbie and Slaney}{1996}}
\bibcite{proof_planning_with_multiple_strategies}{\citeauthoryear {Melis \bgroup \em  et al.\egroup }{2008}}
\bibcite{machine-intelligence-7}{\citeauthoryear {Meltzer{\index {Meltzer, Bernard (1916?--2008)}} and Michie{\index {Michie, Donald (1923--2007)}}}{1972}}
\bibcite{meltzer-1975}{\citeauthoryear {Meltzer{\index {Meltzer, Bernard (1916?--2008)}}}{1975}}
\bibcite{machine-intelligence-3}{\citeauthoryear {Michie{\index {Michie, Donald (1923--2007)}}}{1968}}
\bibcite{milner-1972}{\citeauthoryear {Milner}{1972}}
\bibcite{moore-lynch-kaufmann-1998}{\citeauthoryear {Moore{\mooreindex } \bgroup \em  et al.\egroup }{1998}}
\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{chaff}{\citeauthoryear {Moskewicz \bgroup \em  et al.\egroup }{2001}}
\citation{dac/2001}
\bibcite{musserinductionlessinduction}{\citeauthoryear {Musser}{1980}}
\citation{seventhPOPLeighty}
\bibcite{ijcai3}{\citeauthoryear {Nilsson}{1973}}
\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{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 \em  et 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 and Voronkov}{2001}}
\citation{firstIJCARone}
\bibcite{HandbookAR}{\citeauthoryear {Robinson{\index {Robinson, J. Alan (*1930?)}} and Voronkow}{2001}}
\bibcite{IFIP-1974}{\citeauthoryear {Rosenfeld}{1974}}
\bibcite{axiomofchoice}{\citeauthoryear {Rubin and Rubin}{1985}}
\bibcite{thirdCTRSninetytwo}{\citeauthoryear {Rusinowitch and 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{schoenfield}{\citeauthoryear {Schoenfield}{1967}}
\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{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 and 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 and Nivat}{1996}}
\bibcite{wirthbecker}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} and Becker}{1995}}
\citation{fourthCTRSninetyfour}
\bibcite{wgjsc}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} and Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (*1959)}}ch}{1994a}}
\bibcite{wgcade}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} and Gram{\discretionary {-}{}{}}li{\index {Gramlich, Bernhard (*1959)}}ch}{1994b}}
\citation{twelvethCADEninetyfour}
\bibcite{SR--95--15}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} and K{\"u}hler{\index {Kuehler, Ulrich (*1964)@{K\"uhler, Ulrich (*1964)}}}}{1995}}
\bibcite{wgkp}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} \bgroup \em  et al.\egroup }{1993}}
\citation{wgjsc}
\citation{wgcade}
\bibcite{herbrand-handbook}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}} \bgroup \em  et al.\egroup }{2009}}
\citation{handbook-of-the-history-of-logic}
\bibcite{wirth-pascal}{\citeauthoryear {Wirth}{1971}}
\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{nonpermut}{\citeauthoryear {Wirth{\index {Wirth, Claus-Peter (*1963)}}}{2006}}
\citation{wirth-jsc-non-permut}
\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}}
\citation{nonpermut}
\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)}}}{2013}}
\bibcite{wolff-rationalis}{\citeauthoryear {Wolff}{1728}}
\bibcite{wolff-rationalis-1740}{\citeauthoryear {Wolff}{1740}}
\citation{wolff-rationalis}
\bibcite{secondICSEseventysix}{\citeauthoryear {Yeh and Ramamoorthy}{1976}}
\bibcite{young-1989}{\citeauthoryear {Young}{1989}}
\bibcite{ZKK88}{\citeauthoryear {Zhang \bgroup \em  et al.\egroup }{1988}}
\citation{ninthCADEeightyeight}
\bibcite{presburger-life}{\citeauthoryear {Zygmunt}{1991}}
\@writefile{toc}{\contentsline {chapter}{INDEX}{105}}