A Lightweight Double-negation Translation

Frédéric Gilbert 1, 2, 3, *
* Auteur correspondant
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : Deciding whether a classical theorem can be proved constructively is a well-known undecidable problem. As a consequence, any computable double-negation translation inserts some unnecessary double negations. This paper shows that most of these unnecessary insertions can be avoided without any use of constructive proof search techniques. For this purpose, we restrict the analysis to syntax-directed double-negation translations, which translate a proposition through a single traversal – and include most of the usual translations such as Kolmogorov's, Gödel-Gentzen's, and Kuroda's. A partial order among translations are presented to select translations avoiding as many double negations as possible. This order admits a unique minimal syntax-directed translation with noticeable properties.
Type de document :
Communication dans un congrès
LPAR-20. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. EasyChair Proceedings in Computing, EasyChair Proceedings in Computing
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01245021
Contributeur : Frédéric Gilbert <>
Soumis le : mercredi 16 décembre 2015 - 15:27:22
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : jeudi 17 mars 2016 - 14:51:25

Fichier

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

Identifiants

  • HAL Id : hal-01245021, version 1

Citation

Frédéric Gilbert. A Lightweight Double-negation Translation. LPAR-20. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. EasyChair Proceedings in Computing, EasyChair Proceedings in Computing. 〈hal-01245021〉

Partager

Métriques

Consultations de la notice

248

Téléchargements de fichiers

119