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.
Cite
CITATION STYLE
Gilbert, F. (2017). Automated constructivization of proofs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10203 LNCS, pp. 480–495). Springer Verlag. https://doi.org/10.1007/978-3-662-54458-7_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
