Kripke Models for Classical Logic

Danko Ilik; Gyesik Lee; Hugo Herbelin

doi:10.1016/j.apal.2010.04.007

Kripke Models for Classical Logic

Danko Ilik ^{1, 2, 3, *} Gyesik Lee ^{4, *} Hugo Herbelin ^{1, 2, *}

* Auteur correspondant

1 PPS - Preuves, Programmes et Systèmes

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

3 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]

4 ROSAEC - Research On Software Analysis for Error-free Computing

Abstract : We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.

keyword : Kripke model classical logic sequent calculus lambda mu calculus classical realizability normalization by evaluation

Type de document :

Article dans une revue

Annals of Pure and Applied Logic, Elsevier Masson, 2010, Special Issue: Classical Logic and Computation (2008), 161 (11), pp.1367-1378. 〈10.1016/j.apal.2010.04.007〉

Domaine :

Mathématiques [math] / Logique [math.LO]

Informatique [cs] / Logique en informatique [cs.LO]

Liste complète des métadonnées

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

https://hal.inria.fr/inria-00371959
Contributeur : Danko Ilik <>
Soumis le : mardi 9 mars 2010 - 23:00:58
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : vendredi 24 septembre 2010 - 11:25:33

classical_kripke_rev3.pdf

Fichiers produits par l'(les) auteur(s)

Kripke Models for Classical Logic

Fichiers

Identifiants

Collections

Citation

Exporter

Métriques

491

196

Contact

Kripke Models for Classical Logic

Fichiers

Identifiants

Collections

Citation

Exporter

Partager

Métriques

491

196

Contact