InforLorV4, Main, Curation, bibRecord, 006291

Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs

Identifieur interne : 006291 ( Main/Curation ); précédent : 006290; suivant : 006292

Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs

Auteurs : Didier Galmiche [France] ; Daniel Méry [France]

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:C1B5391D5C9CA108ECDEC7EE18C205AE779B3237

Descripteurs français

Pascal (Inist)
- Appel procédure, Etiquetage, Intelligence artificielle, Modélisation, Multigraphe, Pointeur, Programmation logique, Structure donnée, Sémantique, Théorie graphe.
Wicri :
- topic : Intelligence artificielle.

English descriptors

KwdEn :
- Artificial intelligence, Data structure, Graph theory, Labelling, Logical programming, Modeling, Multigraph, Pointer, Procedure call, Semantics.

Abstract

Abstract: We propose a characterization of provability in BI’s Pointer Logic (PL) that is based on semantic structures called resource graphs. This logic has been defined for reasoning about mutable data structures and results about models and verification have been already provided. Here, we define resource graphs that capture PL models by considering heaps as resources and by using a labelling process. We study provability in PL from a new calculus that builds such graphs from which proofs or countermodels can be generated. Properties of soundness and completeness are proved and the countermodel generation is studied.

Url:

https://api.istex.fr/ark:/67375/HCB-WJQK55N7-H/fulltext.pdf

DOI: 10.1007/11591191_32

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

to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :002D88
to stream Istex, to step Curation: Pour aller vers cette notice dans l'étape Curation :002D51
to stream Istex, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :001605
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :006516
to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000486
to stream PascalFrancis, to step Curation: Pour aller vers cette notice dans l'étape Curation :000547
to stream PascalFrancis, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :000516
to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :006653

Links to Exploration step

ISTEX:C1B5391D5C9CA108ECDEC7EE18C205AE779B3237

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:C1B5391D5C9CA108ECDEC7EE18C205AE779B3237</idno>
<date when="2005" year="2005">2005</date>
<idno type="doi">10.1007/11591191_32</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-WJQK55N7-H/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002D88</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002D88</idno>
<idno type="wicri:Area/Istex/Curation">002D51</idno>
<idno type="wicri:Area/Istex/Checkpoint">001605</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001605</idno>
<idno type="wicri:doubleKey">0302-9743:2005:Galmiche D:characterizing:provability:in</idno>
<idno type="wicri:Area/Main/Merge">006516</idno>
<idno type="wicri:source">INIST</idno>
<idno type="RBID">Pascal:06-0063189</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000486</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000547</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000516</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000516</idno>
<idno type="wicri:doubleKey">0302-9743:2005:Galmiche D:characterizing:provability:in</idno>
<idno type="wicri:Area/Main/Merge">006653</idno>
<idno type="wicri:Area/Main/Curation">006291</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Characterizing Provability in <hi rend="SansSerif">BI</hi>
’s Pointer Logic Through Resource Graphs</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Artificial intelligence</term>
<term>Data structure</term>
<term>Graph theory</term>
<term>Labelling</term>
<term>Logical programming</term>
<term>Modeling</term>
<term>Multigraph</term>
<term>Pointer</term>
<term>Procedure call</term>
<term>Semantics</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Appel procédure</term>
<term>Etiquetage</term>
<term>Intelligence artificielle</term>
<term>Modélisation</term>
<term>Multigraphe</term>
<term>Pointeur</term>
<term>Programmation logique</term>
<term>Structure donnée</term>
<term>Sémantique</term>
<term>Théorie graphe</term>
</keywords>
<keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Intelligence artificielle</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We propose a characterization of provability in BI’s Pointer Logic (PL) that is based on semantic structures called resource graphs. This logic has been defined for reasoning about mutable data structures and results about models and verification have been already provided. Here, we define resource graphs that capture PL models by considering heaps as resources and by using a labelling process. We study provability in PL from a new calculus that builds such graphs from which proofs or countermodels can be generated. Properties of soundness and completeness are proved and the countermodel generation is studied.</div>
</front>
</TEI>
<double idat="0302-9743:2005:Galmiche D:characterizing:provability:in"><INIST><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Characterizing provability in BI's pointer logic through resource graphs</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239</s1>
<s2>Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239</s1>
<s2>Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">06-0063189</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 06-0063189 INIST</idno>
<idno type="RBID">Pascal:06-0063189</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000486</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000547</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000516</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000516</idno>
<idno type="wicri:doubleKey">0302-9743:2005:Galmiche D:characterizing:provability:in</idno>
<idno type="wicri:Area/Main/Merge">006653</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Characterizing provability in BI's pointer logic through resource graphs</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239</s1>
<s2>Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name>
<affiliation wicri:level="4"><inist:fA14 i1="01"><s1>LORIA - Université Henri Poincaré, Campus Scientifique, BP 239</s1>
<s2>Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2005">2005</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Artificial intelligence</term>
<term>Data structure</term>
<term>Graph theory</term>
<term>Labelling</term>
<term>Logical programming</term>
<term>Modeling</term>
<term>Multigraph</term>
<term>Pointer</term>
<term>Procedure call</term>
<term>Semantics</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Programmation logique</term>
<term>Intelligence artificielle</term>
<term>Structure donnée</term>
<term>Etiquetage</term>
<term>Pointeur</term>
<term>Sémantique</term>
<term>Appel procédure</term>
<term>Multigraphe</term>
<term>Modélisation</term>
<term>Théorie graphe</term>
</keywords>
<keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Intelligence artificielle</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We propose a characterization of provability in Bl's Pointer Logic (PL) that is based on semantic structures called resource graphs. This logic has been defined for reasoning about mutable data structures and results about models and verification have been already provided. Here, we define resource graphs that capture PL models by considering heaps as resources and by using a labelling process. We study provability in PL from a new calculus that builds such graphs from which proofs or countermodels can be generated. Properties of soundness and completeness are proved and the countermodel generation is studied.</div>
</front>
</TEI>
</INIST>
<ISTEX><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:C1B5391D5C9CA108ECDEC7EE18C205AE779B3237</idno>
<date when="2005" year="2005">2005</date>
<idno type="doi">10.1007/11591191_32</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-WJQK55N7-H/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">002D88</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002D88</idno>
<idno type="wicri:Area/Istex/Curation">002D51</idno>
<idno type="wicri:Area/Istex/Checkpoint">001605</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001605</idno>
<idno type="wicri:doubleKey">0302-9743:2005:Galmiche D:characterizing:provability:in</idno>
<idno type="wicri:Area/Main/Merge">006516</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Characterizing Provability in <hi rend="SansSerif">BI</hi>
’s Pointer Logic Through Resource Graphs</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
<affiliation wicri:level="4"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA – Université Henri Poincaré, Campus Scientifique, BP 239, Vandœuvre-lès-Nancy</wicri:regionArea>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
<settlement type="city" wicri:auto="agglo">Nancy</settlement>
</placeName>
<orgName type="university">Université Henri Poincaré</orgName>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="eISSN">1611-3349</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We propose a characterization of provability in BI’s Pointer Logic (PL) that is based on semantic structures called resource graphs. This logic has been defined for reasoning about mutable data structures and results about models and verification have been already provided. Here, we define resource graphs that capture PL models by considering heaps as resources and by using a labelling process. We study provability in PL from a new calculus that builds such graphs from which proofs or countermodels can be generated. Properties of soundness and completeness are proved and the countermodel generation is studied.</div>
</front>
</TEI>
</ISTEX>
</double>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation

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

HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 006291 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Curation
   |type=    RBID
   |clé=     ISTEX:C1B5391D5C9CA108ECDEC7EE18C205AE779B3237
   |texte=   Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs
}}

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

Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs

Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs

Source :

Descripteurs français

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