Unbounded Proof-Length Speed-up in Deduction Modulo

Guillaume Burel 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In 1973, Parikh proved a speed-up theorem conjectured by Gödel 37 years before: there exist arithmetical formulæ that are provable in first-order arithmetic, but whose shorter proof in second-order arithmetic is arbitrarily smaller than any proof in first order. On the other hand, resolution for higher-order logic can be simulated step by step in a first-order narrowing and resolution method based on deduction modulo, whose paradigm is to separate deduction and computation to make proofs clearer and shorter. We first prove that it is possible to find formulæ whose smaller proof in natural deduction modulo a very simple rewrite system is unboundedly smaller than any proof in pure natural deduction. Then, we show that i+1th-order arithmetic can be linearly simulated into ith-order arithmetic modulo some confluent and terminating rewrite system. We also prove that there exists a speed-up between ith-order arithmetic modulo this system and ith-order arithmetic without modulo. These two results allows us to prove that the speed-up conjectured by Gödel does not come from the deductive part of the proofs, but can be expressed as simple computation, therefore justifying the use of deduction modulo as an efficient first order setting simulating higher order.
Type de document :
Communication dans un congrès
Jacques Duparc and Thomas Henziger. 16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Sep 2007, Lausanne, Switzerland. Springer Verlag, 4646, pp.496-511, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74915-8_37〉
Liste complète des métadonnées

Littérature citée [22 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00138195
Contributeur : Guillaume Burel <>
Soumis le : mardi 3 juillet 2007 - 11:33:41
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 16:54:57

Fichiers

speedup_full.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Guillaume Burel. Unbounded Proof-Length Speed-up in Deduction Modulo. Jacques Duparc and Thomas Henziger. 16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Sep 2007, Lausanne, Switzerland. Springer Verlag, 4646, pp.496-511, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74915-8_37〉. 〈inria-00138195v3〉

Partager

Métriques

Consultations de la notice

277

Téléchargements de fichiers

72