Skip to Main content Skip to Navigation
New interface
Conference papers

Automated Constructivization of Proofs

Frédéric Gilbert 1, 2 
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
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
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 : Thursday, February 17, 2022 - 10:08:03 AM
Long-term archiving on: : Thursday, August 3, 2017 - 12:38:56 PM


Files produced by the author(s)



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



Record views


Files downloads