Characterizing provability in BI's pointer logic through resource graphs
Identifieur interne : 000516 ( PascalFrancis/Checkpoint ); précédent : 000515; suivant : 000517Characterizing provability in BI's pointer logic through resource graphs
Auteurs : Didier Galmiche [France] ; Daniel Mery [France]Source :
- Lecture notes in computer science [ 0302-9743 ] ; 2005.
Descripteurs français
- Pascal (Inist)
- Wicri :
- topic : Intelligence artificielle.
English descriptors
- KwdEn :
Abstract
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.
Affiliations:
Links toward previous steps (curation, corpus...)
Links to Exploration step
Pascal:06-0063189Le document en format XML
<record><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></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><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0></fA01><fA05><s2>3835</s2></fA05><fA08 i1="01" i2="1" l="ENG"><s1>Characterizing provability in BI's pointer logic through resource graphs</s1></fA08><fA09 i1="01" i2="1" l="ENG"><s1>Logic for programming, artificial intelligence, and reasoning : 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005 : Proceedings</s1></fA09><fA11 i1="01" i2="1"><s1>GALMICHE (Didier)</s1></fA11><fA11 i1="02" i2="1"><s1>MERY (Daniel)</s1></fA11><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></fA14><fA20><s1>459-473</s1></fA20><fA21><s1>2005</s1></fA21><fA23 i1="01"><s0>ENG</s0></fA23><fA26 i1="01"><s0>3-540-30553-X</s0></fA26><fA43 i1="01"><s1>INIST</s1><s2>16343</s2><s5>354000138672300310</s5></fA43><fA44><s0>0000</s0><s1>© 2006 INIST-CNRS. All rights reserved.</s1></fA44><fA45><s0>12 ref.</s0></fA45><fA47 i1="01" i2="1"><s0>06-0063189</s0></fA47><fA60><s1>P</s1><s2>C</s2></fA60><fA61><s0>A</s0></fA61><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0></fA64><fA66 i1="01"><s0>DEU</s0></fA66><fC01 i1="01" l="ENG"><s0>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.</s0></fC01><fC02 i1="01" i2="X"><s0>001D02C</s0></fC02><fC02 i1="02" i2="X"><s0>001D02A04</s0></fC02><fC03 i1="01" i2="X" l="FRE"><s0>Programmation logique</s0><s5>06</s5></fC03><fC03 i1="01" i2="X" l="ENG"><s0>Logical programming</s0><s5>06</s5></fC03><fC03 i1="01" i2="X" l="SPA"><s0>Programación lógica</s0><s5>06</s5></fC03><fC03 i1="02" i2="X" l="FRE"><s0>Intelligence artificielle</s0><s5>07</s5></fC03><fC03 i1="02" i2="X" l="ENG"><s0>Artificial intelligence</s0><s5>07</s5></fC03><fC03 i1="02" i2="X" l="SPA"><s0>Inteligencia artificial</s0><s5>07</s5></fC03><fC03 i1="03" i2="X" l="FRE"><s0>Structure donnée</s0><s5>08</s5></fC03><fC03 i1="03" i2="X" l="ENG"><s0>Data structure</s0><s5>08</s5></fC03><fC03 i1="03" i2="X" l="SPA"><s0>Estructura datos</s0><s5>08</s5></fC03><fC03 i1="04" i2="X" l="FRE"><s0>Etiquetage</s0><s5>09</s5></fC03><fC03 i1="04" i2="X" l="ENG"><s0>Labelling</s0><s5>09</s5></fC03><fC03 i1="04" i2="X" l="SPA"><s0>Etiquetaje</s0><s5>09</s5></fC03><fC03 i1="05" i2="X" l="FRE"><s0>Pointeur</s0><s5>18</s5></fC03><fC03 i1="05" i2="X" l="ENG"><s0>Pointer</s0><s5>18</s5></fC03><fC03 i1="05" i2="X" l="SPA"><s0>Marcador</s0><s5>18</s5></fC03><fC03 i1="06" i2="X" l="FRE"><s0>Sémantique</s0><s5>19</s5></fC03><fC03 i1="06" i2="X" l="ENG"><s0>Semantics</s0><s5>19</s5></fC03><fC03 i1="06" i2="X" l="SPA"><s0>Semántica</s0><s5>19</s5></fC03><fC03 i1="07" i2="X" l="FRE"><s0>Appel procédure</s0><s5>20</s5></fC03><fC03 i1="07" i2="X" l="ENG"><s0>Procedure call</s0><s5>20</s5></fC03><fC03 i1="07" i2="X" l="SPA"><s0>Llamada procedimiento</s0><s5>20</s5></fC03><fC03 i1="08" i2="X" l="FRE"><s0>Multigraphe</s0><s5>23</s5></fC03><fC03 i1="08" i2="X" l="ENG"><s0>Multigraph</s0><s5>23</s5></fC03><fC03 i1="08" i2="X" l="SPA"><s0>Multígrafo</s0><s5>23</s5></fC03><fC03 i1="09" i2="X" l="FRE"><s0>Modélisation</s0><s5>24</s5></fC03><fC03 i1="09" i2="X" l="ENG"><s0>Modeling</s0><s5>24</s5></fC03><fC03 i1="09" i2="X" l="SPA"><s0>Modelización</s0><s5>24</s5></fC03><fC03 i1="10" i2="X" l="FRE"><s0>Théorie graphe</s0><s5>25</s5></fC03><fC03 i1="10" i2="X" l="ENG"><s0>Graph theory</s0><s5>25</s5></fC03><fC03 i1="10" i2="X" l="SPA"><s0>Teoría grafo</s0><s5>25</s5></fC03><fN21><s1>037</s1></fN21><fN44 i1="01"><s1>OTO</s1></fN44><fN82><s1>OTO</s1></fN82></pA><pR><fA30 i1="01" i2="1" l="ENG"><s1>Logic for programming, artificial intelligence, and reasoning. International conference</s1><s2>12</s2><s3>Montego Bay JAM</s3><s4>2005-12-02</s4></fA30></pR></standard></inist><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Nancy</li><li>Vandœuvre-lès-Nancy</li></settlement><orgName><li>Université Henri Poincaré</li></orgName></list><tree><country name="France"><region name="Grand Est"><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name></region><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Mery">Daniel Mery</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000516 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Checkpoint/biblio.hfd -nk 000516 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= PascalFrancis
|étape= Checkpoint
|type= RBID
|clé= Pascal:06-0063189
|texte= Characterizing provability in BI's pointer logic through resource graphs
}}
| This area was generated with Dilib version V0.6.33. |  |