Cette thèse propose et étudie de nouveaux systèmes déductifs mêlant calculs et déductions. La déduction modulo est un premier formalisme qui traduit un pouvoir calculatoire grâce à un système de réécriture. Nous présentons un paradigme dual appelé superdéduction qui traduit un pouvoir déductif par de nouvelles inférences. Ces pouvoirs calculatoires et déductifs modifient la représentation des preuves et leur interaction par les processus d'élimination des coupures. La normalisation forte ou l'admissibilité des coupures ne sont plus garanties et apparaissent alors comme des propriétés intrinsèques des théories représentées sous forme de systèmes de réécriture. Nous démontrons que certains critères permeent d'assurer ces propriétés, notamment en définissant un langage de termes de preuve pour la superdéduction et en étudiant la permutabilité des inférences en calcul des séquents classique. Notre attention est focalisée sur les calculs des séquents classiques et la représentation des preuves dans de tels systèmes. D'autres formalismes connexes sont envisagés, notamment les réseaux de preuve et le focusing. Nous comparons cette dernière approe à la superdéduction, ce qui nous amène à proposer une refonte du paradigme de superdéduction basée sur un système de multifocusing pour la logique classique. Nous en montrons les effets bénéfiques en démontrant la complétude des systèmes déductifs obtenus.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00553219 |
| Date | 12 March 2010 |
| Creators | Houtmann, Clément |
| Publisher | Université Henri Poincaré - Nancy I |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0088 seconds