Corpus
PascalFrancis
Racine
Corpus
Checkpoint
PascalFrancis
Racine
PascalFrancis
Exploration
Accueil
Racine
Racine

Serveur d'exploration sur la recherche en informatique en Lorraine

Attention, ce site est en cours de développement !
Attention, site généré par des moyens informatiques à partir de corpus bruts.
Les informations ne sont donc pas validées.

Sequent calculi and decidability for intuitionistic hybrid logic

Identifieur interne : 000129 ( PascalFrancis/Corpus ); précédent : 000128; suivant : 000130

Sequent calculi and decidability for intuitionistic hybrid logic

Auteurs : Didier Galmiche ; Yakoub Salhi

Source :

RBID : Pascal:12-0044340

Descripteurs français

English descriptors

Abstract

In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for IHL and then prove its decidability.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

pA  
A01 01  1    @0 0890-5401
A02 01      @0 INFCEC
A03   1    @0 Inf. comput. : (Print)
A05       @2 209
A06       @2 12
A08 01  1  ENG  @1 Sequent calculi and decidability for intuitionistic hybrid logic
A09 01  1  ENG  @1 Intuitionistic Modal Logic and Applications (IMLA 2008)
A11 01  1    @1 GALMICHE (Didier)
A11 02  1    @1 SALHI (Yakoub)
A12 01  1    @1 DE PAIVA (Valeria) @9 ed.
A12 02  1    @1 PIENTKA (Brigitte) @9 ed.
A14 01      @1 LORIA- UHP Nancy 1, Campus Scientifique, BP239 @2 54 506 Vandœuvre-lès-Nancy @3 FRA @Z 1 aut. @Z 2 aut.
A15 01      @1 Rearden Commerce @2 Foster City, CA @3 USA @Z 1 aut.
A15 02      @1 School of Computer Science, McGill University @3 CAN @Z 2 aut.
A20       @1 1447-1463
A21       @1 2011
A23 01      @0 ENG
A43 01      @1 INIST @2 8341 @5 354000505693010020
A44       @0 0000 @1 © 2012 INIST-CNRS. All rights reserved.
A45       @0 19 ref.
A47 01  1    @0 12-0044340
A60       @1 P
A61       @0 A
A64 01  1    @0 Information and computation : (Print)
A66 01      @0 NLD
C01 01    ENG  @0 In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for IHL and then prove its decidability.
C02 01  X    @0 001D02A08
C02 02  X    @0 001A02A01B
C02 03  X    @0 001A02A01F
C02 04  X    @0 001D02C02
C03 01  X  FRE  @0 Informatique théorique @5 01
C03 01  X  ENG  @0 Computer theory @5 01
C03 01  X  SPA  @0 Informática teórica @5 01
C03 02  X  FRE  @0 Décidabilité @5 17
C03 02  X  ENG  @0 Decidability @5 17
C03 02  X  SPA  @0 Decidibilidad @5 17
C03 03  X  FRE  @0 Logique intuitionniste @5 18
C03 03  X  ENG  @0 Intuitionistic logic @5 18
C03 03  X  SPA  @0 Lógica intuicionista @5 18
C03 04  X  FRE  @0 Théorie preuve @5 19
C03 04  X  ENG  @0 Proof theory @5 19
C03 04  X  SPA  @0 Teoría demonstración @5 19
C03 05  X  FRE  @0 Théorie constructive @5 20
C03 05  X  ENG  @0 Constructive theory @5 20
C03 05  X  SPA  @0 Teoría constructiva @5 20
C03 06  X  FRE  @0 Calcul séquent @5 21
C03 06  X  ENG  @0 Sequent calculus @5 21
C03 06  X  SPA  @0 Càlculo sequente @5 21
C03 07  X  FRE  @0 Consistance sémantique @5 22
C03 07  X  ENG  @0 Soundness @5 22
C03 07  X  SPA  @0 Consistencia semantica @5 22
C03 08  X  FRE  @0 Complétude @5 23
C03 08  X  ENG  @0 Completeness @5 23
C03 08  X  SPA  @0 Completitud @5 23
C03 09  X  FRE  @0 Elimination coupure @5 24
C03 09  X  ENG  @0 Cut elimination @5 24
C03 09  X  SPA  @0 Eliminación corte @5 24
C03 10  X  FRE  @0 03B20 @4 INC @5 70
C03 11  X  FRE  @0 03Fxx @4 INC @5 71
C03 12  X  FRE  @0 68T15 @4 INC @5 72
C03 13  X  FRE  @0 Déduction naturelle @4 INC @5 73
C03 14  X  FRE  @0 Procédure décision @4 INC @5 74
N21       @1 023
N44 01      @1 OTO
N82       @1 OTO

Format Inist (serveur)

NO : PASCAL 12-0044340 INIST
ET : Sequent calculi and decidability for intuitionistic hybrid logic
AU : GALMICHE (Didier); SALHI (Yakoub); DE PAIVA (Valeria); PIENTKA (Brigitte)
AF : LORIA- UHP Nancy 1, Campus Scientifique, BP239/54 506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut.); Rearden Commerce/Foster City, CA/Etats-Unis (1 aut.); School of Computer Science, McGill University/Canada (2 aut.)
DT : Publication en série; Niveau analytique
SO : Information and computation : (Print); ISSN 0890-5401; Coden INFCEC; Pays-Bas; Da. 2011; Vol. 209; No. 12; Pp. 1447-1463; Bibl. 19 ref.
LA : Anglais
EA : In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for IHL and then prove its decidability.
CC : 001D02A08; 001A02A01B; 001A02A01F; 001D02C02
FD : Informatique théorique; Décidabilité; Logique intuitionniste; Théorie preuve; Théorie constructive; Calcul séquent; Consistance sémantique; Complétude; Elimination coupure; 03B20; 03Fxx; 68T15; Déduction naturelle; Procédure décision
ED : Computer theory; Decidability; Intuitionistic logic; Proof theory; Constructive theory; Sequent calculus; Soundness; Completeness; Cut elimination
SD : Informática teórica; Decidibilidad; Lógica intuicionista; Teoría demonstración; Teoría constructiva; Càlculo sequente; Consistencia semantica; Completitud; Eliminación corte
LO : INIST-8341.354000505693010020
ID : 12-0044340

Links to Exploration step

Pascal:12-0044340

Le document en format XML

<record>
<TEI>
<teiHeader>
<fileDesc>
<titleStmt>
<title xml:lang="en" level="a">Sequent calculi and decidability for intuitionistic hybrid logic</title>
<author>
<name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation>
<inist:fA14 i1="01">
<s1>LORIA- UHP Nancy 1, Campus Scientifique, BP239</s1>
<s2>54 506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author>
<name sortKey="Salhi, Yakoub" sort="Salhi, Yakoub" uniqKey="Salhi Y" first="Yakoub" last="Salhi">Yakoub Salhi</name>
<affiliation>
<inist:fA14 i1="01">
<s1>LORIA- UHP Nancy 1, Campus Scientifique, BP239</s1>
<s2>54 506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt>
<idno type="wicri:source">INIST</idno>
<idno type="inist">12-0044340</idno>
<date when="2011">2011</date>
<idno type="stanalyst">PASCAL 12-0044340 INIST</idno>
<idno type="RBID">Pascal:12-0044340</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000129</idno>
</publicationStmt>
<sourceDesc>
<biblStruct>
<analytic>
<title xml:lang="en" level="a">Sequent calculi and decidability for intuitionistic hybrid logic</title>
<author>
<name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation>
<inist:fA14 i1="01">
<s1>LORIA- UHP Nancy 1, Campus Scientifique, BP239</s1>
<s2>54 506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author>
<name sortKey="Salhi, Yakoub" sort="Salhi, Yakoub" uniqKey="Salhi Y" first="Yakoub" last="Salhi">Yakoub Salhi</name>
<affiliation>
<inist:fA14 i1="01">
<s1>LORIA- UHP Nancy 1, Campus Scientifique, BP239</s1>
<s2>54 506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series>
<title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
<imprint>
<date when="2011">2011</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt>
<title level="j" type="main">Information and computation : (Print)</title>
<title level="j" type="abbreviated">Inf. comput. : (Print)</title>
<idno type="ISSN">0890-5401</idno>
</seriesStmt>
</fileDesc>
<profileDesc>
<textClass>
<keywords scheme="KwdEn" xml:lang="en">
<term>Completeness</term>
<term>Computer theory</term>
<term>Constructive theory</term>
<term>Cut elimination</term>
<term>Decidability</term>
<term>Intuitionistic logic</term>
<term>Proof theory</term>
<term>Sequent calculus</term>
<term>Soundness</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr">
<term>Informatique théorique</term>
<term>Décidabilité</term>
<term>Logique intuitionniste</term>
<term>Théorie preuve</term>
<term>Théorie constructive</term>
<term>Calcul séquent</term>
<term>Consistance sémantique</term>
<term>Complétude</term>
<term>Elimination coupure</term>
<term>03B20</term>
<term>03Fxx</term>
<term>68T15</term>
<term>Déduction naturelle</term>
<term>Procédure décision</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front>
<div type="abstract" xml:lang="en">In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for
<sub>IHL</sub>
and then prove its decidabilit
<sup>y</sup>
.</div>
</front>
</TEI>
<inist>
<standard h6="B">
<pA>
<fA01 i1="01" i2="1">
<s0>0890-5401</s0>
</fA01>
<fA02 i1="01">
<s0>INFCEC</s0>
</fA02>
<fA03 i2="1">
<s0>Inf. comput. : (Print)</s0>
</fA03>
<fA05>
<s2>209</s2>
</fA05>
<fA06>
<s2>12</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG">
<s1>Sequent calculi and decidability for intuitionistic hybrid logic</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG">
<s1>Intuitionistic Modal Logic and Applications (IMLA 2008)</s1>
</fA09>
<fA11 i1="01" i2="1">
<s1>GALMICHE (Didier)</s1>
</fA11>
<fA11 i1="02" i2="1">
<s1>SALHI (Yakoub)</s1>
</fA11>
<fA12 i1="01" i2="1">
<s1>DE PAIVA (Valeria)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1">
<s1>PIENTKA (Brigitte)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01">
<s1>LORIA- UHP Nancy 1, Campus Scientifique, BP239</s1>
<s2>54 506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</fA14>
<fA15 i1="01">
<s1>Rearden Commerce</s1>
<s2>Foster City, CA</s2>
<s3>USA</s3>
<sZ>1 aut.</sZ>
</fA15>
<fA15 i1="02">
<s1>School of Computer Science, McGill University</s1>
<s3>CAN</s3>
<sZ>2 aut.</sZ>
</fA15>
<fA20>
<s1>1447-1463</s1>
</fA20>
<fA21>
<s1>2011</s1>
</fA21>
<fA23 i1="01">
<s0>ENG</s0>
</fA23>
<fA43 i1="01">
<s1>INIST</s1>
<s2>8341</s2>
<s5>354000505693010020</s5>
</fA43>
<fA44>
<s0>0000</s0>
<s1>© 2012 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45>
<s0>19 ref.</s0>
</fA45>
<fA47 i1="01" i2="1">
<s0>12-0044340</s0>
</fA47>
<fA60>
<s1>P</s1>
</fA60>
<fA61>
<s0>A</s0>
</fA61>
<fA64 i1="01" i2="1">
<s0>Information and computation : (Print)</s0>
</fA64>
<fA66 i1="01">
<s0>NLD</s0>
</fA66>
<fC01 i1="01" l="ENG">
<s0>In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for
<sub>IHL</sub>
and then prove its decidabilit
<sup>y</sup>
.</s0>
</fC01>
<fC02 i1="01" i2="X">
<s0>001D02A08</s0>
</fC02>
<fC02 i1="02" i2="X">
<s0>001A02A01B</s0>
</fC02>
<fC02 i1="03" i2="X">
<s0>001A02A01F</s0>
</fC02>
<fC02 i1="04" i2="X">
<s0>001D02C02</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE">
<s0>Informatique théorique</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG">
<s0>Computer theory</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA">
<s0>Informática teórica</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE">
<s0>Décidabilité</s0>
<s5>17</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG">
<s0>Decidability</s0>
<s5>17</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA">
<s0>Decidibilidad</s0>
<s5>17</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE">
<s0>Logique intuitionniste</s0>
<s5>18</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG">
<s0>Intuitionistic logic</s0>
<s5>18</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA">
<s0>Lógica intuicionista</s0>
<s5>18</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE">
<s0>Théorie preuve</s0>
<s5>19</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG">
<s0>Proof theory</s0>
<s5>19</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA">
<s0>Teoría demonstración</s0>
<s5>19</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE">
<s0>Théorie constructive</s0>
<s5>20</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG">
<s0>Constructive theory</s0>
<s5>20</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA">
<s0>Teoría constructiva</s0>
<s5>20</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE">
<s0>Calcul séquent</s0>
<s5>21</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG">
<s0>Sequent calculus</s0>
<s5>21</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA">
<s0>Càlculo sequente</s0>
<s5>21</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE">
<s0>Consistance sémantique</s0>
<s5>22</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG">
<s0>Soundness</s0>
<s5>22</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA">
<s0>Consistencia semantica</s0>
<s5>22</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE">
<s0>Complétude</s0>
<s5>23</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG">
<s0>Completeness</s0>
<s5>23</s5>
</fC03>
<fC03 i1="08" i2="X" l="SPA">
<s0>Completitud</s0>
<s5>23</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE">
<s0>Elimination coupure</s0>
<s5>24</s5>
</fC03>
<fC03 i1="09" i2="X" l="ENG">
<s0>Cut elimination</s0>
<s5>24</s5>
</fC03>
<fC03 i1="09" i2="X" l="SPA">
<s0>Eliminación corte</s0>
<s5>24</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE">
<s0>03B20</s0>
<s4>INC</s4>
<s5>70</s5>
</fC03>
<fC03 i1="11" i2="X" l="FRE">
<s0>03Fxx</s0>
<s4>INC</s4>
<s5>71</s5>
</fC03>
<fC03 i1="12" i2="X" l="FRE">
<s0>68T15</s0>
<s4>INC</s4>
<s5>72</s5>
</fC03>
<fC03 i1="13" i2="X" l="FRE">
<s0>Déduction naturelle</s0>
<s4>INC</s4>
<s5>73</s5>
</fC03>
<fC03 i1="14" i2="X" l="FRE">
<s0>Procédure décision</s0>
<s4>INC</s4>
<s5>74</s5>
</fC03>
<fN21>
<s1>023</s1>
</fN21>
<fN44 i1="01">
<s1>OTO</s1>
</fN44>
<fN82>
<s1>OTO</s1>
</fN82>
</pA>
</standard>
<server>
<NO>PASCAL 12-0044340 INIST</NO>
<ET>Sequent calculi and decidability for intuitionistic hybrid logic</ET>
<AU>GALMICHE (Didier); SALHI (Yakoub); DE PAIVA (Valeria); PIENTKA (Brigitte)</AU>
<AF>LORIA- UHP Nancy 1, Campus Scientifique, BP239/54 506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut.); Rearden Commerce/Foster City, CA/Etats-Unis (1 aut.); School of Computer Science, McGill University/Canada (2 aut.)</AF>
<DT>Publication en série; Niveau analytique</DT>
<SO>Information and computation : (Print); ISSN 0890-5401; Coden INFCEC; Pays-Bas; Da. 2011; Vol. 209; No. 12; Pp. 1447-1463; Bibl. 19 ref.</SO>
<LA>Anglais</LA>
<EA>In this paper we study the proof theory of the first constructive version of hybrid logic called Intuitionistic Hybrid Logic (IHL) in order to prove its decidability. In this perspective we propose a sequent-style natural deduction system and then the first sequent calculus for this logic. We prove its main properties like soundness, completeness and also the cut-elimination property. Finally we provide, from our calculus, the first decision procedure for
<sub>IHL</sub>
and then prove its decidabilit
<sup>y</sup>
.</EA>
<CC>001D02A08; 001A02A01B; 001A02A01F; 001D02C02</CC>
<FD>Informatique théorique; Décidabilité; Logique intuitionniste; Théorie preuve; Théorie constructive; Calcul séquent; Consistance sémantique; Complétude; Elimination coupure; 03B20; 03Fxx; 68T15; Déduction naturelle; Procédure décision</FD>
<ED>Computer theory; Decidability; Intuitionistic logic; Proof theory; Constructive theory; Sequent calculus; Soundness; Completeness; Cut elimination</ED>
<SD>Informática teórica; Decidibilidad; Lógica intuicionista; Teoría demonstración; Teoría constructiva; Càlculo sequente; Consistencia semantica; Completitud; Eliminación corte</SD>
<LO>INIST-8341.354000505693010020</LO>
<ID>12-0044340</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000129 | SxmlIndent | more

Ou

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000129 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |type=    RBID
   |clé=     Pascal:12-0044340
   |texte=   Sequent calculi and decidability for intuitionistic hybrid logic
}}
Wicri

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022