inria-00371959, version 4
Kripke Models for Classical Logic
Danko Ilik
1, 2, 3Gyesik Lee
4Hugo Herbelin
1, 2
Annals of Pure and Applied Logic 161, 11 (2010) 1367-1378
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.
- 1: Preuves, Programmes et Systèmes (PPS)
- CNRS : UMR7126 – Université Paris VII - Paris Diderot
- 2: PI.R2 (INRIA Paris - Rocquencourt)
- INRIA – Université Paris VII - Paris Diderot – 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
- Domain : Mathematics/Logic
Computer Science/Logic in Computer Science - Keywords : Kripke model – classical logic – sequent calculus – lambda mu calculus – classical realizability – normalization by evaluation
- Available versions : v1 (2009-04-01) v2 (2009-10-12) v3 (2010-02-26) v4 (2010-06-07)
- inria-00371959, version 4
- http://hal.inria.fr/inria-00371959
- oai:hal.inria.fr:inria-00371959
- From: Danko Ilik
- Submitted on: Tuesday, 9 March 2010 23:00:58
- Updated on: Monday, 20 September 2010 17:15:44






Associated documents

See also
Export