Authors
Claus-Peter Wirth
Title
Descente Infinie + Deduction
In
Research Report 737/2000 (green/grey series), Fachbereich Informatik, Universität Dortmund,
Bibtex Entry
Up-to-dateness
Final edition of internal report (Feb. 1, 2003).
There is a more recent, extended and improved journal version!
There is also an old short version!
Abstract
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) classical 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.
Full paper