A Rewrite System for Proof Constructivization - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

A Rewrite System for Proof Constructivization

Résumé

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.
Fichier principal
Vignette du fichier
LFMTP_2016.pdf (235.68 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01420634 , version 1 (20-12-2016)

Identifiants

Citer

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⟩
125 Consultations
221 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More