InforLorV4, Main, Merge, bibRecord, 005394

Pure Extensions, Proof Rules, and Hybrid Axiomatics

Identifieur interne : 005394 ( Main/Merge ); précédent : 005393; suivant : 005395

Pure Extensions, Proof Rules, and Hybrid Axiomatics

Auteurs : Patrick Blackburn [France] ; Balder Ten Cate [Pays-Bas]

Source :

Studia Logica [ 0039-3215 ] ; 2006.

RBID : Hal:inria-00119855

English descriptors

mix :
- Hybrid logic, axiomatisation, completeness, modal logic, nominals, proof rules.

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:

https://hal.inria.fr/inria-00119855

DOI: 10.1007/s11225-006-9009-6

Links toward previous steps (curation, corpus...)

to stream Hal, to step Corpus: 003E58
to stream Hal, to step Curation: 003E58
to stream Hal, to step Checkpoint: 004292

Links to Exploration step

Hal:inria-00119855

Le 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 wicri:level="1"><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>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Nancy 2</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Institut national polytechnique de Lorraine</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
</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 wicri:level="1"><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>
<country>Pays-Bas</country>
<placeName><settlement type="city">Amsterdam</settlement>
<region>Hollande-Septentrionale</region>
</placeName>
<orgName type="university">Université d'Amsterdam</orgName>
</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>
<idno type="wicri:Area/Hal/Curation">003E58</idno>
<idno type="wicri:Area/Hal/Checkpoint">004292</idno>
<idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">004292</idno>
<idno type="wicri:doubleKey">0039-3215:2006:Blackburn P:pure:extensions:proof</idno>
<idno type="wicri:Area/Main/Merge">005394</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 wicri:level="1"><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>
<country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Nancy 2</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Institut national polytechnique de Lorraine</orgName>
<orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName>
</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 wicri:level="1"><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>
<country>Pays-Bas</country>
<placeName><settlement type="city">Amsterdam</settlement>
<region>Hollande-Septentrionale</region>
</placeName>
<orgName type="university">Université d'Amsterdam</orgName>
</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>
</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 005394 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 005394 | 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é=     Hal:inria-00119855
   |texte=   Pure Extensions, Proof Rules, and Hybrid Axiomatics
}}

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

	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.

Serveur d'exploration sur la recherche en informatique en Lorraine

Pure Extensions, Proof Rules, and Hybrid Axiomatics

Pure Extensions, Proof Rules, and Hybrid Axiomatics

Source :

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

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