InforLorV4, Istex, Corpus, bibRecord, 003B22

Resource Tableaux

Identifieur interne : 003B22 ( Istex/Corpus ); précédent : 003B21; suivant : 003B23

Resource Tableaux

Auteurs : Didier Galmiche ; Daniel Méry ; David Pym

Source :

Lecture Notes in Computer Science [ 0302-9743 ]

RBID : ISTEX:F71E0B68369621B1437F3428CF7C75CDD1007685

Abstract

Abstract: The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource rich enough to provide a “pointer logic” semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI’s tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, ⊥, the challenge consists in dealing with BI’s Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. As consequences, we have two strong new results for BI: the decidability of propositional BI and the finite model property with respect to Grothendieck topological semantics. In addition, we propose, by considering partially defined monoids, a new semantics which generalizes the semantics of BI’s pointer logic and for which BI is complete

Url:

https://api.istex.fr/ark:/67375/HCB-DS02CDVK-S/fulltext.pdf

DOI: 10.1007/3-540-45793-3_13

Links to Exploration step

ISTEX:F71E0B68369621B1437F3428CF7C75CDD1007685

Le document en format XML

<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Resource Tableaux</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: galmiche@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: dmery@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Pym, David" sort="Pym, David" uniqKey="Pym D" first="David" last="Pym">David Pym</name>
<affiliation><mods:affiliation>University of Bath, England</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: d.j.pym@bath.ac.uk</mods:affiliation>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:F71E0B68369621B1437F3428CF7C75CDD1007685</idno>
<date when="2002" year="2002">2002</date>
<idno type="doi">10.1007/3-540-45793-3_13</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-DS02CDVK-S/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">003B22</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003B22</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Resource Tableaux</title>
<author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: galmiche@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Mery, Daniel" sort="Mery, Daniel" uniqKey="Mery D" first="Daniel" last="Méry">Daniel Méry</name>
<affiliation><mods:affiliation>LORIA, Nancy, France</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: dmery@loria.fr</mods:affiliation>
</affiliation>
</author>
<author><name sortKey="Pym, David" sort="Pym, David" uniqKey="Pym D" first="David" last="Pym">David Pym</name>
<affiliation><mods:affiliation>University of Bath, England</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: d.j.pym@bath.ac.uk</mods:affiliation>
</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="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: The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource rich enough to provide a “pointer logic” semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI’s tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, ⊥, the challenge consists in dealing with BI’s Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. As consequences, we have two strong new results for BI: the decidability of propositional BI and the finite model property with respect to Grothendieck topological semantics. In addition, we propose, by considering partially defined monoids, a new semantics which generalizes the semantics of BI’s pointer logic and for which BI is complete</div>
</front>
</TEI>
<istex><corpusName>springer-ebooks</corpusName>
<author><json:item><name>Didier Galmiche</name>
<affiliations><json:string>LORIA, Nancy, France</json:string>
<json:string>E-mail: galmiche@loria.fr</json:string>
</affiliations>
</json:item>
<json:item><name>Daniel Méry</name>
<affiliations><json:string>LORIA, Nancy, France</json:string>
<json:string>E-mail: dmery@loria.fr</json:string>
</affiliations>
</json:item>
<json:item><name>David Pym</name>
<affiliations><json:string>University of Bath, England</json:string>
<json:string>E-mail: d.j.pym@bath.ac.uk</json:string>
</affiliations>
</json:item>
</author>
<subject><json:item><lang><json:string>eng</json:string>
</lang>
<value>BI</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>resources</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>semantics</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>tableaux</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>decidability</value>
</json:item>
<json:item><lang><json:string>eng</json:string>
</lang>
<value>finite model property</value>
</json:item>
</subject>
<arkIstex>ark:/67375/HCB-DS02CDVK-S</arkIstex>
<language><json:string>eng</json:string>
</language>
<originalGenre><json:string>OriginalPaper</json:string>
</originalGenre>
<abstract>Abstract: The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource rich enough to provide a “pointer logic” semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI’s tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, ⊥, the challenge consists in dealing with BI’s Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. As consequences, we have two strong new results for BI: the decidability of propositional BI and the finite model property with respect to Grothendieck topological semantics. In addition, we propose, by considering partially defined monoids, a new semantics which generalizes the semantics of BI’s pointer logic and for which BI is complete</abstract>
<qualityIndicators><score>9.196</score>
<pdfWordCount>8053</pdfWordCount>
<pdfCharCount>34576</pdfCharCount>
<pdfVersion>1.3</pdfVersion>
<pdfPageCount>17</pdfPageCount>
<pdfPageSize>451 x 677 pts</pdfPageSize>
<refBibsNative>false</refBibsNative>
<abstractWordCount>183</abstractWordCount>
<abstractCharCount>1179</abstractCharCount>
<keywordCount>6</keywordCount>
</qualityIndicators>
<title>Resource Tableaux</title>
<chapterId><json:string>13</json:string>
<json:string>Chap13</json:string>
</chapterId>
<genre><json:string>conference</json:string>
</genre>
<serie><title>Lecture Notes in Computer Science</title>
<language><json:string>unknown</json:string>
</language>
<copyrightDate>2002</copyrightDate>
<issn><json:string>0302-9743</json:string>
</issn>
<editor><json:item><name>Gerhard Goos</name>
<affiliations><json:string>Karlsruhe University, Germany</json:string>
</affiliations>
</json:item>
<json:item><name>Juris Hartmanis</name>
<affiliations><json:string>Cornell University, NY, USA</json:string>
</affiliations>
</json:item>
<json:item><name>Jan van Leeuwen</name>
<affiliations><json:string>Utrecht University, The Netherlands</json:string>
</affiliations>
</json:item>
</editor>
</serie>
<host><title>Computer Science Logic</title>
<language><json:string>unknown</json:string>
</language>
<copyrightDate>2002</copyrightDate>
<doi><json:string>10.1007/3-540-45793-3</json:string>
</doi>
<issn><json:string>0302-9743</json:string>
</issn>
<eisbn><json:string>978-3-540-45793-0</json:string>
</eisbn>
<bookId><json:string>3-540-45793-3</json:string>
</bookId>
<isbn><json:string>978-3-540-44240-0</json:string>
</isbn>
<volume>2471</volume>
<pages><first>183</first>
<last>199</last>
</pages>
<genre><json:string>book-series</json:string>
</genre>
<editor><json:item><name>Julian Bradfield</name>
<affiliations><json:string>Laboratory for Foundations of Computer Science Division of Informatics, University of Edinburgh, King’s Buildings, Mayfield Road, EH9 3JZ, Edinburgh, UK</json:string>
<json:string>E-mail: cs102@dcs.ed.ac.uk</json:string>
</affiliations>
</json:item>
</editor>
<subject><json:item><value>Computer Science</value>
</json:item>
<json:item><value>Computer Science</value>
</json:item>
<json:item><value>Mathematical Logic and Formal Languages</value>
</json:item>
<json:item><value>Artificial Intelligence (incl. Robotics)</value>
</json:item>
<json:item><value>Logics and Meanings of Programs</value>
</json:item>
<json:item><value>Mathematical Logic and Foundations</value>
</json:item>
</subject>
</host>
<ark><json:string>ark:/67375/HCB-DS02CDVK-S</json:string>
</ark>
<publicationDate>2002</publicationDate>
<copyrightDate>2002</copyrightDate>
<doi><json:string>10.1007/3-540-45793-3_13</json:string>
</doi>
<id>F71E0B68369621B1437F3428CF7C75CDD1007685</id>
<score>1</score>
<fulltext><json:item><extension>pdf</extension>
<original>true</original>
<mimetype>application/pdf</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-DS02CDVK-S/fulltext.pdf</uri>
</json:item>
<json:item><extension>zip</extension>
<original>false</original>
<mimetype>application/zip</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-DS02CDVK-S/bundle.zip</uri>
</json:item>
<istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-DS02CDVK-S/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Resource Tableaux</title>
</titleStmt>
<publicationStmt><authority>ISTEX</authority>
<availability><licence>Springer-Verlag Berlin Heidelberg</licence>
</availability>
<date when="2002">2002</date>
</publicationStmt>
<notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note>
<note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note>
</notesStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Resource Tableaux</title>
<author><persName><forename type="first">Didier</forename>
<surname>Galmiche</surname>
</persName>
<email>galmiche@loria.fr</email>
<affiliation><orgName type="institution">LORIA</orgName>
<address><settlement>Nancy</settlement>
<country key="FR">FRANCE</country>
</address>
</affiliation>
</author>
<author><persName><forename type="first">Daniel</forename>
<surname>Méry</surname>
</persName>
<email>dmery@loria.fr</email>
<affiliation><orgName type="institution">LORIA</orgName>
<address><settlement>Nancy</settlement>
<country key="FR">FRANCE</country>
</address>
</affiliation>
</author>
<author><persName><forename type="first">David</forename>
<surname>Pym</surname>
</persName>
<email>d.j.pym@bath.ac.uk</email>
<affiliation><orgName type="institution">University of Bath</orgName>
<address><country key=""></country>
</address>
</affiliation>
</author>
<idno type="istex">F71E0B68369621B1437F3428CF7C75CDD1007685</idno>
<idno type="ark">ark:/67375/HCB-DS02CDVK-S</idno>
<idno type="DOI">10.1007/3-540-45793-3_13</idno>
</analytic>
<monogr><title level="m" type="main">Computer Science Logic</title>
<title level="m" type="sub">16th International Workshop, CSL 2002 11th Annual Conference of the EACSL Edinburgh, Scotland, UK, September 22–25, 2002 Proceedings</title>
<title level="m" type="part">Linear and Resource Logics</title>
<idno type="DOI">10.1007/3-540-45793-3</idno>
<idno type="book-id">3-540-45793-3</idno>
<idno type="ISBN">978-3-540-44240-0</idno>
<idno type="eISBN">978-3-540-45793-0</idno>
<idno type="chapter-id">Chap13</idno>
<idno type="part-id">Part4</idno>
<editor><persName><forename type="first">Julian</forename>
<surname>Bradfield</surname>
</persName>
<email>cs102@dcs.ed.ac.uk</email>
<affiliation><orgName type="department">Laboratory for Foundations of Computer Science Division of Informatics</orgName>
<orgName type="institution">University of Edinburgh</orgName>
<address><street>King’s Buildings, Mayfield Road</street>
<settlement>Edinburgh</settlement>
<postCode>EH9 3JZ</postCode>
<country key="GB">UNITED KINGDOM</country>
</address>
</affiliation>
</editor>
<imprint><biblScope unit="vol">2471</biblScope>
<biblScope unit="page" from="183">183</biblScope>
<biblScope unit="page" to="199">199</biblScope>
<biblScope unit="chapter-count">40</biblScope>
<biblScope unit="part-chapter-count">3</biblScope>
</imprint>
</monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<editor><persName><forename type="first">Gerhard</forename>
<surname>Goos</surname>
</persName>
<affiliation><orgName type="institution">Karlsruhe University</orgName>
<address><country key="DE">GERMANY</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Juris</forename>
<surname>Hartmanis</surname>
</persName>
<affiliation><orgName type="institution">Cornell University</orgName>
<address><region>NY</region>
<country key="US">UNITED STATES</country>
</address>
</affiliation>
</editor>
<editor><persName><forename type="first">Jan</forename>
<nameLink>van</nameLink>
<surname>Leeuwen</surname>
</persName>
<affiliation><orgName type="institution">Utrecht University</orgName>
<address><country key=""></country>
</address>
</affiliation>
</editor>
<idno type="pISSN">0302-9743</idno>
<idno type="seriesID">558</idno>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><abstract xml:lang="en"><head>Abstract</head>
<p>The logic of bunched implications, <hi rend="bold">BI</hi>
, provides a logical analysis of a basic notion of resource rich enough to provide a “pointer logic” semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for <hi rend="bold">BI</hi>
, so providing an elegant basis for efficient theorem proving tools for <hi rend="bold">BI</hi>
. It is based on the use of an algebra of labels for <hi rend="bold">BI</hi>
’s tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For <hi rend="bold">BI</hi>
 with inconsistency, ⊥, the challenge consists in dealing with <hi rend="bold">BI</hi>
’s Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method <hi rend="bold">TBI</hi>
 with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. As consequences, we have two strong new results for <hi rend="bold">BI</hi>
: the decidability of propositional <hi rend="bold">BI</hi>
 and the finite model property with respect to Grothendieck topological semantics. In addition, we propose, by considering partially defined monoids, a new semantics which generalizes the semantics of <hi rend="bold">BI</hi>
’s pointer logic and for which <hi rend="bold">BI</hi>
 is complete</p>
</abstract>
<textClass ana="keyword"><keywords xml:lang="en"><term>BI</term>
<term>resources</term>
<term>semantics</term>
<term>tableaux</term>
<term>decidability</term>
<term>finite model property</term>
</keywords>
</textClass>
<textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label>
<item><term>Computer Science</term>
</item>
</list>
</keywords>
</textClass>
<textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label>
<item><term type="Primary">Computer Science</term>
</item>
<label>I16048</label>
<item><term type="Secondary" subtype="priority-1">Mathematical Logic and Formal Languages</term>
</item>
<label>I21017</label>
<item><term type="Secondary" subtype="priority-2">Artificial Intelligence (incl. Robotics)</term>
</item>
<label>I1603X</label>
<item><term type="Secondary" subtype="priority-3">Logics and Meanings of Programs</term>
</item>
<label>M24005</label>
<item><term type="Secondary" subtype="priority-4">Mathematical Logic and Foundations</term>
</item>
</list>
</keywords>
</textClass>
<langUsage><language ident="EN"></language>
</langUsage>
</profileDesc>
</teiHeader>
</istex:fulltextTEI>
<json:item><extension>txt</extension>
<original>false</original>
<mimetype>text/plain</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-DS02CDVK-S/fulltext.txt</uri>
</json:item>
</fulltext>
<metadata><istex:metadataXml wicri:clean="corpus springer-ebooks not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration>
<istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType>
<istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName>
<PublisherLocation>Berlin, Heidelberg</PublisherLocation>
</PublisherInfo>
<Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID>
<SeriesPrintISSN>0302-9743</SeriesPrintISSN>
<SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle>
</SeriesInfo>
<SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName>
<FamilyName>Goos</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName>
<FamilyName>Hartmanis</FamilyName>
</EditorName>
</Editor>
<Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName>
<Particle>van</Particle>
<FamilyName>Leeuwen</FamilyName>
</EditorName>
</Editor>
<Affiliation ID="Aff1"><OrgName>Karlsruhe University</OrgName>
<OrgAddress><Country>Germany</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff2"><OrgName>Cornell University</OrgName>
<OrgAddress><State>NY</State>
<Country>USA</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff3"><OrgName>Utrecht University</OrgName>
<OrgAddress><Country>The Netherlands</Country>
</OrgAddress>
</Affiliation>
</EditorGroup>
</SeriesHeader>
<Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-45793-3</BookID>
<BookTitle>Computer Science Logic</BookTitle>
<BookSubTitle>16th International Workshop, CSL 2002 11th Annual Conference of the EACSL Edinburgh, Scotland, UK, September 22–25, 2002 Proceedings</BookSubTitle>
<BookVolumeNumber>2471</BookVolumeNumber>
<BookSequenceNumber>2471</BookSequenceNumber>
<BookDOI>10.1007/3-540-45793-3</BookDOI>
<BookTitleID>72496</BookTitleID>
<BookPrintISBN>978-3-540-44240-0</BookPrintISBN>
<BookElectronicISBN>978-3-540-45793-0</BookElectronicISBN>
<BookChapterCount>40</BookChapterCount>
<BookHistory><OnlineDate><Year>2002</Year>
<Month>9</Month>
<Day>2</Day>
</OnlineDate>
</BookHistory>
<BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName>
<CopyrightYear>2002</CopyrightYear>
</BookCopyright>
<BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject>
<BookSubject Code="I16048" Priority="1" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject>
<BookSubject Code="I21017" Priority="2" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject>
<BookSubject Code="I1603X" Priority="3" Type="Secondary">Logics and Meanings of Programs</BookSubject>
<BookSubject Code="M24005" Priority="4" Type="Secondary">Mathematical Logic and Foundations</BookSubject>
<SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection>
</BookSubjectGroup>
<BookContext><SeriesID>558</SeriesID>
</BookContext>
</BookInfo>
<BookHeader><EditorGroup><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Julian</GivenName>
<FamilyName>Bradfield</FamilyName>
</EditorName>
<Contact><Email>cs102@dcs.ed.ac.uk</Email>
</Contact>
</Editor>
<Affiliation ID="Aff4"><OrgDivision>Laboratory for Foundations of Computer Science Division of Informatics</OrgDivision>
<OrgName>University of Edinburgh</OrgName>
<OrgAddress><Street>King’s Buildings, Mayfield Road</Street>
<City>Edinburgh</City>
<Postcode>EH9 3JZ</Postcode>
<Country>UK</Country>
</OrgAddress>
</Affiliation>
</EditorGroup>
</BookHeader>
<Part ID="Part4"><PartInfo TocLevels="0"><PartID>4</PartID>
<PartSequenceNumber>4</PartSequenceNumber>
<PartTitle>Linear and Resource Logics</PartTitle>
<PartChapterCount>3</PartChapterCount>
<PartContext><SeriesID>558</SeriesID>
<BookID>3-540-45793-3</BookID>
<BookTitle>Computer Science Logic</BookTitle>
</PartContext>
</PartInfo>
<Chapter ID="Chap13" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>13</ChapterID>
<ChapterDOI>10.1007/3-540-45793-3_13</ChapterDOI>
<ChapterSequenceNumber>13</ChapterSequenceNumber>
<ChapterTitle Language="En">Resource Tableaux</ChapterTitle>
<ChapterSubTitle Language="En">Extended Abstract</ChapterSubTitle>
<ChapterFirstPage>183</ChapterFirstPage>
<ChapterLastPage>199</ChapterLastPage>
<ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName>
<CopyrightYear>2002</CopyrightYear>
</ChapterCopyright>
<ChapterHistory><RegistrationDate><Year>2002</Year>
<Month>9</Month>
<Day>1</Day>
</RegistrationDate>
<OnlineDate><Year>2002</Year>
<Month>9</Month>
<Day>2</Day>
</OnlineDate>
</ChapterHistory>
<ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant>
<AbstractGrant Grant="OpenAccess"></AbstractGrant>
<BodyPDFGrant Grant="Restricted"></BodyPDFGrant>
<BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant>
<BibliographyGrant Grant="Restricted"></BibliographyGrant>
<ESMGrant Grant="Restricted"></ESMGrant>
</ChapterGrants>
<ChapterContext><SeriesID>558</SeriesID>
<PartID>4</PartID>
<BookID>3-540-45793-3</BookID>
<BookTitle>Computer Science Logic</BookTitle>
</ChapterContext>
</ChapterInfo>
<ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff5"><AuthorName DisplayOrder="Western"><GivenName>Didier</GivenName>
<FamilyName>Galmiche</FamilyName>
</AuthorName>
<Contact><Email>galmiche@loria.fr</Email>
</Contact>
</Author>
<Author AffiliationIDS="Aff5"><AuthorName DisplayOrder="Western"><GivenName>Daniel</GivenName>
<FamilyName>Méry</FamilyName>
</AuthorName>
<Contact><Email>dmery@loria.fr</Email>
</Contact>
</Author>
<Author AffiliationIDS="Aff6"><AuthorName DisplayOrder="Western"><GivenName>David</GivenName>
<FamilyName>Pym</FamilyName>
</AuthorName>
<Contact><Email>d.j.pym@bath.ac.uk</Email>
</Contact>
</Author>
<Affiliation ID="Aff5"><OrgName>LORIA</OrgName>
<OrgAddress><City>Nancy</City>
<Country>France</Country>
</OrgAddress>
</Affiliation>
<Affiliation ID="Aff6"><OrgName>University of Bath</OrgName>
<OrgAddress><Country>England</Country>
</OrgAddress>
</Affiliation>
</AuthorGroup>
<Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading>
<Para>The logic of bunched implications, <Emphasis Type="Bold">BI</Emphasis>
, provides a logical analysis of a basic notion of resource rich enough to provide a “pointer logic” semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for <Emphasis Type="Bold">BI</Emphasis>
, so providing an elegant basis for efficient theorem proving tools for <Emphasis Type="Bold">BI</Emphasis>
. It is based on the use of an algebra of labels for <Emphasis Type="Bold">BI</Emphasis>
’s tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For <Emphasis Type="Bold">BI</Emphasis>
 with inconsistency, ⊥, the challenge consists in dealing with <Emphasis Type="Bold">BI</Emphasis>
’s Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method <Emphasis Type="Bold">TBI</Emphasis>
 with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. As consequences, we have two strong new results for <Emphasis Type="Bold">BI</Emphasis>
: the decidability of propositional <Emphasis Type="Bold">BI</Emphasis>
 and the finite model property with respect to Grothendieck topological semantics. In addition, we propose, by considering partially defined monoids, a new semantics which generalizes the semantics of <Emphasis Type="Bold">BI</Emphasis>
’s pointer logic and for which <Emphasis Type="Bold">BI</Emphasis>
 is complete</Para>
</Abstract>
<KeywordGroup Language="En"><Heading>Keywords</Heading>
<Keyword>BI</Keyword>
<Keyword>resources</Keyword>
<Keyword>semantics</Keyword>
<Keyword>tableaux</Keyword>
<Keyword>decidability</Keyword>
<Keyword>finite model property</Keyword>
</KeywordGroup>
</ChapterHeader>
<NoBody></NoBody>
</Chapter>
</Part>
</Book>
</Series>
</Publisher>
</istex:document>
</istex:metadataXml>
<mods version="3.6"><titleInfo lang="en"><title>Resource Tableaux</title>
<subTitle>Extended Abstract</subTitle>
</titleInfo>
<titleInfo type="alternative" contentType="CDATA"><title>Resource Tableaux</title>
</titleInfo>
<name type="personal"><namePart type="given">Didier</namePart>
<namePart type="family">Galmiche</namePart>
<affiliation>LORIA, Nancy, France</affiliation>
<affiliation>E-mail: galmiche@loria.fr</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Daniel</namePart>
<namePart type="family">Méry</namePart>
<affiliation>LORIA, Nancy, France</affiliation>
<affiliation>E-mail: dmery@loria.fr</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">David</namePart>
<namePart type="family">Pym</namePart>
<affiliation>University of Bath, England</affiliation>
<affiliation>E-mail: d.j.pym@bath.ac.uk</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<typeOfResource>text</typeOfResource>
<genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre>
<originInfo><publisher>Springer Berlin Heidelberg</publisher>
<place><placeTerm type="text">Berlin, Heidelberg</placeTerm>
</place>
<dateIssued encoding="w3cdtf">2002</dateIssued>
<copyrightDate encoding="w3cdtf">2002</copyrightDate>
</originInfo>
<language><languageTerm type="code" authority="rfc3066">en</languageTerm>
<languageTerm type="code" authority="iso639-2b">eng</languageTerm>
</language>
<abstract lang="en">Abstract: The logic of bunched implications, BI, provides a logical analysis of a basic notion of resource rich enough to provide a “pointer logic” semantics for programs which manipulate mutable data structures. We develop a theory of semantic tableaux for BI, so providing an elegant basis for efficient theorem proving tools for BI. It is based on the use of an algebra of labels for BI’s tableaux to solve the resource-distribution problem, the labels being the elements of resource models. For BI with inconsistency, ⊥, the challenge consists in dealing with BI’s Grothendieck topological models within such a proof-search method, based on labels. We prove soundness and completeness theorems for a resource tableaux method TBI with respect to this semantics and provide a way to build countermodels from so-called dependency graphs. As consequences, we have two strong new results for BI: the decidability of propositional BI and the finite model property with respect to Grothendieck topological semantics. In addition, we propose, by considering partially defined monoids, a new semantics which generalizes the semantics of BI’s pointer logic and for which BI is complete</abstract>
<subject lang="en"><genre>Keywords</genre>
<topic>BI</topic>
<topic>resources</topic>
<topic>semantics</topic>
<topic>tableaux</topic>
<topic>decidability</topic>
<topic>finite model property</topic>
</subject>
<relatedItem type="host"><titleInfo><title>Computer Science Logic</title>
<subTitle>16th International Workshop, CSL 2002 11th Annual Conference of the EACSL Edinburgh, Scotland, UK, September 22–25, 2002 Proceedings</subTitle>
</titleInfo>
<name type="personal"><namePart type="given">Julian</namePart>
<namePart type="family">Bradfield</namePart>
<affiliation>Laboratory for Foundations of Computer Science Division of Informatics, University of Edinburgh, King’s Buildings, Mayfield Road, EH9 3JZ, Edinburgh, UK</affiliation>
<affiliation>E-mail: cs102@dcs.ed.ac.uk</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre>
<originInfo><publisher>Springer</publisher>
<copyrightDate encoding="w3cdtf">2002</copyrightDate>
<issuance>monographic</issuance>
</originInfo>
<subject><genre>Book-Subject-Collection</genre>
<topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic>
</subject>
<subject><genre>Book-Subject-Group</genre>
<topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic>
<topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic>
<topic authority="SpringerSubjectCodes" authorityURI="M24005">Mathematical Logic and Foundations</topic>
</subject>
<identifier type="DOI">10.1007/3-540-45793-3</identifier>
<identifier type="ISBN">978-3-540-44240-0</identifier>
<identifier type="eISBN">978-3-540-45793-0</identifier>
<identifier type="ISSN">0302-9743</identifier>
<identifier type="BookTitleID">72496</identifier>
<identifier type="BookID">3-540-45793-3</identifier>
<identifier type="BookChapterCount">40</identifier>
<identifier type="BookVolumeNumber">2471</identifier>
<identifier type="BookSequenceNumber">2471</identifier>
<identifier type="PartChapterCount">3</identifier>
<part><date>2002</date>
<detail type="part"><title>Linear and Resource Logics</title>
</detail>
<detail type="volume"><number>2471</number>
<caption>vol.</caption>
</detail>
<extent unit="pages"><start>183</start>
<end>199</end>
</extent>
</part>
<recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin>
</recordInfo>
</relatedItem>
<relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title>
</titleInfo>
<name type="personal"><namePart type="given">Gerhard</namePart>
<namePart type="family">Goos</namePart>
<affiliation>Karlsruhe University, Germany</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Juris</namePart>
<namePart type="family">Hartmanis</namePart>
<affiliation>Cornell University, NY, USA</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<name type="personal"><namePart type="given">Jan</namePart>
<namePart type="family">van Leeuwen</namePart>
<affiliation>Utrecht University, The Netherlands</affiliation>
<role><roleTerm type="text">editor</roleTerm>
</role>
</name>
<originInfo><publisher>Springer</publisher>
<copyrightDate encoding="w3cdtf">2002</copyrightDate>
<issuance>serial</issuance>
</originInfo>
<identifier type="ISSN">0302-9743</identifier>
<identifier type="SeriesID">558</identifier>
<recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin>
</recordInfo>
</relatedItem>
<identifier type="istex">F71E0B68369621B1437F3428CF7C75CDD1007685</identifier>
<identifier type="ark">ark:/67375/HCB-DS02CDVK-S</identifier>
<identifier type="DOI">10.1007/3-540-45793-3_13</identifier>
<identifier type="ChapterID">13</identifier>
<identifier type="ChapterID">Chap13</identifier>
<accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2002</accessCondition>
<recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource>
<recordOrigin>Springer-Verlag Berlin Heidelberg, 2002</recordOrigin>
</recordInfo>
</mods>
<json:item><extension>json</extension>
<original>false</original>
<mimetype>application/json</mimetype>
<uri>https://api.istex.fr/ark:/67375/HCB-DS02CDVK-S/record.json</uri>
</json:item>
</metadata>
</istex>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus

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

HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003B22 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Istex
   |étape=   Corpus
   |type=    RBID
   |clé=     ISTEX:F71E0B68369621B1437F3428CF7C75CDD1007685
   |texte=   Resource Tableaux
}}

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

Resource Tableaux

Resource Tableaux

Source :

Abstract

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