Loading...
Please wait, while we are loading the content...
Similar Documents
A Rewrite System for Proof Constructivization
| Content Provider | ACM Digital Library |
|---|---|
| Author | Cauderlier, Raphaël |
| 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. |
| Starting Page | 1 |
| Ending Page | 7 |
| Page Count | 7 |
| File Format | |
| ISBN | 9781450347778 |
| DOI | 10.1145/2966268.2966270 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2016-06-23 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Intuitionistic logic Confluence Dedukti Meta-programming Rewriting Logical framework |
| Content Type | Text |
| Resource Type | Article |
