login
english version rss feed
inria-00371959, version 2
See detailed view  BibTeX  EndNote  TEI  RefWorks
Kripke Models for Classical Logic
Danko Ilik (Author to contact preferably , http://www.lix.polytechnique.fr/~danko/) 123, Gyesik Lee (Author to contact preferably , http://ropas.snu.ac.kr/~gslee/) 4, Hugo Herbelin (Author to contact preferably , http://pauillac.inria.fr/~herbelin) 12
(2009)
Icone de classical_kripke_rev1.pdf
Icone de classical_kripke_rev1.ps
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.
1:  Preuves, Programmes et Systèmes (PPS)
CNRS : UMR7126 – Université Paris-Diderot - Paris VII
2:  PI.R2 (INRIA Paris - Rocquencourt)
INRIA – Université Paris-Diderot - Paris VII – CNRS : UMR7126
3:  Laboratoire d'informatique de l'école polytechnique (LIX)
CNRS : UMR7161 – Polytechnique - X
4:  Research On Software Analysis for Error-free Computing (ROSAEC)
Seoul National University
Mathematics/Logic
Computer Science/Logic in Computer Science
Kripke model – classical logic – sequent calculus – lambda mu calculus – classical realizability – normalization by evaluation