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

https://hal.inria.fr/hal-01516788
Contributor : Frédéric Gilbert <>
Submitted on : Tuesday, May 2, 2017 - 11:30:30 AM
Last modification on : Thursday, December 5, 2019 - 1:38:40 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

242

Files downloads

178