Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
Identifieur interne : 002D69 ( Istex/Corpus ); précédent : 002D68; suivant : 002D70Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
Auteurs : Silvio Ghilardi ; Enrica Nicolini ; Silvio Ranise ; Daniele ZucchelliSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: The theory of arrays, introduced by McCarthy in his seminal paper “Toward a mathematical science of computation”, is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions.
Url:
DOI: 10.1007/11853886_16
Links to Exploration step
ISTEX:C0B0245ECBE1AE666144FE0A4F656023446D24D8Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</title><author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name><affiliation><mods:affiliation>Dipartimento di Informatica, Università degli Studi di Milano, Italia</mods:affiliation></affiliation></author><author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name><affiliation><mods:affiliation>Dipartimento di Matematica, Università degli Studi di Milano, Italia</mods:affiliation></affiliation></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation><mods:affiliation>Dipartimento di Informatica, Università degli Studi di Milano, Italia</mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA & INRIA-Lorraine, Nancy, France</mods:affiliation></affiliation></author><author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name><affiliation><mods:affiliation>Dipartimento di Informatica, Università degli Studi di Milano, Italia</mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA & INRIA-Lorraine, Nancy, France</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:C0B0245ECBE1AE666144FE0A4F656023446D24D8</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1007/11853886_16</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-H1JKPJRX-G/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002D69</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002D69</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</title><author><name sortKey="Ghilardi, Silvio" sort="Ghilardi, Silvio" uniqKey="Ghilardi S" first="Silvio" last="Ghilardi">Silvio Ghilardi</name><affiliation><mods:affiliation>Dipartimento di Informatica, Università degli Studi di Milano, Italia</mods:affiliation></affiliation></author><author><name sortKey="Nicolini, Enrica" sort="Nicolini, Enrica" uniqKey="Nicolini E" first="Enrica" last="Nicolini">Enrica Nicolini</name><affiliation><mods:affiliation>Dipartimento di Matematica, Università degli Studi di Milano, Italia</mods:affiliation></affiliation></author><author><name sortKey="Ranise, Silvio" sort="Ranise, Silvio" uniqKey="Ranise S" first="Silvio" last="Ranise">Silvio Ranise</name><affiliation><mods:affiliation>Dipartimento di Informatica, Università degli Studi di Milano, Italia</mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA & INRIA-Lorraine, Nancy, France</mods:affiliation></affiliation></author><author><name sortKey="Zucchelli, Daniele" sort="Zucchelli, Daniele" uniqKey="Zucchelli D" first="Daniele" last="Zucchelli">Daniele Zucchelli</name><affiliation><mods:affiliation>Dipartimento di Informatica, Università degli Studi di Milano, Italia</mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA & INRIA-Lorraine, Nancy, France</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: The theory of arrays, introduced by McCarthy in his seminal paper “Toward a mathematical science of computation”, is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Silvio Ghilardi</name><affiliations><json:string>Dipartimento di Informatica, Università degli Studi di Milano, Italia</json:string></affiliations></json:item><json:item><name>Enrica Nicolini</name><affiliations><json:string>Dipartimento di Matematica, Università degli Studi di Milano, Italia</json:string></affiliations></json:item><json:item><name>Silvio Ranise</name><affiliations><json:string>Dipartimento di Informatica, Università degli Studi di Milano, Italia</json:string><json:string>LORIA & INRIA-Lorraine, Nancy, France</json:string></affiliations></json:item><json:item><name>Daniele Zucchelli</name><affiliations><json:string>Dipartimento di Informatica, Università degli Studi di Milano, Italia</json:string><json:string>LORIA & INRIA-Lorraine, Nancy, France</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-H1JKPJRX-G</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: The theory of arrays, introduced by McCarthy in his seminal paper “Toward a mathematical science of computation”, is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions.</abstract><qualityIndicators><score>9.364</score><pdfWordCount>5689</pdfWordCount><pdfCharCount>28829</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>13</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>197</abstractWordCount><abstractCharCount>1361</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</title><chapterId><json:string>16</json:string><json:string>Chap16</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>2006</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><volume>II</volume><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>University of California, Los Angeles, CA, 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>Logics in Artificial Intelligence</title><language><json:string>unknown</json:string></language><copyrightDate>2006</copyrightDate><doi><json:string>10.1007/11853886</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-39627-7</json:string></eisbn><bookId><json:string>978-3-540-39627-7</json:string></bookId><isbn><json:string>978-3-540-39625-3</json:string></isbn><volume>4160</volume><pages><first>177</first><last>189</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Michael Fisher</name><affiliations><json:string>Department of Computer Science, University of Liverpool, Liverpool, U.K.</json:string><json:string>E-mail: MFisher@liverpool.ac.uk</json:string></affiliations></json:item><json:item><name>Wiebe van der Hoek</name><affiliations><json:string>University of Liverpool, United Kingdom</json:string><json:string>E-mail: wiebe@csc.liv.ac.uk</json:string></affiliations></json:item><json:item><name>Boris Konev</name><affiliations><json:string>University of Liverpool, Liverpool, UK</json:string><json:string>E-mail: konev@liverpool.ac.uk</json:string></affiliations></json:item><json:item><name>Alexei Lisitsa</name><affiliations><json:string>Department of Computer Science, The University of Liverpool,</json:string><json:string>E-mail: alexei@csc.liv.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>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Programming Techniques</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-H1JKPJRX-G</json:string></ark><publicationDate>2006</publicationDate><copyrightDate>2006</copyrightDate><doi><json:string>10.1007/11853886_16</json:string></doi><id>C0B0245ECBE1AE666144FE0A4F656023446D24D8</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-H1JKPJRX-G/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-H1JKPJRX-G/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-H1JKPJRX-G/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2006">2006</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">Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</title><author><persName><forename type="first">Silvio</forename><surname>Ghilardi</surname></persName><affiliation><orgName type="department">Dipartimento di Informatica</orgName><orgName type="institution">Università degli Studi di Milano</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Enrica</forename><surname>Nicolini</surname></persName><affiliation><orgName type="department">Dipartimento di Matematica</orgName><orgName type="institution">Università degli Studi di Milano</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Silvio</forename><surname>Ranise</surname></persName><affiliation><orgName type="department">Dipartimento di Informatica</orgName><orgName type="institution">Università degli Studi di Milano</orgName><address><country key=""></country></address></affiliation><affiliation><orgName type="institution">LORIA & INRIA-Lorraine</orgName><address><settlement>Nancy</settlement><country key="FR">FRANCE</country></address></affiliation></author><author><persName><forename type="first">Daniele</forename><surname>Zucchelli</surname></persName><affiliation><orgName type="department">Dipartimento di Informatica</orgName><orgName type="institution">Università degli Studi di Milano</orgName><address><country key=""></country></address></affiliation><affiliation><orgName type="institution">LORIA & INRIA-Lorraine</orgName><address><settlement>Nancy</settlement><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">C0B0245ECBE1AE666144FE0A4F656023446D24D8</idno><idno type="ark">ark:/67375/HCB-H1JKPJRX-G</idno><idno type="DOI">10.1007/11853886_16</idno></analytic><monogr><title level="m" type="main">Logics in Artificial Intelligence</title><title level="m" type="sub">10th European Conference, JELIA 2006 Liverpool, UK, September 13-15, 2006 Proceedings</title><title level="m" type="part">Technical Papers</title><idno type="DOI">10.1007/11853886</idno><idno type="book-id">978-3-540-39627-7</idno><idno type="ISBN">978-3-540-39625-3</idno><idno type="eISBN">978-3-540-39627-7</idno><idno type="chapter-id">Chap16</idno><idno type="part-id">Part2</idno><editor><persName><forename type="first">Michael</forename><surname>Fisher</surname></persName><email>MFisher@liverpool.ac.uk</email><affiliation><orgName type="department">Department of Computer Science</orgName><orgName type="institution">University of Liverpool</orgName><address><settlement>Liverpool</settlement><country key=""></country></address></affiliation></editor><editor><persName><forename type="first">Wiebe</forename><nameLink>van der</nameLink><surname>Hoek</surname></persName><email>wiebe@csc.liv.ac.uk</email><affiliation><orgName type="institution">University of Liverpool</orgName><address><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Boris</forename><surname>Konev</surname></persName><email>konev@liverpool.ac.uk</email><affiliation><orgName type="institution">University of Liverpool</orgName><address><settlement>Liverpool</settlement><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Alexei</forename><surname>Lisitsa</surname></persName><email>alexei@csc.liv.ac.uk</email><affiliation><orgName type="department">Department of Computer Science</orgName><orgName type="institution">The University of Liverpool</orgName><address><country key=""></country></address></affiliation></editor><imprint><biblScope unit="vol">4160</biblScope><biblScope unit="page" from="177">177</biblScope><biblScope unit="page" to="189">189</biblScope><biblScope unit="chapter-count">49</biblScope><biblScope unit="part-chapter-count">34</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">University of California</orgName><address><settlement>Los Angeles</settlement><region>CA</region><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>The theory of arrays, introduced by McCarthy in his seminal paper “Toward a mathematical science of computation”, is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays.</p><p>We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions.</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>I14010</label><item><term type="Secondary" subtype="priority-2">Programming Techniques</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-3">Mathematical Logic and Formal Languages</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-H1JKPJRX-G/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>University of California</OrgName><OrgAddress><City>Los Angeles</City><State>CA</State><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-39627-7</BookID><BookTitle>Logics in Artificial Intelligence</BookTitle><BookSubTitle>10th European Conference, JELIA 2006 Liverpool, UK, September 13-15, 2006 Proceedings</BookSubTitle><BookVolumeNumber>4160</BookVolumeNumber><BookSequenceNumber>4160</BookSequenceNumber><BookDOI>10.1007/11853886</BookDOI><BookTitleID>141360</BookTitleID><BookPrintISBN>978-3-540-39625-3</BookPrintISBN><BookElectronicISBN>978-3-540-39627-7</BookElectronicISBN><BookChapterCount>49</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2006</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="I14010" Priority="2" Type="Secondary">Programming Techniques</BookSubject><BookSubject Code="I16048" Priority="3" Type="Secondary">Mathematical Logic and Formal Languages</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>Michael</GivenName><FamilyName>Fisher</FamilyName></EditorName><Contact><Email>MFisher@liverpool.ac.uk</Email></Contact></Editor><Editor AffiliationIDS="Aff19"><EditorName DisplayOrder="Western"><GivenName>Wiebe</GivenName><Particle>van der</Particle><FamilyName>Hoek</FamilyName></EditorName><Contact><Email>wiebe@csc.liv.ac.uk</Email></Contact></Editor><Editor AffiliationIDS="Aff20"><EditorName DisplayOrder="Western"><GivenName>Boris</GivenName><FamilyName>Konev</FamilyName></EditorName><Contact><Email>konev@liverpool.ac.uk</Email></Contact></Editor><Editor AffiliationIDS="Aff21"><EditorName DisplayOrder="Western"><GivenName>Alexei</GivenName><FamilyName>Lisitsa</FamilyName></EditorName><Contact><Email>alexei@csc.liv.ac.uk</Email></Contact></Editor><Affiliation ID="Aff18"><OrgDivision>Department of Computer Science</OrgDivision><OrgName>University of Liverpool</OrgName><OrgAddress><City>Liverpool</City><Country>U.K.</Country></OrgAddress></Affiliation><Affiliation ID="Aff19"><OrgName>University of Liverpool</OrgName><OrgAddress><Country>United Kingdom</Country></OrgAddress></Affiliation><Affiliation ID="Aff20"><OrgName>University of Liverpool</OrgName><OrgAddress><City>Liverpool</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff21"><OrgDivision>Department of Computer Science</OrgDivision><OrgName>The University of Liverpool</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartNumber>II</PartNumber><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Technical Papers</PartTitle><PartChapterCount>34</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Logics in Artificial Intelligence</BookTitle></PartContext></PartInfo><Chapter ID="Chap16" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>16</ChapterID><ChapterDOI>10.1007/11853886_16</ChapterDOI><ChapterSequenceNumber>16</ChapterSequenceNumber><ChapterTitle Language="En">Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</ChapterTitle><ChapterFirstPage>177</ChapterFirstPage><ChapterLastPage>189</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2006</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>2</PartID><BookID>978-3-540-39627-7</BookID><BookTitle>Logics in Artificial Intelligence</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff22"><AuthorName DisplayOrder="Western"><GivenName>Silvio</GivenName><FamilyName>Ghilardi</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff23"><AuthorName DisplayOrder="Western"><GivenName>Enrica</GivenName><FamilyName>Nicolini</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff22 Aff24"><AuthorName DisplayOrder="Western"><GivenName>Silvio</GivenName><FamilyName>Ranise</FamilyName></AuthorName></Author><Author AffiliationIDS="Aff22 Aff24"><AuthorName DisplayOrder="Western"><GivenName>Daniele</GivenName><FamilyName>Zucchelli</FamilyName></AuthorName></Author><Affiliation ID="Aff22"><OrgDivision>Dipartimento di Informatica</OrgDivision><OrgName>Università degli Studi di Milano</OrgName><OrgAddress><Country>Italia</Country></OrgAddress></Affiliation><Affiliation ID="Aff23"><OrgDivision>Dipartimento di Matematica</OrgDivision><OrgName>Università degli Studi di Milano</OrgName><OrgAddress><Country>Italia</Country></OrgAddress></Affiliation><Affiliation ID="Aff24"><OrgName>LORIA & INRIA-Lorraine</OrgName><OrgAddress><City>Nancy</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>The theory of arrays, introduced by McCarthy in his seminal paper “Toward a mathematical science of computation”, is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays.</Para><Para>We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies</title></titleInfo><name type="personal"><namePart type="given">Silvio</namePart><namePart type="family">Ghilardi</namePart><affiliation>Dipartimento di Informatica, Università degli Studi di Milano, Italia</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Enrica</namePart><namePart type="family">Nicolini</namePart><affiliation>Dipartimento di Matematica, Università degli Studi di Milano, Italia</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Silvio</namePart><namePart type="family">Ranise</namePart><affiliation>Dipartimento di Informatica, Università degli Studi di Milano, Italia</affiliation><affiliation>LORIA & INRIA-Lorraine, Nancy, France</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Daniele</namePart><namePart type="family">Zucchelli</namePart><affiliation>Dipartimento di Informatica, Università degli Studi di Milano, Italia</affiliation><affiliation>LORIA & INRIA-Lorraine, Nancy, France</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">2006</dateIssued><copyrightDate encoding="w3cdtf">2006</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: The theory of arrays, introduced by McCarthy in his seminal paper “Toward a mathematical science of computation”, is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e. checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays has the algebraic structure of Presburger Arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger Arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to reuse as much as possible existing techniques so to ease the implementation of the proposed methods. To this end, we show how to use both model-theoretic and rewriting-based theorem proving (i.e., superposition) techniques to implement the instantiation strategies of the various extensions.</abstract><relatedItem type="host"><titleInfo><title>Logics in Artificial Intelligence</title><subTitle>10th European Conference, JELIA 2006 Liverpool, UK, September 13-15, 2006 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Michael</namePart><namePart type="family">Fisher</namePart><affiliation>Department of Computer Science, University of Liverpool, Liverpool, U.K.</affiliation><affiliation>E-mail: MFisher@liverpool.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Wiebe</namePart><namePart type="family">van der Hoek</namePart><affiliation>University of Liverpool, United Kingdom</affiliation><affiliation>E-mail: wiebe@csc.liv.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Boris</namePart><namePart type="family">Konev</namePart><affiliation>University of Liverpool, Liverpool, UK</affiliation><affiliation>E-mail: konev@liverpool.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Alexei</namePart><namePart type="family">Lisitsa</namePart><affiliation>Department of Computer Science, The University of Liverpool, </affiliation><affiliation>E-mail: alexei@csc.liv.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">2006</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="I14010">Programming Techniques</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic></subject><identifier type="DOI">10.1007/11853886</identifier><identifier type="ISBN">978-3-540-39625-3</identifier><identifier type="eISBN">978-3-540-39627-7</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">141360</identifier><identifier type="BookID">978-3-540-39627-7</identifier><identifier type="BookChapterCount">49</identifier><identifier type="BookVolumeNumber">4160</identifier><identifier type="BookSequenceNumber">4160</identifier><identifier type="PartChapterCount">34</identifier><part><date>2006</date><detail type="part"><title>II: Technical Papers</title></detail><detail type="volume"><number>4160</number><caption>vol.</caption></detail><extent unit="pages"><start>177</start><end>189</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2006</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>University of California, Los Angeles, CA, 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">2006</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>University of California, Los Angeles, CA, 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">Michael</namePart><namePart type="family">Fisher</namePart><affiliation>Department of Computer Science, University of Liverpool, Liverpool, U.K.</affiliation><affiliation>E-mail: MFisher@liverpool.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Wiebe</namePart><namePart type="family">van der Hoek</namePart><affiliation>University of Liverpool, United Kingdom</affiliation><affiliation>E-mail: wiebe@csc.liv.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Boris</namePart><namePart type="family">Konev</namePart><affiliation>University of Liverpool, Liverpool, UK</affiliation><affiliation>E-mail: konev@liverpool.ac.uk</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Alexei</namePart><namePart type="family">Lisitsa</namePart><affiliation>Department of Computer Science, The University of Liverpool, </affiliation><affiliation>E-mail: alexei@csc.liv.ac.uk</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><part><detail type="volume"><number>II</number><caption>vol.</caption></detail></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2006</recordOrigin></recordInfo></relatedItem><identifier type="istex">C0B0245ECBE1AE666144FE0A4F656023446D24D8</identifier><identifier type="ark">ark:/67375/HCB-H1JKPJRX-G</identifier><identifier type="DOI">10.1007/11853886_16</identifier><identifier type="ChapterID">16</identifier><identifier type="ChapterID">Chap16</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2006</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, 2006</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-H1JKPJRX-G/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 002D69 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002D69 | 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:C0B0245ECBE1AE666144FE0A4F656023446D24D8
|texte= Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
}}
| This area was generated with Dilib version V0.6.33. |  |