Good proofs in deduction modulo
Bonnes démonstrations en déduction modulo
Résumé
This thesis studies how computations may simplify proofs and aims to make mechanized proof search better. We are particularly interested in deduction modulo and superdeduction, two close formalisms allowing the integration of computations into proofs through a rewrite system. We consider three simplicity criteria related to proof search.
Cut admissibility makes it possible to restrain the proof-search space but does not always hold in deduction modulo. We define a completion method transforming a rewrite system representing computations so that at the end cut admissibility holds. By the way, we show how to transform any first-order theory to integrate it into the computational part of proofs.
We show then how deduction modulo unboundedly reduces proof lengths, by transferring deduction steps into computations. In particular, we apply this to higher-order arithmetic to show that proof-length speedups between ith- and i+1st-order arithmetic disappear when working in deduction modulo, making it possible to work in first-order logic modulo without increasing proof lengths.
Following this last result, we investigate which higher-order systems can be simulated in first order using deduction modulo. We are interested by pure type systems, which are generic type systems for the lambda-calculus with dependent types. We show how these systems can be encoded in superdeduction. This offers new perspectives on their normalization and on proof search within them. We also develop a methodology to describe how superdeduction can be used to specify deductive systems.
Cut admissibility makes it possible to restrain the proof-search space but does not always hold in deduction modulo. We define a completion method transforming a rewrite system representing computations so that at the end cut admissibility holds. By the way, we show how to transform any first-order theory to integrate it into the computational part of proofs.
We show then how deduction modulo unboundedly reduces proof lengths, by transferring deduction steps into computations. In particular, we apply this to higher-order arithmetic to show that proof-length speedups between ith- and i+1st-order arithmetic disappear when working in deduction modulo, making it possible to work in first-order logic modulo without increasing proof lengths.
Following this last result, we investigate which higher-order systems can be simulated in first order using deduction modulo. We are interested by pure type systems, which are generic type systems for the lambda-calculus with dependent types. We show how these systems can be encoded in superdeduction. This offers new perspectives on their normalization and on proof search within them. We also develop a methodology to describe how superdeduction can be used to specify deductive systems.
Cette thèse étudie comment l'intégration du calcul dans les démonstrations peut les simplifier. Nous nous intéressons pour cela à la déduction modulo et à la surdéduction, deux formalismes proches dans lesquels le calcul est incorporé dans les démonstrations via un système de réécriture. Pour améliorer la recherche mécanisée de démonstration, nous considérons trois critères de simplicité.
L'admissibilité des coupures permet de restreindre l'espace de recherche des démonstrations, mais elle n'est pas toujours assurée en déduction modulo. Nous définissons une procédure qui complète le système de réécriture pour, au final, admettre les coupures. Au passage, nous montrons comment transformer toute théorie pour l'intégrer à la partie calculatoire des démonstrations.
Nous montrons ensuite comment la déduction modulo permet de réduire arbitrairement la taille des démonstrations, en transférant des étapes de déduction dans le calcul. En particulier, nous appliquons ceci à l'arithmétique d'ordre supérieur pour démontrer que les réductions de taille qui sont possibles en augmentant l'ordre dans lequel on se place disparaissent si on travaille en déduction modulo.
Suite à ce dernier résultat, nous avons recherchés quels sont les systèmes d'ordre supérieur pouvant être simulés au premier ordre, en déduction modulo. Nous nous sommes intéressés aux systèmes de type purs et nous montrons comment ils peuvent être encodés en surdéduction, ce qui offre de nouvelles perspectives concernant leur normalisation et la recherche de démonstration dans ceux-ci. Nous développons également une méthodologie qui permet d'utiliser la surdéduction pour spécifier des systèmes de déduction.
L'admissibilité des coupures permet de restreindre l'espace de recherche des démonstrations, mais elle n'est pas toujours assurée en déduction modulo. Nous définissons une procédure qui complète le système de réécriture pour, au final, admettre les coupures. Au passage, nous montrons comment transformer toute théorie pour l'intégrer à la partie calculatoire des démonstrations.
Nous montrons ensuite comment la déduction modulo permet de réduire arbitrairement la taille des démonstrations, en transférant des étapes de déduction dans le calcul. En particulier, nous appliquons ceci à l'arithmétique d'ordre supérieur pour démontrer que les réductions de taille qui sont possibles en augmentant l'ordre dans lequel on se place disparaissent si on travaille en déduction modulo.
Suite à ce dernier résultat, nous avons recherchés quels sont les systèmes d'ordre supérieur pouvant être simulés au premier ordre, en déduction modulo. Nous nous sommes intéressés aux systèmes de type purs et nous montrons comment ils peuvent être encodés en surdéduction, ce qui offre de nouvelles perspectives concernant leur normalisation et la recherche de démonstration dans ceux-ci. Nous développons également une méthodologie qui permet d'utiliser la surdéduction pour spécifier des systèmes de déduction.
Fichier principal
manuscript.pdf (2.36 Mo)
Télécharger le fichier
soutenance.pdf (1.6 Mo)
Télécharger le fichier
Format : Autre
Loading...