Skip to Main content Skip to Navigation
New interface
Conference papers

A Rewrite System for Proof Constructivization

Abstract : Proof constructivization is the problem of automatically extracting constructive proofs out of classical proofs. This process is required when classical theorem provers are integrated in intuitionistic proof assistants. We use the ability of rewrite systems to represent partial functions to implement heuristics for proof constructivization in Dedukti, a logical framework based on rewriting in which proofs are first-class objects which can be the subject of computation. We benchmark these heuristics on the proofs output by the automated theorem prover Zenon on the TPTP library of problems.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Raphaël Cauderlier Connect in order to contact the contributor
Submitted on : Tuesday, December 20, 2016 - 6:12:53 PM
Last modification on : Tuesday, October 25, 2022 - 4:21:58 PM


Files produced by the author(s)



Raphaël Cauderlier. A Rewrite System for Proof Constructivization. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016, Jun 2016, Porto, Portugal. pp.1 - 7, ⟨10.1145/2966268.2966270⟩. ⟨hal-01420634⟩



Record views


Files downloads