Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic
Identifieur interne : 002F81 ( Istex/Corpus ); précédent : 002F80; suivant : 002F82Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic
Auteurs : Silvio Ranise ; Christophe Ringeissen ; Calogero G. ZarbaSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.
Url:
DOI: 10.1007/11559306_3
Links to Exploration step
ISTEX:C999F91510BA36B2C64229AECD6D8034288F3847Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic</title><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation><mods:affiliation>LORIA and INRIA-Lorraine, </mods:affiliation></affiliation></author><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation><mods:affiliation>LORIA and INRIA-Lorraine, </mods:affiliation></affiliation></author><author><name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name><affiliation><mods:affiliation>University of New Mexico, </mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:C999F91510BA36B2C64229AECD6D8034288F3847</idno><date when="2005" year="2005">2005</date><idno type="doi">10.1007/11559306_3</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-7N6V0C23-2/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002F81</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002F81</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic</title><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation><mods:affiliation>LORIA and INRIA-Lorraine, </mods:affiliation></affiliation></author><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation><mods:affiliation>LORIA and INRIA-Lorraine, </mods:affiliation></affiliation></author><author><name sortKey="Zarba, Calogero G" sort="Zarba, Calogero G" uniqKey="Zarba C" first="Calogero G." last="Zarba">Calogero G. Zarba</name><affiliation><mods:affiliation>University of New Mexico, </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="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: Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Silvio Ranise</name><affiliations><json:string>LORIA and INRIA-Lorraine,</json:string></affiliations></json:item><json:item><name>Christophe Ringeissen</name><affiliations><json:string>LORIA and INRIA-Lorraine,</json:string></affiliations></json:item><json:item><name>Calogero G. Zarba</name><affiliations><json:string>University of New Mexico,</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-7N6V0C23-2</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.</abstract><qualityIndicators><score>9.016</score><pdfWordCount>6943</pdfWordCount><pdfCharCount>32398</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>17</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>168</abstractWordCount><abstractCharCount>1039</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic</title><chapterId><json:string>3</json:string><json:string>Chap3</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>2005</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>David Hutchison</name><affiliations><json:string>Lancaster University, UK</json:string></affiliations></json:item><json:item><name>Takeo Kanade</name><affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string></affiliations></json:item><json:item><name>Josef Kittler</name><affiliations><json:string>University of Surrey, Guildford, UK</json:string></affiliations></json:item><json:item><name>Jon M. Kleinberg</name><affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string></affiliations></json:item><json:item><name>Friedemann Mattern</name><affiliations><json:string>ETH Zurich, Switzerland</json:string></affiliations></json:item><json:item><name>John C. Mitchell</name><affiliations><json:string>Stanford University, CA, USA</json:string></affiliations></json:item><json:item><name>Moni Naor</name><affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string></affiliations></json:item><json:item><name>Oscar Nierstrasz</name><affiliations><json:string>University of Bern, Switzerland</json:string></affiliations></json:item><json:item><name>C. Pandu Rangan</name><affiliations><json:string>Indian Institute of Technology, Madras, India</json:string></affiliations></json:item><json:item><name>Bernhard Steffen</name><affiliations><json:string>University of Dortmund, Germany</json:string></affiliations></json:item><json:item><name>Madhu Sudan</name><affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string></affiliations></json:item><json:item><name>Demetri Terzopoulos</name><affiliations><json:string>New York University, NY, USA</json:string></affiliations></json:item><json:item><name>Dough Tygar</name><affiliations><json:string>University of California, Berkeley, CA, USA</json:string></affiliations></json:item><json:item><name>Moshe Y. Vardi</name><affiliations><json:string>Rice University, Houston, TX, USA</json:string></affiliations></json:item><json:item><name>Gerhard Weikum</name><affiliations><json:string>Max-Planck Institute of Computer Science, Saarbruecken, Germany</json:string></affiliations></json:item></editor></serie><host><title>Frontiers of Combining Systems</title><language><json:string>unknown</json:string></language><copyrightDate>2005</copyrightDate><doi><json:string>10.1007/11559306</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-540-31730-2</json:string></eisbn><bookId><json:string>978-3-540-31730-2</json:string></bookId><isbn><json:string>978-3-540-29051-3</json:string></isbn><volume>3717</volume><pages><first>48</first><last>64</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Bernhard Gramlich</name><affiliations><json:string>Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9 – E185/2, A-1040, Wien, Austria</json:string><json:string>E-mail: gramlich@logic.at</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>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item><json:item><value>Programming Techniques</value></json:item><json:item><value>Software Engineering</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-7N6V0C23-2</json:string></ark><publicationDate>2005</publicationDate><copyrightDate>2005</copyrightDate><doi><json:string>10.1007/11559306_3</json:string></doi><id>C999F91510BA36B2C64229AECD6D8034288F3847</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-7N6V0C23-2/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-7N6V0C23-2/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-7N6V0C23-2/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2005">2005</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">Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic</title><author><persName><forename type="first">Silvio</forename><surname>Ranise</surname></persName><affiliation><orgName type="institution">LORIA and INRIA-Lorraine</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Christophe</forename><surname>Ringeissen</surname></persName><affiliation><orgName type="institution">LORIA and INRIA-Lorraine</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Calogero</forename><forename type="first">G.</forename><surname>Zarba</surname></persName><affiliation><orgName type="institution">University of New Mexico</orgName><address><country key=""></country></address></affiliation></author><idno type="istex">C999F91510BA36B2C64229AECD6D8034288F3847</idno><idno type="ark">ark:/67375/HCB-7N6V0C23-2</idno><idno type="DOI">10.1007/11559306_3</idno></analytic><monogr><title level="m" type="main">Frontiers of Combining Systems</title><title level="m" type="sub">5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005. Proceedings</title><title level="m" type="part">Logics, Theories, and Decision Procedures I</title><idno type="DOI">10.1007/11559306</idno><idno type="book-id">978-3-540-31730-2</idno><idno type="ISBN">978-3-540-29051-3</idno><idno type="eISBN">978-3-540-31730-2</idno><idno type="chapter-id">Chap3</idno><idno type="part-id">Part1</idno><editor><persName><forename type="first">Bernhard</forename><surname>Gramlich</surname></persName><email>gramlich@logic.at</email><affiliation><orgName type="department">Fakultät für Informatik</orgName><orgName type="institution">Technische Universität Wien</orgName><address><street>Favoritenstr. 9 – E185/2</street><postCode>A-1040</postCode><settlement>Wien</settlement><country key="AT">AUSTRIA</country></address></affiliation></editor><imprint><biblScope unit="vol">3717</biblScope><biblScope unit="page" from="48">48</biblScope><biblScope unit="page" to="64">64</biblScope><biblScope unit="chapter-count">19</biblScope><biblScope unit="part-chapter-count">4</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">David</forename><surname>Hutchison</surname></persName><affiliation><orgName type="institution">Lancaster University</orgName><address><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName><affiliation><orgName type="institution">Carnegie Mellon University</orgName><address><settlement>Pittsburgh</settlement><region>PA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName><affiliation><orgName type="institution">University of Surrey</orgName><address><settlement>Guildford</settlement><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName><affiliation><orgName type="institution">Cornell University</orgName><address><settlement>Ithaca</settlement><region>NY</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName><affiliation><orgName type="institution">ETH Zurich</orgName><address><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName><affiliation><orgName type="institution">Stanford University</orgName><address><settlement>CA</settlement><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moni</forename><surname>Naor</surname></persName><affiliation><orgName type="institution">Weizmann Institute of Science</orgName><address><settlement>Rehovot</settlement><country key="IL">ISRAEL</country></address></affiliation></editor><editor><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName><affiliation><orgName type="institution">University of Bern</orgName><address><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName><affiliation><orgName type="institution">Indian Institute of Technology</orgName><address><settlement>Madras</settlement><country key="IN">INDIA</country></address></affiliation></editor><editor><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName><affiliation><orgName type="institution">University of Dortmund</orgName><address><country key="DE">GERMANY</country></address></affiliation></editor><editor><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName><affiliation><orgName type="institution">Massachusetts Institute of Technology</orgName><address><settlement>MA</settlement><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName><affiliation><orgName type="institution">New York University</orgName><address><settlement>NY</settlement><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Dough</forename><surname>Tygar</surname></persName><affiliation><orgName type="institution">University of California</orgName><address><settlement>Berkeley</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName><affiliation><orgName type="institution">Rice University</orgName><address><settlement>Houston</settlement><region>TX</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName><affiliation><orgName type="institution">Max-Planck Institute of Computer Science</orgName><address><settlement>Saarbruecken</settlement><country key="DE">GERMANY</country></address></affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory <hi rend="italic">S</hi> modeling the data structure with a theory <hi rend="italic">T</hi> modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both <hi rend="italic">S</hi> and <hi rend="italic">T</hi> are stably infinite.</p><p>The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of <hi rend="italic">polite</hi> theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory <hi rend="italic">S</hi> with any theory <hi rend="italic">T</hi> of the elements, regardless of whether <hi rend="italic">T</hi> is stably infinite or not.</p><p>The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of <hi rend="italic">shiny</hi> theories with nonstably infinite theories in one-sorted logic.</p></abstract><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>I21017</label><item><term type="Secondary" subtype="priority-1">Artificial Intelligence (incl. Robotics)</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-2">Mathematical Logic and Formal Languages</term></item><label>I14010</label><item><term type="Secondary" subtype="priority-3">Programming Techniques</term></item><label>I14029</label><item><term type="Secondary" subtype="priority-4">Software Engineering</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-7N6V0C23-2/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><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName><FamilyName>Hutchison</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName><FamilyName>Kanade</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName><FamilyName>Kittler</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName><GivenName>M.</GivenName><FamilyName>Kleinberg</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName><FamilyName>Mattern</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName><GivenName>C.</GivenName><FamilyName>Mitchell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName><FamilyName>Naor</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName><FamilyName>Nierstrasz</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Pandu Rangan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Steffen</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName><FamilyName>Sudan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName><FamilyName>Terzopoulos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Dough</GivenName><FamilyName>Tygar</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName><GivenName>Y.</GivenName><FamilyName>Vardi</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Weikum</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Lancaster University</OrgName><OrgAddress><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>University of Surrey</OrgName><OrgAddress><City>Guildford</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>Cornell University</OrgName><OrgAddress><City>Ithaca</City><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>ETH Zurich</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgName>Stanford University</OrgName><OrgAddress><City>CA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>Weizmann Institute of Science</OrgName><OrgAddress><City>Rehovot</City><Country>Israel</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgName>University of Bern</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgName>Indian Institute of Technology</OrgName><OrgAddress><City>Madras</City><Country>India</Country></OrgAddress></Affiliation><Affiliation ID="Aff10"><OrgName>University of Dortmund</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff11"><OrgName>Massachusetts Institute of Technology</OrgName><OrgAddress><City>MA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff12"><OrgName>New York University</OrgName><OrgAddress><City>NY</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff13"><OrgName>University of California</OrgName><OrgAddress><City>Berkeley</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff14"><OrgName>Rice University</OrgName><OrgAddress><City>Houston</City><State>TX</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff15"><OrgName>Max-Planck Institute of Computer Science</OrgName><OrgAddress><City>Saarbruecken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesPrintISSN>0302-9743</SubSeriesPrintISSN><SubSeriesElectronicISSN>1611-3349</SubSeriesElectronicISSN><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff17"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Affiliation ID="Aff16"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff17"><OrgName>University of Saarland</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SubSeriesHeader></SubSeries><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-540-31730-2</BookID><BookTitle>Frontiers of Combining Systems</BookTitle><BookSubTitle>5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005. Proceedings</BookSubTitle><BookVolumeNumber>3717</BookVolumeNumber><BookSequenceNumber>3717</BookSequenceNumber><BookDOI>10.1007/11559306</BookDOI><BookTitleID>126717</BookTitleID><BookPrintISBN>978-3-540-29051-3</BookPrintISBN><BookElectronicISBN>978-3-540-31730-2</BookElectronicISBN><BookChapterCount>19</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2005</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I21017" Priority="1" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><BookSubject Code="I16048" Priority="2" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I14010" Priority="3" Type="Secondary">Programming Techniques</BookSubject><BookSubject Code="I14029" Priority="4" Type="Secondary">Software Engineering</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID><SubSeriesID>1244</SubSeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff18"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Gramlich</FamilyName></EditorName><Contact><Email>gramlich@logic.at</Email></Contact></Editor><Affiliation ID="Aff18"><OrgDivision>Fakultät für Informatik</OrgDivision><OrgName>Technische Universität Wien</OrgName><OrgAddress><Street>Favoritenstr. 9 – E185/2</Street><Postcode>A-1040</Postcode><City>Wien</City><Country>Austria</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part1"><PartInfo TocLevels="0"><PartID>1</PartID><PartSequenceNumber>1</PartSequenceNumber><PartTitle>Logics, Theories, and Decision Procedures I</PartTitle><PartChapterCount>4</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Frontiers of Combining Systems</BookTitle></PartContext></PartInfo><Chapter ID="Chap3" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>3</ChapterID><ChapterDOI>10.1007/11559306_3</ChapterDOI><ChapterSequenceNumber>3</ChapterSequenceNumber><ChapterTitle Language="En">Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic</ChapterTitle><ChapterFirstPage>48</ChapterFirstPage><ChapterLastPage>64</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2005</CopyrightYear></ChapterCopyright><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>1</PartID><BookID>978-3-540-31730-2</BookID><BookTitle>Frontiers of Combining Systems</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff19"><AuthorName DisplayOrder="Western"><GivenName>Silvio</GivenName><FamilyName>Ranise</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff19"><AuthorName DisplayOrder="Western"><GivenName>Christophe</GivenName><FamilyName>Ringeissen</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff20"><AuthorName DisplayOrder="Western"><GivenName>Calogero</GivenName><GivenName>G.</GivenName><FamilyName>Zarba</FamilyName></AuthorName></Author><Affiliation ID="Aff19"><OrgName>LORIA and INRIA-Lorraine</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation><Affiliation ID="Aff20"><OrgName>University of New Mexico</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory <Emphasis Type="Italic">S</Emphasis> modeling the data structure with a theory <Emphasis Type="Italic">T</Emphasis> modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both <Emphasis Type="Italic">S</Emphasis> and <Emphasis Type="Italic">T</Emphasis> are stably infinite.</Para><Para>The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of <Emphasis Type="Italic">polite</Emphasis> theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory <Emphasis Type="Italic">S</Emphasis> with any theory <Emphasis Type="Italic">T</Emphasis> of the elements, regardless of whether <Emphasis Type="Italic">T</Emphasis> is stably infinite or not.</Para><Para>The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of <Emphasis Type="Italic">shiny</Emphasis> theories with nonstably infinite theories in one-sorted logic.</Para></Abstract><ArticleNote Type="Misc"><SimplePara>This work is partly supported by grants NSF ITR CCR-0113611, NSF CCR-0098114, and projects ACI GECCOO, and QSL VALDA-2.</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic</title></titleInfo><name type="personal"><namePart type="given">Silvio</namePart><namePart type="family">Ranise</namePart><affiliation>LORIA and INRIA-Lorraine, </affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Christophe</namePart><namePart type="family">Ringeissen</namePart><affiliation>LORIA and INRIA-Lorraine, </affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Calogero</namePart><namePart type="given">G.</namePart><namePart type="family">Zarba</namePart><affiliation>University of New Mexico, </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">2005</dateIssued><copyrightDate encoding="w3cdtf">2005</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: Most computer programs store elements of a given nature into container-based data structures such as lists, arrays, sets, and multisets. To verify the correctness of these programs, one needs to combine a theory S modeling the data structure with a theory T modeling the elements. This combination can be achieved using the classic Nelson-Oppen method only if both S and T are stably infinite. The goal of this paper is to relax the stable infiniteness requirement. To achieve this goal, we introduce the notion of polite theories, and we show that natural examples of polite theories include those modeling data structures such as lists, arrays, sets, and multisets. Furthemore, we provide a method that is able to combine a polite theory S with any theory T of the elements, regardless of whether T is stably infinite or not. The results of this paper generalize to many-sorted logic those recently obtained by Tinelli and Zarba concerning the combination of shiny theories with nonstably infinite theories in one-sorted logic.</abstract><relatedItem type="host"><titleInfo><title>Frontiers of Combining Systems</title><subTitle>5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Gramlich</namePart><affiliation>Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9 – E185/2, A-1040, Wien, Austria</affiliation><affiliation>E-mail: gramlich@logic.at</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">2005</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="I21017">Artificial Intelligence (incl. Robotics)</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I14010">Programming Techniques</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic></subject><identifier type="DOI">10.1007/11559306</identifier><identifier type="ISBN">978-3-540-29051-3</identifier><identifier type="eISBN">978-3-540-31730-2</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">126717</identifier><identifier type="BookID">978-3-540-31730-2</identifier><identifier type="BookChapterCount">19</identifier><identifier type="BookVolumeNumber">3717</identifier><identifier type="BookSequenceNumber">3717</identifier><identifier type="PartChapterCount">4</identifier><part><date>2005</date><detail type="part"><title>Logics, Theories, and Decision Procedures I</title></detail><detail type="volume"><number>3717</number><caption>vol.</caption></detail><extent unit="pages"><start>48</start><end>64</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2005</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>New York University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Dough</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2005</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>New York University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Dough</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jaime</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jörg</namePart><namePart type="family">Siekmann</namePart><affiliation>University of Saarland, Saarbrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Gramlich</namePart><affiliation>Fakultät für Informatik, Technische Universität Wien, Favoritenstr. 9 – E185/2, A-1040, Wien, Austria</affiliation><affiliation>E-mail: gramlich@logic.at</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2005</recordOrigin></recordInfo></relatedItem><identifier type="istex">C999F91510BA36B2C64229AECD6D8034288F3847</identifier><identifier type="ark">ark:/67375/HCB-7N6V0C23-2</identifier><identifier type="DOI">10.1007/11559306_3</identifier><identifier type="ChapterID">3</identifier><identifier type="ChapterID">Chap3</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2005</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, 2005</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-7N6V0C23-2/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 002F81 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002F81 | 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:C999F91510BA36B2C64229AECD6D8034288F3847
|texte= Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic
}}
| This area was generated with Dilib version V0.6.33. |  |