Sequent calculi and decidability for intuitionistic hybrid logic
Identifieur interne : 002846 ( Main/Merge ); précédent : 002845; suivant : 002847Sequent calculi and decidability for intuitionistic hybrid logic
Auteurs : Didier Galmiche [France] ; Yakoub Salhi [France]Source :
- Information and computation : (Print) [ 0890-5401 ] ; 2011.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
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.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000129
- to stream PascalFrancis, to step Curation: 000882
- to stream PascalFrancis, to step Checkpoint: 000122
Links to Exploration step
Pascal:12-0044340Le 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 wicri:level="1"><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>
<country>France</country>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
<wicri:noRegion>BP239</wicri:noRegion>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Salhi, Yakoub" sort="Salhi, Yakoub" uniqKey="Salhi Y" first="Yakoub" last="Salhi">Yakoub Salhi</name>
<affiliation wicri:level="1"><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>
<country>France</country>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
<wicri:noRegion>BP239</wicri:noRegion>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
</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>
<idno type="wicri:Area/PascalFrancis/Curation">000882</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000122</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000122</idno>
<idno type="wicri:doubleKey">0890-5401:2011:Galmiche D:sequent:calculi:and</idno>
<idno type="wicri:Area/Main/Merge">002846</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 wicri:level="1"><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>
<country>France</country>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
<wicri:noRegion>BP239</wicri:noRegion>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Salhi, Yakoub" sort="Salhi, Yakoub" uniqKey="Salhi Y" first="Yakoub" last="Salhi">Yakoub Salhi</name>
<affiliation wicri:level="1"><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>
<country>France</country>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
<wicri:noRegion>BP239</wicri:noRegion>
<wicri:noRegion>54 506 Vandœuvre-lès-Nancy</wicri:noRegion>
</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>
<affiliations><list><country><li>France</li>
</country>
</list>
<tree><country name="France"><noRegion><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</noRegion>
<name sortKey="Salhi, Yakoub" sort="Salhi, Yakoub" uniqKey="Salhi Y" first="Yakoub" last="Salhi">Yakoub Salhi</name>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002846 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 002846 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Main |étape= Merge |type= RBID |clé= Pascal:12-0044340 |texte= Sequent calculi and decidability for intuitionistic hybrid logic }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |