Return to search

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

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. Ces apports sont constitués de deux heuristiques efficaces et surtout de deux algorithmes corrects. Le premier algorithme calcule des généralisations correctes pour des théories non-conditionnelles. Le second est une méthode d'induction originale -- la "partition de termes"-- permettant la preuve automatique de théorèmes inductifs.

Identiferoai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00505928
Date29 March 2002
CreatorsUrso, Pascal
PublisherUniversité de Nice Sophia-Antipolis
Source SetsCCSD theses-EN-ligne, France
LanguageFrench
Detected LanguageFrench
TypePhD thesis

Page generated in 0.0018 seconds