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.
Type de document :
Communication dans un congrès
Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016, Jun 2016, Porto, Portugal. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016, pp.1 - 7, 2016, 〈http://dlicata.web.wesleyan.edu/events/lfmtp2016/〉. 〈10.1145/2966268.2966270〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01420634
Contributeur : Raphaël Cauderlier <>
Soumis le : mardi 20 décembre 2016 - 18:12:53
Dernière modification le : mardi 13 novembre 2018 - 17:10:03

Fichier

LFMTP_2016.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice 2016, pp.1 - 7, 2016, 〈http://dlicata.web.wesleyan.edu/events/lfmtp2016/〉. 〈10.1145/2966268.2966270〉. 〈hal-01420634〉

Partager

Métriques

Consultations de la notice

191

Téléchargements de fichiers

59