Automated Constructivization of Proofs

Frédéric Gilbert 1, 2
2 LSL - Laboratoire Sûreté des Logiciels
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
Abstract : No computable function can output a constructive proof from a classical one whenever its associated theorem also holds constructively. We show in this paper that it is however possible, in practice, to turn a large amount of classical proofs into constructive ones. We describe for this purpose a linear-time constructivization algorithm which is provably complete on large fragments of predicate logic.
Type de document :
Communication dans un congrès
FoSSaCS 2017, Apr 2017, Uppsala, Sweden. 2017, 〈10.1007/978-3-662-54458-7_28〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01516788
Contributeur : Frédéric Gilbert <>
Soumis le : mardi 2 mai 2017 - 11:30:30
Dernière modification le : mardi 9 janvier 2018 - 14:13:30
Document(s) archivé(s) le : jeudi 3 août 2017 - 12:38:56

Fichiers

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

Identifiants

Collections

Citation

Frédéric Gilbert. Automated Constructivization of Proofs. FoSSaCS 2017, Apr 2017, Uppsala, Sweden. 2017, 〈10.1007/978-3-662-54458-7_28〉. 〈hal-01516788〉

Partager

Métriques

Consultations de la notice

76

Téléchargements de fichiers

31