Généralisations et méthodes correctes pour l'induction mathématique
Institution:
NiceDisciplines:
Directors:
Abstract EN:
A major challenge for induction is to mechanize the most possible the omega-rule. The most advanced induction theorem provers and theoretical contributions, either do not provide sound rules speculating lemma or generalization, or simply desert appellation ``automatic prover'' to prefer ``proof-checker''. This thesis essentially purposes enhancements to mathematical inductive proofs methods in that way. These enhancements are composed of two efficient heuristics and, mainly, two sound algorithms. The first sound algorithm computes sound generalization for unconditional theories. The second is a completely new method -- ``term partition'' -- to proof inductive theorem.
Abstract FR:
L'un des plus importants défis pour l'induction est de mécaniser le plus possible la règle-omega. En fait, les systèmes de preuve et les contributions théoriques les plus avancées, soit ne proposent pas de règles permettant une spéculation correcte de lemme ou de généralisation, soit évitent l'appellation << automatique >> pour préférer celle de << vérificateur de preuve>>. Dans cette thèse, nous proposons des apports aux méthodes de preuve par induction dans le sens d'un 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.