Skip to Main content Skip to Navigation
Journal articles

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
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download
https://hal.inria.fr/inria-00371959
Contributor : Danko Ilik Connect in order to contact the contributor
Submitted on : Tuesday, March 9, 2010 - 11:00:58 PM
Last modification on : Friday, January 21, 2022 - 3:21:45 AM
Long-term archiving on: : Friday, September 24, 2010 - 11:25:33 AM

Files

Vignette du document
classical_kripke_rev3.pdf
Files produced by the author(s)

Identifiers

Collections

UNIV-PARIS7 | X | PPS | CNRS | INRIA | LIX | INSMI | X-LIX | X-DEP-INFO | INRIA2 | UNIV-PARIS

Citation

Danko Ilik, Gyesik Lee, Hugo Herbelin. Kripke Models for Classical Logic. 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⟩. ⟨inria-00371959v4⟩

Export

BibTeX TEI DC DCterms EndNote Datacite

Share

Metrics

Record views

308

Files downloads

443

 

Contact                    Legal Notice                    Personal Data