@TechReport{ags-2003-d-1,
  author     ={Claus-Peter Wirth},
  institution={FB Informatik, {Univ.\ Dortmund}},
  number     ={737/2000},
  title      ={Descente Infinie + {Deduction. \ Extd.\ version, Feb.\,1, 2003},
               {\url{http://www.ags.uni-sb.de/~cp/p/tab99/new.html}}},
  type       ={Research Report (green/grey series)},
  year       ={2000},
  abstract   ={Although induction is omnipresent, inductive theorem proving in
the form of descente infinie has not yet been integrated into full first-order
deductive calculi.
We present such an integration that even works for higher-order logic. This
integration is based on lemma
and induction hypothesis application for free variable
sequent and tableau calculi.
We discuss the appropriateness of these types of calculi for this integration.
The deductive part of this integration requires the first combination of
raising, explicit variable dependency representation,
the liberalized delta-rule, and preservation of solutions.}}