×

Computer-assisted human-oriented inductive theorem proving by descente infinie – a manifesto. (English) Zbl 1314.03019

This article is an entertaining position paper that provides an introduction to and arguments in favour of using so-called descente infinie (a term coined by Fermat for a much older method) together with modern deductive calculi.
The author argues that working mathematicians require interactive proof assistants, and that currently available systems are somewhat lacking in this respect. He explains that for inductive proofs two important and usually hard tasks can be identified: (1) forming induction hypotheses and (2) an induction ordering. These are the foundations of descente infinie, which was originally used for identifying smaller counterexamples along a well-founded ordering. In formal logic, this is usually captured by the theorem of Noetherian induction.
This is contrasted to the prevalent technique of explicit induction in deduction, which is less flexible, as it needs fixing hypotheses and ordering in descente infinie in advance. The author describes also several other problems with explicit induction and quotes the solver QUODLIBET, which incorporates the discussed descente infinie approach and has proved to be effective with mathematicians and also reasonably efficient in practice.
One note of caution: there seems to be a consistent typo in Peano’s first name in the paper. It should be Giuseppe, not Guiseppe.

MSC:

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI