Normalization by Completeness with Heyting Algebras

Abstract : Usual normalization by evaluation techniques have a strong relationship with completeness with respect to Kripke structures. But Kripke structures is not the only semantics that ts intuitionistic logic: Heyting algebras are a more algebraic alternative. In this paper, we focus on this less investigated area: how completeness with respect to Heyting algebras generate a normalization algorithm for a natural deduction calculus, in the propositional fragment. Our main contributions is that we prove in a direct way completeness of natural deduction with respect to Heyting algebras, that the underlying algorithm natively deals with disjunction, that we formalized those proofs in Coq, and give an extracted algorithm.
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
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-01204599
Contributeur : Claire Medrala <>
Soumis le : jeudi 24 septembre 2015 - 11:30:09
Dernière modification le : mardi 11 septembre 2018 - 15:53:14
Document(s) archivé(s) le : mardi 29 décembre 2015 - 09:45:36

Fichier

A-614.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01204599, version 1

Collections

Citation

Gaëtan Gilbert, Olivier Hermant. Normalization by Completeness with Heyting Algebras. LPAR 20 : 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. 〈hal-01204599〉

Partager

Métriques

Consultations de la notice

300

Téléchargements de fichiers

124