Skip to Main content Skip to Navigation
Conference papers

A Lightweight Double-negation Translation

Frédéric Gilbert 1, 2, 3, *
* Corresponding author
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.
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-01245021
Contributor : Frédéric Gilbert <>
Submitted on : Wednesday, December 16, 2015 - 3:27:22 PM
Last modification on : Friday, June 25, 2021 - 9:52:03 AM
Long-term archiving on: : Thursday, March 17, 2016 - 2:51:25 PM

File

paper_36.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-01245021⟩

Share

Metrics

Record views

566

Files downloads

480