Skip to Main content Skip to Navigation
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 metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-01420634
Contributor : Raphaël Cauderlier <>
Submitted on : Tuesday, December 20, 2016 - 6:12:53 PM
Last modification on : Tuesday, July 7, 2020 - 11:52:47 AM

File

LFMTP_2016.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

270

Files downloads

384