Matching in a Class of Combined Non-disjoint Theories
Identifieur interne : 001E68 ( Istex/Corpus ); précédent : 001E67; suivant : 001E69Matching in a Class of Combined Non-disjoint Theories
Auteurs : Christophe RingeissenSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Solving equational problems is an ubiquitous process in automated deduction, where one needs for instance unification in completion procedures to compute critical pairs, and matching to apply rewrite rules. We present new equational matching and unification results in some combinations of non-disjoint equational theories. Some results are already known for theories sharing an appropriate notion of constructors. We investigate the idea of considering theories that are not explicitly based on the notion of constructors. In this direction, a new class of theories is presented, where a theory is defined as a union of two subtheories, one such that shared symbols do not affect the behavior of the theory, and another one given by a term rewrite system on shared symbols. Matching and unification problems are studied for this class of theories, and for unions of theories in this class. Results obtained for the matching problem are particularly relevant.
Url:
DOI: 10.1007/978-3-540-45085-6_17
Links to Exploration step
ISTEX:848CD1B788CEF025D0459457FAA34FA0A26EDE99Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Matching in a Class of Combined Non-disjoint Theories</title><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation><mods:affiliation>LORIA – INRIA, 615, rue du Jardin Botanique, BP 101, 54602, Villers-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Christophe.Ringeissen@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:848CD1B788CEF025D0459457FAA34FA0A26EDE99</idno><date when="2003" year="2003">2003</date><idno type="doi">10.1007/978-3-540-45085-6_17</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-73CMT166-6/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001E68</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001E68</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Matching in a Class of Combined Non-disjoint Theories</title><author><name sortKey="Ringeissen, Christophe" sort="Ringeissen, Christophe" uniqKey="Ringeissen C" first="Christophe" last="Ringeissen">Christophe Ringeissen</name><affiliation><mods:affiliation>LORIA – INRIA, 615, rue du Jardin Botanique, BP 101, 54602, Villers-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Christophe.Ringeissen@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: Solving equational problems is an ubiquitous process in automated deduction, where one needs for instance unification in completion procedures to compute critical pairs, and matching to apply rewrite rules. We present new equational matching and unification results in some combinations of non-disjoint equational theories. Some results are already known for theories sharing an appropriate notion of constructors. We investigate the idea of considering theories that are not explicitly based on the notion of constructors. In this direction, a new class of theories is presented, where a theory is defined as a union of two subtheories, one such that shared symbols do not affect the behavior of the theory, and another one given by a term rewrite system on shared symbols. Matching and unification problems are studied for this class of theories, and for unions of theories in this class. Results obtained for the matching problem are particularly relevant.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Christophe Ringeissen</name><affiliations><json:string>LORIA – INRIA, 615, rue du Jardin Botanique, BP 101, 54602, Villers-lès-Nancy Cedex, France</json:string><json:string>E-mail: Christophe.Ringeissen@loria.fr</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-73CMT166-6</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: Solving equational problems is an ubiquitous process in automated deduction, where one needs for instance unification in completion procedures to compute critical pairs, and matching to apply rewrite rules. We present new equational matching and unification results in some combinations of non-disjoint equational theories. Some results are already known for theories sharing an appropriate notion of constructors. We investigate the idea of considering theories that are not explicitly based on the notion of constructors. In this direction, a new class of theories is presented, where a theory is defined as a union of two subtheories, one such that shared symbols do not affect the behavior of the theory, and another one given by a term rewrite system on shared symbols. Matching and unification problems are studied for this class of theories, and for unions of theories in this class. Results obtained for the matching problem are particularly relevant.</abstract><qualityIndicators><score>8.788</score><pdfWordCount>7048</pdfWordCount><pdfCharCount>32880</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>16</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>149</abstractWordCount><abstractCharCount>969</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Matching in a Class of Combined Non-disjoint Theories</title><chapterId><json:string>17</json:string><json:string>Chap17</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>2003</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>Gerhard Goos</name><affiliations><json:string>Karlsruhe University, Germany</json:string></affiliations></json:item><json:item><name>Juris Hartmanis</name><affiliations><json:string>Cornell University, NY, USA</json:string></affiliations></json:item><json:item><name>Jan van Leeuwen</name><affiliations><json:string>Utrecht University, The Netherlands</json:string></affiliations></json:item></editor></serie><host><title>Automated Deduction – CADE-19</title><language><json:string>unknown</json:string></language><copyrightDate>2003</copyrightDate><doi><json:string>10.1007/b11829</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-45085-6</json:string></eisbn><bookId><json:string>978-3-540-45085-6</json:string></bookId><isbn><json:string>978-3-540-40559-7</json:string></isbn><volume>2741</volume><pages><first>212</first><last>227</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Franz Baader</name><affiliations><json:string>Theoretical Computer Science, TU Dresden, Germany</json:string><json:string>E-mail: baader@tcs.inf.tu-dresden.de</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 Languages, Compilers, Interpreters</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-73CMT166-6</json:string></ark><publicationDate>2003</publicationDate><copyrightDate>2003</copyrightDate><doi><json:string>10.1007/978-3-540-45085-6_17</json:string></doi><id>848CD1B788CEF025D0459457FAA34FA0A26EDE99</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-73CMT166-6/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-73CMT166-6/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-73CMT166-6/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Matching in a Class of Combined Non-disjoint Theories</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2003">2003</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">Matching in a Class of Combined Non-disjoint Theories</title><author><persName><forename type="first">Christophe</forename><surname>Ringeissen</surname></persName><email>Christophe.Ringeissen@loria.fr</email><affiliation><orgName type="institution">LORIA – INRIA</orgName><address><street>615, rue du Jardin Botanique</street><postBox>BP 101</postBox><postCode>54602</postCode><settlement>Villers-lès-Nancy Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">848CD1B788CEF025D0459457FAA34FA0A26EDE99</idno><idno type="ark">ark:/67375/HCB-73CMT166-6</idno><idno type="DOI">10.1007/978-3-540-45085-6_17</idno></analytic><monogr><title level="m" type="main">Automated Deduction – CADE-19</title><title level="m" type="sub">19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28 – August 2, 2003. Proceedings</title><title level="m" type="part">Session 6</title><idno type="DOI">10.1007/b11829</idno><idno type="book-id">978-3-540-45085-6</idno><idno type="ISBN">978-3-540-40559-7</idno><idno type="eISBN">978-3-540-45085-6</idno><idno type="chapter-id">Chap17</idno><idno type="part-id">Part6</idno><editor><persName><forename type="first">Franz</forename><surname>Baader</surname></persName><email>baader@tcs.inf.tu-dresden.de</email><affiliation><orgName type="department">Theoretical Computer Science</orgName><orgName type="institution">TU Dresden</orgName><address><country key="DE">GERMANY</country></address></affiliation></editor><imprint><biblScope unit="vol">2741</biblScope><biblScope unit="page" from="212">212</biblScope><biblScope unit="page" to="227">227</biblScope><biblScope unit="chapter-count">41</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">Gerhard</forename><surname>Goos</surname></persName><affiliation><orgName type="institution">Karlsruhe University</orgName><address><country key="DE">GERMANY</country></address></affiliation></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName><affiliation><orgName type="institution">Cornell University</orgName><address><region>NY</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Jan</forename><nameLink>van</nameLink><surname>Leeuwen</surname></persName><affiliation><orgName type="institution">Utrecht University</orgName><address><country key=""></country></address></affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>Solving equational problems is an ubiquitous process in automated deduction, where one needs for instance unification in completion procedures to compute critical pairs, and matching to apply rewrite rules. We present new equational matching and unification results in some combinations of non-disjoint equational theories. Some results are already known for theories sharing an appropriate notion of constructors. We investigate the idea of considering theories that are not explicitly based on the notion of constructors. In this direction, a new class of theories is presented, where a theory is defined as a union of two subtheories, one such that shared symbols do not affect the behavior of the theory, and another one given by a term rewrite system on shared symbols. Matching and unification problems are studied for this class of theories, and for unions of theories in this class. Results obtained for the matching problem are particularly relevant.</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>I14037</label><item><term type="Secondary" subtype="priority-2">Programming Languages, Compilers, Interpreters</term></item><label>I1603X</label><item><term type="Secondary" subtype="priority-3">Logics and Meanings of Programs</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-4">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-73CMT166-6/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>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Karlsruhe University</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Cornell University</OrgName><OrgAddress><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>Utrecht University</OrgName><OrgAddress><Country>The Netherlands</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><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="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Affiliation ID="Aff4"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><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-45085-6</BookID><BookTitle>Automated Deduction – CADE-19</BookTitle><BookSubTitle>19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28 – August 2, 2003. Proceedings</BookSubTitle><BookVolumeNumber>2741</BookVolumeNumber><BookSequenceNumber>2741</BookSequenceNumber><BookDOI>10.1007/b11829</BookDOI><BookTitleID>77379</BookTitleID><BookPrintISBN>978-3-540-40559-7</BookPrintISBN><BookElectronicISBN>978-3-540-45085-6</BookElectronicISBN><BookChapterCount>41</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2003</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="I14037" Priority="2" Type="Secondary">Programming Languages, Compilers, Interpreters</BookSubject><BookSubject Code="I1603X" Priority="3" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I16048" Priority="4" 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="Aff6"><EditorName DisplayOrder="Western"><GivenName>Franz</GivenName><FamilyName>Baader</FamilyName></EditorName><Contact><Email>baader@tcs.inf.tu-dresden.de</Email></Contact></Editor><Affiliation ID="Aff6"><OrgDivision>Theoretical Computer Science</OrgDivision><OrgName>TU Dresden</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part6"><PartInfo TocLevels="0"><PartID>6</PartID><PartSequenceNumber>6</PartSequenceNumber><PartTitle>Session 6</PartTitle><PartChapterCount>4</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Automated Deduction – CADE-19</BookTitle></PartContext></PartInfo><Chapter ID="Chap17" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>17</ChapterID><ChapterDOI>10.1007/978-3-540-45085-6_17</ChapterDOI><ChapterSequenceNumber>17</ChapterSequenceNumber><ChapterTitle Language="En">Matching in a Class of Combined Non-disjoint Theories</ChapterTitle><ChapterFirstPage>212</ChapterFirstPage><ChapterLastPage>227</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2003</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>6</PartID><BookID>978-3-540-45085-6</BookID><BookTitle>Automated Deduction – CADE-19</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff7"><AuthorName DisplayOrder="Western"><GivenName>Christophe</GivenName><FamilyName>Ringeissen</FamilyName></AuthorName><Contact><Email>Christophe.Ringeissen@loria.fr</Email></Contact></Author><Affiliation ID="Aff7"><OrgName>LORIA – INRIA</OrgName><OrgAddress><Street>615, rue du Jardin Botanique</Street><Postbox>BP 101</Postbox><Postcode>54602</Postcode><City>Villers-lès-Nancy Cedex</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>Solving equational problems is an ubiquitous process in automated deduction, where one needs for instance unification in completion procedures to compute critical pairs, and matching to apply rewrite rules. We present new equational matching and unification results in some combinations of non-disjoint equational theories. Some results are already known for theories sharing an appropriate notion of constructors. We investigate the idea of considering theories that are not explicitly based on the notion of constructors. In this direction, a new class of theories is presented, where a theory is defined as a union of two subtheories, one such that shared symbols do not affect the behavior of the theory, and another one given by a term rewrite system on shared symbols. Matching and unification problems are studied for this class of theories, and for unions of theories in this class. Results obtained for the matching problem are particularly relevant.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Matching in a Class of Combined Non-disjoint Theories</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Matching in a Class of Combined Non-disjoint Theories</title></titleInfo><name type="personal"><namePart type="given">Christophe</namePart><namePart type="family">Ringeissen</namePart><affiliation>LORIA – INRIA, 615, rue du Jardin Botanique, BP 101, 54602, Villers-lès-Nancy Cedex, France</affiliation><affiliation>E-mail: Christophe.Ringeissen@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">2003</dateIssued><copyrightDate encoding="w3cdtf">2003</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: Solving equational problems is an ubiquitous process in automated deduction, where one needs for instance unification in completion procedures to compute critical pairs, and matching to apply rewrite rules. We present new equational matching and unification results in some combinations of non-disjoint equational theories. Some results are already known for theories sharing an appropriate notion of constructors. We investigate the idea of considering theories that are not explicitly based on the notion of constructors. In this direction, a new class of theories is presented, where a theory is defined as a union of two subtheories, one such that shared symbols do not affect the behavior of the theory, and another one given by a term rewrite system on shared symbols. Matching and unification problems are studied for this class of theories, and for unions of theories in this class. Results obtained for the matching problem are particularly relevant.</abstract><relatedItem type="host"><titleInfo><title>Automated Deduction – CADE-19</title><subTitle>19th International Conference on Automated Deduction, Miami Beach, FL, USA, July 28 – August 2, 2003. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Franz</namePart><namePart type="family">Baader</namePart><affiliation>Theoretical Computer Science, TU Dresden, Germany</affiliation><affiliation>E-mail: baader@tcs.inf.tu-dresden.de</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">2003</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="I14037">Programming Languages, Compilers, Interpreters</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic></subject><identifier type="DOI">10.1007/b11829</identifier><identifier type="ISBN">978-3-540-40559-7</identifier><identifier type="eISBN">978-3-540-45085-6</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">77379</identifier><identifier type="BookID">978-3-540-45085-6</identifier><identifier type="BookChapterCount">41</identifier><identifier type="BookVolumeNumber">2741</identifier><identifier type="BookSequenceNumber">2741</identifier><identifier type="PartChapterCount">4</identifier><part><date>2003</date><detail type="part"><title>Session 6</title></detail><detail type="volume"><number>2741</number><caption>vol.</caption></detail><extent unit="pages"><start>212</start><end>227</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2003</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><affiliation>Karlsruhe University, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><affiliation>Cornell University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><affiliation>Utrecht University, The Netherlands</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2003</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title></titleInfo><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Goos</namePart><affiliation>Karlsruhe University, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><affiliation>Cornell University, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><affiliation>Utrecht University, The Netherlands</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><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">Franz</namePart><namePart type="family">Baader</namePart><affiliation>Theoretical Computer Science, TU Dresden, Germany</affiliation><affiliation>E-mail: baader@tcs.inf.tu-dresden.de</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, 2003</recordOrigin></recordInfo></relatedItem><identifier type="istex">848CD1B788CEF025D0459457FAA34FA0A26EDE99</identifier><identifier type="ark">ark:/67375/HCB-73CMT166-6</identifier><identifier type="DOI">10.1007/978-3-540-45085-6_17</identifier><identifier type="ChapterID">17</identifier><identifier type="ChapterID">Chap17</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2003</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, 2003</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-73CMT166-6/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 001E68 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 001E68 | 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:848CD1B788CEF025D0459457FAA34FA0A26EDE99
|texte= Matching in a Class of Combined Non-disjoint Theories
}}
| This area was generated with Dilib version V0.6.33. |  |