Computer-assisted human-oriented inductive theorem proving by descente infinie--a manifesto
Claus-Peter Wirth · Logic Journal of IGPL · 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.