Skip to Main content Skip to Navigation
Conference papers

Automated Constructivization of Proofs

Frédéric Gilbert 1, 2
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LSV - Laboratoire Spécification et Vérification [Cachan]
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.
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-01516788
Contributor : Frédéric Gilbert Connect in order to contact the contributor
Submitted on : Tuesday, May 2, 2017 - 11:30:30 AM
Last modification on : Friday, June 25, 2021 - 9:52:03 AM
Long-term archiving on: : Thursday, August 3, 2017 - 12:38:56 PM

Files

constructivization.pdf
Files produced by the author(s)

Identifiers

Citation

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

Share

Metrics

Record views

350

Files downloads

399