Polarizing Double Negation Translations

Abstract : Double-negation translations are used to encode and decode classical proofs in intuitionistic logic. We show that, in the cut-free fragment, we can simplify the translations and introduce fewer negations. To achieve this, we consider the polarization of the formulae and adapt those translation to the different connectives and quantifiers. We show that the embedding results still hold, using a customized version of the focused classical sequent calculus. We also prove the latter equivalent to more usual versions of the sequent calculus. This polarization process allows lighter embeddings, and sheds some light on the relationship between intuitionistic and classical connectives.
Type de document :
Communication dans un congrès
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.182-197, 2013, LNCS ARCoSS
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-00920224
Contributeur : Olivier Hermant <>
Soumis le : mercredi 18 décembre 2013 - 21:30:07
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : jeudi 20 mars 2014 - 11:27:07

Fichiers

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

Identifiants

  • HAL Id : hal-00920224, version 2
  • ARXIV : 1312.5420

Collections

Citation

Mélanie Boudard, Olivier Hermant. Polarizing Double Negation Translations. Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.182-197, 2013, LNCS ARCoSS. 〈hal-00920224v2〉

Partager

Métriques

Consultations de la notice

368

Téléchargements de fichiers

117