@Article{wirthcardinal,
author    ={Claus-Peter Wirth},
title     ={Descente Infinie + {D}eduction},
journal   ={Logic Journal of the IGPL},
year      ={2004},
pages     ={1--96},
volume    ={12},
number    ={1},
publisher ={Oxford University Press},
note      ={{\url{www.ags.uni-sb.de/~cp/p/d}}},
abstract  ={Inductive theorem proving in the form of descente infinie was
known to the ancient Greeks and is the standard induction method of a working
mathematician since it was reinvented in the middle of the 17th century.
We present an integration of descente infinie into state-of-the-art
free-variable sequent and tableau calculi.
It is well-suited for an efficient interplay of human interaction and
automation and combines raising, explicit representation of 
dependence between variables,
the liberalized delta-rule, preservation of solutions,
and unrestricted applicability of lemmas and induction hypotheses.
The semantical requirements are satisfied for a variety of two-valued logics,
such as clausal logic, classical first-order logic,
and higher-order modal logic.}}