Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus

Hugo Herbelin 1, 2 Gyesik Lee 3, *
* Auteur correspondant
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : We give a simple intuitionistic completeness proof of Kripke semantics for intuitionistic logic with implication and universal quantification with respect to cut-free intuitionistic sequent calculus. The Kripke semantics is ``simplified'' in the way that the domain remains constant. The proof has been formalised in the Coq proof assistant and by combining soundness with completeness, we obtain an executable cut-elimination procedure. The proof easily extends to the case of the absurdity connective using Kripke models with exploding nodes à la Veldman.
Type de document :
Communication dans un congrès
Hiroakira Ono and Makoto Kanazama and Ruy de Queiroz. Workshop on Logic, Language, Information and Computation, Jun 2009, Tokyo, Japan. Springer, 5514, pp.209-217, 2009, Lecture Notes in Artificial Intelligence
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00381554
Contributeur : Hugo Herbelin <>
Soumis le : mardi 5 mai 2009 - 18:48:07
Dernière modification le : jeudi 11 janvier 2018 - 06:22:37
Document(s) archivé(s) le : lundi 15 octobre 2012 - 09:56:37

Fichier

wollic-HerLee09-kripke-cut-eli...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00381554, version 1

Collections

Citation

Hugo Herbelin, Gyesik Lee. Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus. Hiroakira Ono and Makoto Kanazama and Ruy de Queiroz. Workshop on Logic, Language, Information and Computation, Jun 2009, Tokyo, Japan. Springer, 5514, pp.209-217, 2009, Lecture Notes in Artificial Intelligence. 〈inria-00381554〉

Partager

Métriques

Consultations de la notice

216

Téléchargements de fichiers

89