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

inria-00371959, version 4

Kripke Models for Classical Logic

Danko Ilik ( Auteur à contacter de préférence ) ^1, 2, 3, Gyesik Lee () ⁴, Hugo Herbelin () ^1, 2

Annals of Pure and Applied Logic 161, 11 (2010) 1367-1378

Résumé : 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

inria-00371959, version 4
http://hal.inria.fr/inria-00371959
oai:hal.inria.fr:inria-00371959
Contributeur : Danko Ilik <>
Soumis le : Mardi 9 Mars 2010, 23:00:58
Dernière modification le : Lundi 20 Septembre 2010, 17:15:44

Voir la fiche détaillée

Documents associés

PDF :

PS :

arXiv : 0904.0071

DOI : 10.1016/j.apal.2010.04.007

Voir aussi

En savoir plus sur cette publication

Exporter

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>Articles dans des revues avec comité de lecture</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 VII - Paris Diderot</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 VII - Paris Diderot</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 VII - Paris Diderot</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 VII - Paris Diderot</orgName>
<orgName type="institution">CNRS : UMR7126</orgName>
</affiliation>
</author>
<title type="main" level="a">Kripke Models for Classical Logic</title></analytic><monogr><title level="j" type="main">Annals of Pure and Applied Logic</title><imprint><publisher>Elsevier</publisher><biblScope type="publicationDate">2010-08-00</biblScope><biblScope type="vol">161</biblScope><biblScope type="issue">11</biblScope><biblScope type="pp">1367-1378</biblScope></imprint></monogr><idno type="doi">10.1016/j.apal.2010.04.007</idno><idno type="HALid">http://hal.inria.fr/inria-00371959</idno><idno type="HALFile">http://hal.inria.fr/inria-00371959/PDF/classical_kripke_rev3.pdf</idno></biblStruct>
</listBibl>
</listBibl>