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
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 metadatas

Cited literature [13 references]  Display  Hide  Download
Contributor : Frédéric Gilbert <>
Submitted on : Tuesday, May 2, 2017 - 11:30:30 AM
Last modification on : Tuesday, July 7, 2020 - 11:52:47 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