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, *}

* Corresponding author

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

Document type :

Journal articles

Domain :

Mathematics [math] / Logic [math.LO]

Computer Science [cs] / Logic in Computer Science [cs.LO]

Liste complète des métadonnées

Cited literature [34 references] Display Hide Download

https://hal.inria.fr/inria-00371959
Contributor : Danko Ilik <>
Submitted on : Tuesday, March 9, 2010 - 11:00:58 PM
Last modification on : Friday, April 12, 2019 - 2:46:04 PM
Document(s) archivé(s) le : Friday, September 24, 2010 - 11:25:33 AM

classical_kripke_rev3.pdf

Files produced by the author(s)

Kripke Models for Classical Logic

Files

Identifiers

Collections

Citation

Export

Metrics

515

454

Contact

Kripke Models for Classical Logic

Files

Identifiers

Collections

Citation

Export

Share

Metrics

515

454

Contact