Tree Automata with Equality Constraints Modulo Equational Theories
Identifieur interne : 001900 ( Istex/Corpus ); précédent : 001899; suivant : 001901Tree Automata with Equality Constraints Modulo Equational Theories
Auteurs : Florent Jacquemard ; Michael Rusinowitch ; Laurent VigneronSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.
Url:
DOI: 10.1007/11814771_45
Links to Exploration step
ISTEX:6B5D7A874A050E8BCB345D15C19CDBF128CDD14FLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Tree Automata with Equality Constraints Modulo Equational Theories</title><author><name sortKey="Jacquemard, Florent" sort="Jacquemard, Florent" uniqKey="Jacquemard F" first="Florent" last="Jacquemard">Florent Jacquemard</name><affiliation><mods:affiliation>INRIA Futurs & LSV, UMR 8643, </mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: florent.jacquemard@inria.fr</mods:affiliation></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name><affiliation><mods:affiliation>LORIA & INRIA Lorraine, UMR 7503, </mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: rusi@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name><affiliation><mods:affiliation>LORIA & Univ. Nancy 2, UMR 7503, </mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: vigneron@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:6B5D7A874A050E8BCB345D15C19CDBF128CDD14F</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1007/11814771_45</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-S63RQ5TQ-K/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001900</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001900</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Tree Automata with Equality Constraints Modulo Equational Theories</title><author><name sortKey="Jacquemard, Florent" sort="Jacquemard, Florent" uniqKey="Jacquemard F" first="Florent" last="Jacquemard">Florent Jacquemard</name><affiliation><mods:affiliation>INRIA Futurs & LSV, UMR 8643, </mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: florent.jacquemard@inria.fr</mods:affiliation></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michael" last="Rusinowitch">Michael Rusinowitch</name><affiliation><mods:affiliation>LORIA & INRIA Lorraine, UMR 7503, </mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: rusi@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name><affiliation><mods:affiliation>LORIA & Univ. Nancy 2, UMR 7503, </mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: vigneron@loria.fr</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: This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Florent Jacquemard</name><affiliations><json:string>INRIA Futurs & LSV, UMR 8643,</json:string><json:string>E-mail: florent.jacquemard@inria.fr</json:string></affiliations></json:item><json:item><name>Michael Rusinowitch</name><affiliations><json:string>LORIA & INRIA Lorraine, UMR 7503,</json:string><json:string>E-mail: rusi@loria.fr</json:string></affiliations></json:item><json:item><name>Laurent Vigneron</name><affiliations><json:string>LORIA & Univ. Nancy 2, UMR 7503,</json:string><json:string>E-mail: vigneron@loria.fr</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-S63RQ5TQ-K</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>94</abstractWordCount><abstractCharCount>681</abstractCharCount><keywordCount>0</keywordCount><score>8.128</score><pdfWordCount>7140</pdfWordCount><pdfCharCount>34892</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize></qualityIndicators><title>Tree Automata with Equality Constraints Modulo Equational Theories</title><chapterId><json:string>45</json:string><json:string>Chap45</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><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>Automated Reasoning</title><language><json:string>unknown</json:string></language><copyrightDate>2006</copyrightDate><doi><json:string>10.1007/11814771</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-37188-5</json:string></eisbn><bookId><json:string>978-3-540-37188-5</json:string></bookId><isbn><json:string>978-3-540-37187-8</json:string></isbn><volume>4130</volume><pages><first>557</first><last>571</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Ulrich Furbach</name><affiliations><json:string>Department of Computer Science, Artificial Intelligence Research Group, University of Koblenz-Landau, Universitätsstr. 1, 56070, Koblenz</json:string><json:string>E-mail: uli@uni-koblenz.de</json:string></affiliations></json:item><json:item><name>Natarajan Shankar</name><affiliations><json:string>SRI International, MS EL256,, 333 Ravenswood Avenue, 94025-3493, Menlo Park, CA, USA</json:string><json:string>E-mail: shankar@csl.sri.com</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>Logics and Meanings of Programs</value></json:item><json:item><value>Software Engineering</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-S63RQ5TQ-K</json:string></ark><publicationDate>2006</publicationDate><copyrightDate>2006</copyrightDate><doi><json:string>10.1007/11814771_45</json:string></doi><id>6B5D7A874A050E8BCB345D15C19CDBF128CDD14F</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-S63RQ5TQ-K/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-S63RQ5TQ-K/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-S63RQ5TQ-K/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Tree Automata with Equality Constraints Modulo Equational Theories</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">Tree Automata with Equality Constraints Modulo Equational Theories</title><author><persName><forename type="first">Florent</forename><surname>Jacquemard</surname></persName><email>florent.jacquemard@inria.fr</email><affiliation><orgName type="institution">INRIA Futurs & LSV, UMR 8643</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Michael</forename><surname>Rusinowitch</surname></persName><email>rusi@loria.fr</email><affiliation><orgName type="institution">LORIA & INRIA Lorraine, UMR 7503</orgName><address><country key=""></country></address></affiliation></author><author><persName><forename type="first">Laurent</forename><surname>Vigneron</surname></persName><email>vigneron@loria.fr</email><affiliation><orgName type="institution">LORIA & Univ. Nancy 2, UMR 7503</orgName><address><country key=""></country></address></affiliation></author><idno type="istex">6B5D7A874A050E8BCB345D15C19CDBF128CDD14F</idno><idno type="ark">ark:/67375/HCB-S63RQ5TQ-K</idno><idno type="DOI">10.1007/11814771_45</idno></analytic><monogr><title level="m" type="main">Automated Reasoning</title><title level="m" type="sub">Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings</title><title level="m" type="part">Session 11. Decision Procedures</title><idno type="DOI">10.1007/11814771</idno><idno type="book-id">978-3-540-37188-5</idno><idno type="ISBN">978-3-540-37187-8</idno><idno type="eISBN">978-3-540-37188-5</idno><idno type="chapter-id">Chap45</idno><idno type="part-id">Part12</idno><editor><persName><forename type="first">Ulrich</forename><surname>Furbach</surname></persName><email>uli@uni-koblenz.de</email><affiliation><orgName type="department">Department of Computer Science, Artificial Intelligence Research Group</orgName><orgName type="institution">University of Koblenz-Landau</orgName><address><street>Universitätsstr. 1</street><postCode>56070</postCode><settlement>Koblenz</settlement></address></affiliation></editor><editor><persName><forename type="first">Natarajan</forename><surname>Shankar</surname></persName><email>shankar@csl.sri.com</email><affiliation><orgName type="institution">SRI International, MS EL256,</orgName><address><street>333 Ravenswood Avenue</street><postCode>94025-3493</postCode><settlement>Menlo Park</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><imprint><biblScope unit="vol">4130</biblScope><biblScope unit="page" from="557">557</biblScope><biblScope unit="page" to="571">571</biblScope><biblScope unit="chapter-count">53</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">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>This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in <hi rend="italic">e.g.</hi> software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.</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>I1603X</label><item><term type="Secondary" subtype="priority-3">Logics and Meanings of Programs</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-S63RQ5TQ-K/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-37188-5</BookID><BookTitle>Automated Reasoning</BookTitle><BookSubTitle>Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings</BookSubTitle><BookVolumeNumber>4130</BookVolumeNumber><BookSequenceNumber>4130</BookSequenceNumber><BookDOI>10.1007/11814771</BookDOI><BookTitleID>140713</BookTitleID><BookPrintISBN>978-3-540-37187-8</BookPrintISBN><BookElectronicISBN>978-3-540-37188-5</BookElectronicISBN><BookChapterCount>53</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="I16048" Priority="2" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I1603X" Priority="3" Type="Secondary">Logics and Meanings of Programs</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>Ulrich</GivenName><FamilyName>Furbach</FamilyName></EditorName><Contact><Email>uli@uni-koblenz.de</Email></Contact></Editor><Editor AffiliationIDS="Aff19"><EditorName DisplayOrder="Western"><GivenName>Natarajan</GivenName><FamilyName>Shankar</FamilyName></EditorName><Contact><Email>shankar@csl.sri.com</Email></Contact></Editor><Affiliation ID="Aff18"><OrgDivision>Department of Computer Science, Artificial Intelligence Research Group</OrgDivision><OrgName>University of Koblenz-Landau</OrgName><OrgAddress><Street>Universitätsstr. 1</Street><Postcode>56070</Postcode><City>Koblenz</City></OrgAddress></Affiliation><Affiliation ID="Aff19"><OrgName>SRI International, MS EL256,</OrgName><OrgAddress><Street>333 Ravenswood Avenue</Street><Postcode>94025-3493</Postcode><City>Menlo Park</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part12"><PartInfo TocLevels="0"><PartID>12</PartID><PartSequenceNumber>12</PartSequenceNumber><PartTitle>Session 11. Decision Procedures</PartTitle><PartChapterCount>4</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Automated Reasoning</BookTitle></PartContext></PartInfo><Chapter ID="Chap45" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>45</ChapterID><ChapterDOI>10.1007/11814771_45</ChapterDOI><ChapterSequenceNumber>45</ChapterSequenceNumber><ChapterTitle Language="En">Tree Automata with Equality Constraints Modulo Equational Theories</ChapterTitle><ChapterFirstPage>557</ChapterFirstPage><ChapterLastPage>571</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>12</PartID><BookID>978-3-540-37188-5</BookID><BookTitle>Automated Reasoning</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff20"><AuthorName DisplayOrder="Western"><GivenName>Florent</GivenName><FamilyName>Jacquemard</FamilyName></AuthorName><Contact><Email>florent.jacquemard@inria.fr</Email></Contact></Author><Author AffiliationIDS="Aff21"><AuthorName DisplayOrder="Western"><GivenName>Michael</GivenName><FamilyName>Rusinowitch</FamilyName></AuthorName><Contact><Email>rusi@loria.fr</Email></Contact></Author><Author AffiliationIDS="Aff22"><AuthorName DisplayOrder="Western"><GivenName>Laurent</GivenName><FamilyName>Vigneron</FamilyName></AuthorName><Contact><Email>vigneron@loria.fr</Email></Contact></Author><Affiliation ID="Aff20"><OrgName>INRIA Futurs & LSV, UMR 8643</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation><Affiliation ID="Aff21"><OrgName>LORIA & INRIA Lorraine, UMR 7503</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation><Affiliation ID="Aff22"><OrgName>LORIA & Univ. Nancy 2, UMR 7503</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in <Emphasis Type="Italic">e.g.</Emphasis> software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.</Para></Abstract><ArticleNote Type="Misc"><SimplePara>This work has been partially supported by the research projects RNTL PROUVÉ (No 03 V 360) and ACI–SI SATIN and ROSSIGNOL.</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Tree Automata with Equality Constraints Modulo Equational Theories</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Tree Automata with Equality Constraints Modulo Equational Theories</title></titleInfo><name type="personal"><namePart type="given">Florent</namePart><namePart type="family">Jacquemard</namePart><affiliation>INRIA Futurs & LSV, UMR 8643, </affiliation><affiliation>E-mail: florent.jacquemard@inria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Michael</namePart><namePart type="family">Rusinowitch</namePart><affiliation>LORIA & INRIA Lorraine, UMR 7503, </affiliation><affiliation>E-mail: rusi@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Laurent</namePart><namePart type="family">Vigneron</namePart><affiliation>LORIA & Univ. Nancy 2, UMR 7503, </affiliation><affiliation>E-mail: vigneron@loria.fr</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: This paper presents new classes of tree automata combining automata with equality test and automata modulo equational theories. We believe that these classes have a good potential for application in e.g. software verification. These tree automata are obtained by extending the standard Horn clause representations with equational conditions and rewrite systems. We show in particular that a generalized membership problem (extending the emptiness problem) is decidable by proving that the saturation of tree automata presentations with suitable paramodulation strategies terminates. Alternatively our results can be viewed as new decidable classes of first-order formula.</abstract><relatedItem type="host"><titleInfo><title>Automated Reasoning</title><subTitle>Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Ulrich</namePart><namePart type="family">Furbach</namePart><affiliation>Department of Computer Science, Artificial Intelligence Research Group, University of Koblenz-Landau, Universitätsstr. 1, 56070, Koblenz</affiliation><affiliation>E-mail: uli@uni-koblenz.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Natarajan</namePart><namePart type="family">Shankar</namePart><affiliation>SRI International, MS EL256,, 333 Ravenswood Avenue, 94025-3493, Menlo Park, CA, USA</affiliation><affiliation>E-mail: shankar@csl.sri.com</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="I16048">Mathematical Logic and Formal Languages</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic></subject><identifier type="DOI">10.1007/11814771</identifier><identifier type="ISBN">978-3-540-37187-8</identifier><identifier type="eISBN">978-3-540-37188-5</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">140713</identifier><identifier type="BookID">978-3-540-37188-5</identifier><identifier type="BookChapterCount">53</identifier><identifier type="BookVolumeNumber">4130</identifier><identifier type="BookSequenceNumber">4130</identifier><identifier type="PartChapterCount">4</identifier><part><date>2006</date><detail type="part"><title>Session 11. Decision Procedures</title></detail><detail type="volume"><number>4130</number><caption>vol.</caption></detail><extent unit="pages"><start>557</start><end>571</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">Ulrich</namePart><namePart type="family">Furbach</namePart><affiliation>Department of Computer Science, Artificial Intelligence Research Group, University of Koblenz-Landau, Universitätsstr. 1, 56070, Koblenz</affiliation><affiliation>E-mail: uli@uni-koblenz.de</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Natarajan</namePart><namePart type="family">Shankar</namePart><affiliation>SRI International, MS EL256,, 333 Ravenswood Avenue, 94025-3493, Menlo Park, CA, USA</affiliation><affiliation>E-mail: shankar@csl.sri.com</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, 2006</recordOrigin></recordInfo></relatedItem><identifier type="istex">6B5D7A874A050E8BCB345D15C19CDBF128CDD14F</identifier><identifier type="ark">ark:/67375/HCB-S63RQ5TQ-K</identifier><identifier type="DOI">10.1007/11814771_45</identifier><identifier type="ChapterID">45</identifier><identifier type="ChapterID">Chap45</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-S63RQ5TQ-K/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 001900 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001900 | 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:6B5D7A874A050E8BCB345D15C19CDBF128CDD14F
|texte= Tree Automata with Equality Constraints Modulo Equational Theories
}}
| This area was generated with Dilib version V0.6.33. |  |