"Descente Infinie" Theorem Proving

provers using the "Descente Infinie" induction principle.
Different proof techniques, like those based on implicit induction
and saturation, are uniformly presented as applications of this
principle. The framework offers a clear separation between logic
and computation, by the means of
i) an abstract inference system that defines the maximal sets of
induction hypotheses available at every step of a proof, and
ii) reasoning modules that perform the computation and allow for
modular design of the concrete inference rules.
The methodology is applied to build a concrete implicit induction
prover and analyse an existent saturation-based inference system.