Descente Infinie + Deduction
Claus-Peter Wirth · Logic Journal of IGPL · 2004
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 variable dependency, the liberalized δ-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.