Généralisations et méthodes correctes pour l'induction mathématique

TEL :: [tel-00505928, version 1]
http://tel.archives-ouvertes.fr/tel-00505928/fr/
Il existe de nombreux systèmes de preuves par induction visant à automatiser la preuve de théorèmes mathématiques. Cependant, un système de preuve ne peut pas être réellement automatique si plusieurs interactions humaines -- telles que l'apport de lemmes, de généralisations, ou de schémas d'induction -- sont nécessaires pour prouver des théorèmes qui semblent triviaux pour un être humain. Par exemple, la preuve de la commutativité de la multiplication (y * x = x * y) doit notamment recourir à des lemmes exprimant la distributivité de la multiplication ainsi que la distributivité et la commutativité de l'addition. Dans cette thèse, nous proposons des apports aux méthodes de preuve par induction dans le sens d'une plus grande automatisation.
...