Characterizing Provability in BI ’s Pointer Logic Through Resource Graphs
Identifieur interne : 006291 ( Main/Exploration ); précédent : 006290; suivant : 006292Characterizing 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 ]
Descripteurs français
- Pascal (Inist)
- Wicri :
- topic : Intelligence artificielle.
English descriptors
- KwdEn :
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:
DOI: 10.1007/11591191_32
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002D88
- to stream Istex, to step Curation: 002D51
- to stream Istex, to step Checkpoint: 001605
- to stream Main, to step Merge: 006516
- to stream PascalFrancis, to step Corpus: 000486
- to stream PascalFrancis, to step Curation: 000547
- to stream PascalFrancis, to step Checkpoint: 000516
- to stream Main, to step Merge: 006653
- to stream Main, to step Curation: 006291
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><idno type="wicri:Area/Main/Exploration">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><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="Méry">Daniel Méry</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 006291 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/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= Exploration
|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. |  |