Skip to main content Skip to main navigation

Publikation

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

Claus-Peter Wirth
In: Logic Journal of the IGPL Oxford, Vol. 20, Oxford University Press. 12/2012.

Zusammenfassung

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.