Human-Oriented Inductive Theorem Proving by Descente Infinie - A manifesto.

Claus-Peter Wirth

In: Logic Journal of the IGPL Oxford 20 Oxford University Press. 12/2012.


In this position paper, we briefly review the development of automated inductive theorem proving and computer-assisted mathematical induction. We think that the current low expectations on progress in this field result from a faulty projection. On an abstract but hopefully sufficiently descriptive level, we explain why we believe that future progress in the field is to result from human-orientedness and descente infinie.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence