HAL - INRIA :: [inria-00371959, version 2] Kripke Models for Classical Logic

inria-00371959, version 2

arXiv:0904.0071

See detailed view

BibTeX EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="article"><head>Documents without publication reference</head>
<biblStruct type="article" xml:id="inria-00371959"><analytic>
<author><persName><forename>Danko</forename><surname>Ilik</surname></persName>
<affiliation>
<orgName type="laboratory">PPS</orgName>
<orgName type="team">Preuves, Programmes et Systèmes</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7126</orgName>
<orgName type="institution">Université Paris-Diderot - Paris VII</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Paris - Rocquencourt</orgName>
<orgName type="team">PI.R2</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Université Paris-Diderot - Paris VII</orgName>
<orgName type="institution">CNRS : UMR7126</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LIX</orgName>
<orgName type="team">Laboratoire d'informatique de l'école polytechnique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7161</orgName>
<orgName type="institution">Polytechnique - X</orgName>
</affiliation>
</author>
<author><persName><forename>Gyesik</forename><surname>Lee</surname></persName>
<affiliation>
<orgName type="laboratory">ROSAEC</orgName>
<orgName type="team">Research On Software Analysis for Error-free Computing</orgName>
<country>KR</country>
<orgName type="institution">Seoul National University</orgName>
</affiliation>
</author>
<author><persName><forename>Hugo</forename><surname>Herbelin</surname></persName>
<affiliation>
<orgName type="laboratory">PPS</orgName>
<orgName type="team">Preuves, Programmes et Systèmes</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7126</orgName>
<orgName type="institution">Université Paris-Diderot - Paris VII</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">INRIA Paris - Rocquencourt</orgName>
<orgName type="team">PI.R2</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Université Paris-Diderot - Paris VII</orgName>
<orgName type="institution">CNRS : UMR7126</orgName>
</affiliation>
</author>
<title type="main" level="a">Kripke Models for Classical Logic</title></analytic><monogr><imprint/></monogr><idno type="HALid">http://hal.inria.fr/inria-00371959/en/</idno><idno type="HALFile">http://hal.inria.fr/inria-00371959/PDF/classical_kripke_rev1.pdf</idno></biblStruct>
</listBibl>
</listBibl>

Kripke Models for Classical Logic

Danko Ilik (

) ^1, 2, 3, Gyesik Lee (

) ⁴, Hugo Herbelin (

) ^1, 2

(2009)

Access to full text
PDF
PS

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-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

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)


inria-00371959, version 2
http://hal.inria.fr/inria-00371959/en/
oai:hal.inria.fr:inria-00371959_v2
From: Danko Ilik <>
Submitted on: Monday, 12 October 2009 10:00:08
Updated on: Monday, 12 October 2009 11:59:59