- Claus-Peter Wirth
- Descente Infinie + Deduction
Research Report 737/2000 (green/grey series),
Fachbereich Informatik, Universität Dortmund,
- Final edition of internal report (Feb. 1, 2003).
There is a more recent, extended and improved
There is also an old short version!
Although induction is omnipresent,
inductive theorem proving in the form of descente infinie
has not yet been integrated into full 1st order deductive calculi.
We present such an integration for (possibly even higher-order)
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.
- Full paper
- .4 Mbytes
- .2 Mbytes
The fonts of this version differ from the original,
some originally identical fonts are different in this version,
and some figures have moved to silly places,
but the whole file can be searched!
- .7 Mbytes