Automated Constructivization of Proofs

Frédéric Gilbert 1, 2
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
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 : jeudi 15 mars 2018 - 15:03:51
Document(s) archivé(s) le : jeudi 3 août 2017 - 12:38:56

Fichiers

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

Identifiants

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

163

Téléchargements de fichiers

64