Pure Extensions, Proof Rules, and Hybrid Axiomatics
Identifieur interne : 003E58 ( Hal/Corpus ); précédent : 003E57; suivant : 003E59Pure Extensions, Proof Rules, and Hybrid Axiomatics
Auteurs : Patrick Blackburn ; Balder Ten CateSource :
- Studia Logica [ 0039-3215 ] ; 2006.
English descriptors
Abstract
In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language (a decidable system with the same complexity as orthodox propositional modal logic) to the strong Priorean language (which offers full first-order expressivity). We show that hybrid logic offers a genuinely first-order perspective on Kripke semantics: it is possible to define base logics which extend automatically to a wide variety of frame classes and to prove completeness using the Henkin method. In the weaker languages, this requires the use of non-orthodox rules. We discuss these rules in detail and prove non-eliminability and eliminability results. We also show how another type of rule, which reflects the structure of the strong Priorean language, can be employed to give an even wider coverage of frame classes. We show that this deductive apparatus gets progressively simpler as we work our way up the expressivity hierarchy, and conclude the paper by showing that the approach transfers to first-order hybrid logic.
Url:
DOI: 10.1007/s11225-006-9009-6
Links to Exploration step
Hal:inria-00119855Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Pure Extensions, Proof Rules, and Hybrid Axiomatics</title>
<author><name sortKey="Blackburn, Patrick" sort="Blackburn, Patrick" uniqKey="Blackburn P" first="Patrick" last="Blackburn">Patrick Blackburn</name>
<affiliation><hal:affiliation type="researchteam" xml:id="struct-2351" status="OLD"><idno type="RNSR">199421391G</idno>
<orgName>Human-machine dialogue with a significant language component</orgName>
<orgName type="acronym">LANGUE ET DIALOGUE</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
<listRelation><relation active="#struct-160" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="indirect"></relation>
<relation active="#struct-300009" type="indirect"></relation>
<relation active="#struct-300291" type="indirect"></relation>
<relation active="#struct-300292" type="indirect"></relation>
<relation active="#struct-300293" type="indirect"></relation>
<relation active="#struct-2496" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation>
<relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-300291" type="direct"></relation>
<relation active="#struct-300292" type="direct"></relation>
<relation active="#struct-300293" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName>
<orgName type="acronym">UHP</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName>
<orgName type="acronym">INPL</orgName>
<date type="end">2011-12-31</date>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName>
<desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
<author><name sortKey="Ten Cate, Balder" sort="Ten Cate, Balder" uniqKey="Ten Cate B" first="Balder" last="Ten Cate">Balder Ten Cate</name>
<affiliation><hal:affiliation type="laboratory" xml:id="struct-120654" status="VALID"><orgName>University of Amsterdam [Amsterdam]</orgName>
<desc><address><addrLine>Spui 21 1012 WX Amsterdam</addrLine>
<country key="NL"></country>
</address>
<ref type="url">http://www.uva.nl/en/home</ref>
</desc>
<listRelation><relation active="#struct-303011" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-303011" type="direct"><org type="institution" xml:id="struct-303011" status="VALID"><orgName>University of Amsterdam</orgName>
<orgName type="acronym"> UvA</orgName>
<desc><address><country key="NL"></country>
</address>
<ref type="url">https://www.uva.nl/en/home</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">HAL</idno>
<idno type="RBID">Hal:inria-00119855</idno>
<idno type="halId">inria-00119855</idno>
<idno type="halUri">https://hal.inria.fr/inria-00119855</idno>
<idno type="url">https://hal.inria.fr/inria-00119855</idno>
<idno type="doi">10.1007/s11225-006-9009-6</idno>
<date when="2006">2006</date>
<idno type="wicri:Area/Hal/Corpus">003E58</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Pure Extensions, Proof Rules, and Hybrid Axiomatics</title>
<author><name sortKey="Blackburn, Patrick" sort="Blackburn, Patrick" uniqKey="Blackburn P" first="Patrick" last="Blackburn">Patrick Blackburn</name>
<affiliation><hal:affiliation type="researchteam" xml:id="struct-2351" status="OLD"><idno type="RNSR">199421391G</idno>
<orgName>Human-machine dialogue with a significant language component</orgName>
<orgName type="acronym">LANGUE ET DIALOGUE</orgName>
<desc><address><country key="FR"></country>
</address>
</desc>
<listRelation><relation active="#struct-160" type="direct"></relation>
<relation name="UMR7503" active="#struct-441569" type="indirect"></relation>
<relation active="#struct-300009" type="indirect"></relation>
<relation active="#struct-300291" type="indirect"></relation>
<relation active="#struct-300292" type="indirect"></relation>
<relation active="#struct-300293" type="indirect"></relation>
<relation active="#struct-2496" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName>
<orgName type="acronym">LORIA</orgName>
<desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.loria.fr</ref>
</desc>
<listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation>
<relation active="#struct-300009" type="direct"></relation>
<relation active="#struct-300291" type="direct"></relation>
<relation active="#struct-300292" type="direct"></relation>
<relation active="#struct-300293" type="direct"></relation>
</listRelation>
</org>
</tutelle>
<tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno>
<idno type="IdRef">02636817X</idno>
<orgName>Centre National de la Recherche Scientifique</orgName>
<orgName type="acronym">CNRS</orgName>
<date type="start">1939-10-19</date>
<desc><address><country key="FR"></country>
</address>
<ref type="url">http://www.cnrs.fr/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName>
<orgName type="acronym">Inria</orgName>
<desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/en/</ref>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName>
<orgName type="acronym">UHP</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName>
<date type="end">2011-12-31</date>
<desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine>
<country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName>
<orgName type="acronym">INPL</orgName>
<date type="end">2011-12-31</date>
<desc><address><country key="FR"></country>
</address>
</desc>
</org>
</tutelle>
<tutelle active="#struct-2496" type="direct"><org type="laboratory" xml:id="struct-2496" status="OLD"><orgName>INRIA Lorraine</orgName>
<desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine>
<country key="FR"></country>
</address>
<ref type="url">http://www.inria.fr/centre-de-recherche-inria/nancy-grand-est</ref>
</desc>
<listRelation><relation active="#struct-300009" type="direct"></relation>
</listRelation>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
<author><name sortKey="Ten Cate, Balder" sort="Ten Cate, Balder" uniqKey="Ten Cate B" first="Balder" last="Ten Cate">Balder Ten Cate</name>
<affiliation><hal:affiliation type="laboratory" xml:id="struct-120654" status="VALID"><orgName>University of Amsterdam [Amsterdam]</orgName>
<desc><address><addrLine>Spui 21 1012 WX Amsterdam</addrLine>
<country key="NL"></country>
</address>
<ref type="url">http://www.uva.nl/en/home</ref>
</desc>
<listRelation><relation active="#struct-303011" type="direct"></relation>
</listRelation>
<tutelles><tutelle active="#struct-303011" type="direct"><org type="institution" xml:id="struct-303011" status="VALID"><orgName>University of Amsterdam</orgName>
<orgName type="acronym"> UvA</orgName>
<desc><address><country key="NL"></country>
</address>
<ref type="url">https://www.uva.nl/en/home</ref>
</desc>
</org>
</tutelle>
</tutelles>
</hal:affiliation>
</affiliation>
</author>
</analytic>
<idno type="DOI">10.1007/s11225-006-9009-6</idno>
<series><title level="j">Studia Logica</title>
<idno type="ISSN">0039-3215</idno>
<imprint><date type="datePub">2006</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>Hybrid logic</term>
<term>axiomatisation</term>
<term>completeness</term>
<term>modal logic</term>
<term>nominals</term>
<term>proof rules</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language (a decidable system with the same complexity as orthodox propositional modal logic) to the strong Priorean language (which offers full first-order expressivity). We show that hybrid logic offers a genuinely first-order perspective on Kripke semantics: it is possible to define base logics which extend automatically to a wide variety of frame classes and to prove completeness using the Henkin method. In the weaker languages, this requires the use of non-orthodox rules. We discuss these rules in detail and prove non-eliminability and eliminability results. We also show how another type of rule, which reflects the structure of the strong Priorean language, can be employed to give an even wider coverage of frame classes. We show that this deductive apparatus gets progressively simpler as we work our way up the expressivity hierarchy, and conclude the paper by showing that the approach transfers to first-order hybrid logic.</div>
</front>
</TEI>
<hal api="V3"><titleStmt><title xml:lang="en">Pure Extensions, Proof Rules, and Hybrid Axiomatics</title>
<author role="aut"><persName><forename type="first">Patrick</forename>
<surname>Blackburn</surname>
</persName>
<email>patrick.blackburn@loria.fr</email>
<idno type="halauthor">130880</idno>
<orgName ref="#struct-300009"></orgName>
<affiliation ref="#struct-2351"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Balder</forename>
<surname>Ten Cate</surname>
</persName>
<email></email>
<idno type="halauthor">135881</idno>
<affiliation ref="#struct-120654"></affiliation>
</author>
<editor role="depositor"><persName><forename>Patrick</forename>
<surname>Blackburn</surname>
</persName>
<email>patrick.blackburn@loria.fr</email>
</editor>
</titleStmt>
<editionStmt><edition n="v1" type="current"><date type="whenSubmitted">2006-12-12 13:24:43</date>
<date type="whenModified">2016-05-19 01:09:15</date>
<date type="whenReleased">2006-12-12 13:24:43</date>
<date type="whenProduced">2006</date>
</edition>
<respStmt><resp>contributor</resp>
<name key="115178"><persName><forename>Patrick</forename>
<surname>Blackburn</surname>
</persName>
<email>patrick.blackburn@loria.fr</email>
</name>
</respStmt>
</editionStmt>
<publicationStmt><distributor>CCSD</distributor>
<idno type="halId">inria-00119855</idno>
<idno type="halUri">https://hal.inria.fr/inria-00119855</idno>
<idno type="halBibtex">blackburn:inria-00119855</idno>
<idno type="halRefHtml">Studia Logica, Springer Verlag (Germany), 2006, 84 (2), pp.277-322. <10.1007/s11225-006-9009-6></idno>
<idno type="halRef">Studia Logica, Springer Verlag (Germany), 2006, 84 (2), pp.277-322. <10.1007/s11225-006-9009-6></idno>
</publicationStmt>
<seriesStmt><idno type="stamp" n="INRIA">INRIA - Institut National de Recherche en Informatique et en Automatique</idno>
<idno type="stamp" n="CNRS">CNRS - Centre national de la recherche scientifique</idno>
<idno type="stamp" n="INPL">Institut National Polytechnique de Lorraine</idno>
<idno type="stamp" n="INSMI">CNRS-INSMI - INstitut des Sciences Mathématiques et de leurs Interactions</idno>
<idno type="stamp" n="LORIA2">Publications du LORIA</idno>
<idno type="stamp" n="LORIA">LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications</idno>
<idno type="stamp" n="INRIA-NANCY-GRAND-EST">INRIA Nancy - Grand Est</idno>
<idno type="stamp" n="UNIV-LORRAINE">Université de Lorraine</idno>
<idno type="stamp" n="INRIA-LORRAINE">INRIA Nancy - Grand Est</idno>
<idno type="stamp" n="LABO-LORIA-SET" p="LORIA">LABO-LORIA-SET</idno>
</seriesStmt>
<notesStmt><note type="audience" n="1">Not set</note>
<note type="popular" n="0">No</note>
<note type="peer" n="1">Yes</note>
</notesStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Pure Extensions, Proof Rules, and Hybrid Axiomatics</title>
<author role="aut"><persName><forename type="first">Patrick</forename>
<surname>Blackburn</surname>
</persName>
<email>patrick.blackburn@loria.fr</email>
<idno type="halAuthorId">130880</idno>
<orgName ref="#struct-300009"></orgName>
<affiliation ref="#struct-2351"></affiliation>
</author>
<author role="aut"><persName><forename type="first">Balder</forename>
<surname>Ten Cate</surname>
</persName>
<idno type="halAuthorId">135881</idno>
<affiliation ref="#struct-120654"></affiliation>
</author>
</analytic>
<monogr><idno type="halJournalId" status="VALID">19198</idno>
<idno type="issn">0039-3215</idno>
<idno type="eissn">1572-8730</idno>
<title level="j">Studia Logica</title>
<imprint><publisher>Springer Verlag (Germany)</publisher>
<biblScope unit="volume">84</biblScope>
<biblScope unit="issue">2</biblScope>
<biblScope unit="pp">277-322</biblScope>
<date type="datePub">2006</date>
</imprint>
</monogr>
<idno type="doi">10.1007/s11225-006-9009-6</idno>
</biblStruct>
</sourceDesc>
<profileDesc><langUsage><language ident="en">English</language>
</langUsage>
<textClass><keywords scheme="author"><term xml:lang="en">Hybrid logic</term>
<term xml:lang="en">modal logic</term>
<term xml:lang="en">nominals</term>
<term xml:lang="en">axiomatisation</term>
<term xml:lang="en">completeness</term>
<term xml:lang="en">proof rules</term>
</keywords>
<classCode scheme="acm" n="A"></classCode>
<classCode scheme="halDomain" n="math.math-lo">Mathematics [math]/Logic [math.LO]</classCode>
<classCode scheme="halTypology" n="ART">Journal articles</classCode>
</textClass>
<abstract xml:lang="en">In this paper we argue that hybrid logic is the deductive setting most natural for Kripke semantics. We do so by investigating hybrid axiomatics for a variety of systems, ranging from the basic hybrid language (a decidable system with the same complexity as orthodox propositional modal logic) to the strong Priorean language (which offers full first-order expressivity). We show that hybrid logic offers a genuinely first-order perspective on Kripke semantics: it is possible to define base logics which extend automatically to a wide variety of frame classes and to prove completeness using the Henkin method. In the weaker languages, this requires the use of non-orthodox rules. We discuss these rules in detail and prove non-eliminability and eliminability results. We also show how another type of rule, which reflects the structure of the strong Priorean language, can be employed to give an even wider coverage of frame classes. We show that this deductive apparatus gets progressively simpler as we work our way up the expressivity hierarchy, and conclude the paper by showing that the approach transfers to first-order hybrid logic.</abstract>
</profileDesc>
</hal>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Hal/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003E58 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Hal/Corpus/biblio.hfd -nk 003E58 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Hal |étape= Corpus |type= RBID |clé= Hal:inria-00119855 |texte= Pure Extensions, Proof Rules, and Hybrid Axiomatics }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |