Automated Constructivization of Proofs

Frédéric Gilbert (1, 2)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
2 LSL - Laboratoire Sûreté des Logiciels

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.

Domaines: Informatique [cs]; Logique en informatique [cs.LO]; Théorie et langage formel [cs.FL]

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