Completion for multiple reduction orderings
Identifieur interne : 000565 ( Istex/Corpus ); précédent : 000564; suivant : 000566Completion for multiple reduction orderings
Auteurs : Masahito Kurihara ; Hisashi Kondo ; Azuma OhuchiSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We present a completion procedure (called MKB) which works with multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard Kuuth-Bendix completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structure consisting of a pair s: t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s ↔ t. The idea is based on the observation that some of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough.
Url:
DOI: 10.1007/3-540-59200-8_48
Links to Exploration step
ISTEX:197B9AB55250430EA80D66CCF5A77337B0A3BC6DLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Completion for multiple reduction orderings</title><author><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name><affiliation><mods:affiliation>Department of Information Engineering, Hokkaido University, 060, Sapporo, Japan</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: kurihara@huie.hokudai.ac.jp</mods:affiliation></affiliation></author><author><name sortKey="Kondo, Hisashi" sort="Kondo, Hisashi" uniqKey="Kondo H" first="Hisashi" last="Kondo">Hisashi Kondo</name><affiliation><mods:affiliation>Department of Systems Engineering, Ibaraki University, 316, Hitachi, Japan</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: kondo@lily.dse.ibaraki.ac.jp</mods:affiliation></affiliation></author><author><name sortKey="Ohuchi, Azuma" sort="Ohuchi, Azuma" uniqKey="Ohuchi A" first="Azuma" last="Ohuchi">Azuma Ohuchi</name><affiliation><mods:affiliation>Department of Information Engineering, Hokkaido University, 060, Sapporo, Japan</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: ohuchi]@huie.hokudai.ac.jp</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:197B9AB55250430EA80D66CCF5A77337B0A3BC6D</idno><date when="1995" year="1995">1995</date><idno type="doi">10.1007/3-540-59200-8_48</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-F56CR514-2/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000565</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000565</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Completion for multiple reduction orderings</title><author><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name><affiliation><mods:affiliation>Department of Information Engineering, Hokkaido University, 060, Sapporo, Japan</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: kurihara@huie.hokudai.ac.jp</mods:affiliation></affiliation></author><author><name sortKey="Kondo, Hisashi" sort="Kondo, Hisashi" uniqKey="Kondo H" first="Hisashi" last="Kondo">Hisashi Kondo</name><affiliation><mods:affiliation>Department of Systems Engineering, Ibaraki University, 316, Hitachi, Japan</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: kondo@lily.dse.ibaraki.ac.jp</mods:affiliation></affiliation></author><author><name sortKey="Ohuchi, Azuma" sort="Ohuchi, Azuma" uniqKey="Ohuchi A" first="Azuma" last="Ohuchi">Azuma Ohuchi</name><affiliation><mods:affiliation>Department of Information Engineering, Hokkaido University, 060, Sapporo, Japan</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: ohuchi]@huie.hokudai.ac.jp</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</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: We present a completion procedure (called MKB) which works with multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard Kuuth-Bendix completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structure consisting of a pair s: t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s ↔ t. The idea is based on the observation that some of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Masahito Kurihara</name><affiliations><json:string>Department of Information Engineering, Hokkaido University, 060, Sapporo, Japan</json:string><json:string>E-mail: kurihara@huie.hokudai.ac.jp</json:string></affiliations></json:item><json:item><name>Hisashi Kondo</name><affiliations><json:string>Department of Systems Engineering, Ibaraki University, 316, Hitachi, Japan</json:string><json:string>E-mail: kondo@lily.dse.ibaraki.ac.jp</json:string></affiliations></json:item><json:item><name>Azuma Ohuchi</name><affiliations><json:string>Department of Information Engineering, Hokkaido University, 060, Sapporo, Japan</json:string><json:string>E-mail: ohuchi]@huie.hokudai.ac.jp</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-F56CR514-2</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>ReviewPaper</json:string></originalGenre><abstract>Abstract: We present a completion procedure (called MKB) which works with multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard Kuuth-Bendix completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structure consisting of a pair s: t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s ↔ t. The idea is based on the observation that some of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough.</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>167</abstractWordCount><abstractCharCount>1036</abstractCharCount><keywordCount>0</keywordCount><score>9.004</score><pdfWordCount>6556</pdfWordCount><pdfCharCount>29152</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>439.208 x 666 pts</pdfPageSize></qualityIndicators><title>Completion for multiple reduction orderings</title><chapterId><json:string>7</json:string><json:string>Chap7</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>1995</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>Gerhard Goos</name></json:item><json:item><name>Juris Hartmanis</name></json:item><json:item><name>Jan van Leeuwen</name></json:item></editor></serie><host><title>Rewriting Techniques and Applications</title><language><json:string>unknown</json:string></language><copyrightDate>1995</copyrightDate><doi><json:string>10.1007/3-540-59200-8</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-49223-8</json:string></eisbn><bookId><json:string>3540592008</json:string></bookId><isbn><json:string>978-3-540-59200-6</json:string></isbn><volume>914</volume><pages><first>71</first><last>85</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Jieh Hsiang</name></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</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><json:item><value>Symbolic and Algebraic Manipulation</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-F56CR514-2</json:string></ark><publicationDate>1995</publicationDate><copyrightDate>1995</copyrightDate><doi><json:string>10.1007/3-540-59200-8_48</json:string></doi><id>197B9AB55250430EA80D66CCF5A77337B0A3BC6D</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-F56CR514-2/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-F56CR514-2/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-F56CR514-2/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Completion for multiple reduction orderings</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag</licence></availability><date when="1995">1995</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">Completion for multiple reduction orderings</title><author><persName><forename type="first">Masahito</forename><surname>Kurihara</surname></persName><email>kurihara@huie.hokudai.ac.jp</email><affiliation><orgName type="department">Department of Information Engineering</orgName><orgName type="institution">Hokkaido University</orgName><address><postCode>060</postCode><settlement>Sapporo</settlement><country key="JP">JAPAN</country></address></affiliation></author><author><persName><forename type="first">Hisashi</forename><surname>Kondo</surname></persName><email>kondo@lily.dse.ibaraki.ac.jp</email><affiliation><orgName type="department">Department of Systems Engineering</orgName><orgName type="institution">Ibaraki University</orgName><address><postCode>316</postCode><settlement>Hitachi</settlement><country key="JP">JAPAN</country></address></affiliation></author><author><persName><forename type="first">Azuma</forename><surname>Ohuchi</surname></persName><email>ohuchi]@huie.hokudai.ac.jp</email><affiliation><orgName type="department">Department of Information Engineering</orgName><orgName type="institution">Hokkaido University</orgName><address><postCode>060</postCode><settlement>Sapporo</settlement><country key="JP">JAPAN</country></address></affiliation></author><idno type="istex">197B9AB55250430EA80D66CCF5A77337B0A3BC6D</idno><idno type="ark">ark:/67375/HCB-F56CR514-2</idno><idno type="DOI">10.1007/3-540-59200-8_48</idno></analytic><monogr><title level="m" type="main">Rewriting Techniques and Applications</title><title level="m" type="sub">6th International Conference, RTA-95 Kaiserslautern, Germany, April 5–7, 1995 Proceedings</title><idno type="DOI">10.1007/3-540-59200-8</idno><idno type="book-id">3540592008</idno><idno type="ISBN">978-3-540-59200-6</idno><idno type="eISBN">978-3-540-49223-8</idno><idno type="chapter-id">Chap7</idno><editor><persName><forename type="first">Jieh</forename><surname>Hsiang</surname></persName></editor><imprint><biblScope unit="vol">914</biblScope><biblScope unit="page" from="71">71</biblScope><biblScope unit="page" to="85">85</biblScope><biblScope unit="chapter-count">41</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><editor><persName><forename type="first">Gerhard</forename><surname>Goos</surname></persName></editor><editor><persName><forename type="first">Juris</forename><surname>Hartmanis</surname></persName></editor><editor><persName><forename type="first">Jan</forename><nameLink>van</nameLink><surname>Leeuwen</surname></persName></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>We present a completion procedure (called MKB) which works with multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard Kuuth-Bendix completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structure consisting of a pair <hi rend="italic">s: t</hi> of terms associated with the information to show which processes contain the rule <hi rend="italic">s → t</hi> (or <hi rend="italic">t → s</hi>) and which processes contain the equation <hi rend="italic">s ↔ t</hi>. The idea is based on the observation that some of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough.</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>I14037</label><item><term type="Secondary" subtype="priority-1">Programming Languages, Compilers, Interpreters</term></item><label>I1603X</label><item><term type="Secondary" subtype="priority-2">Logics and Meanings of Programs</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-3">Mathematical Logic and Formal Languages</term></item><label>I17052</label><item><term type="Secondary" subtype="priority-4">Symbolic and Algebraic Manipulation</term></item><label>I21017</label><item><term type="Secondary" subtype="priority-5">Artificial Intelligence (incl. Robotics)</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-F56CR514-2/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle><SeriesAbbreviatedTitle>Lect Notes Comput Sci</SeriesAbbreviatedTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Juris</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Jan</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor></EditorGroup></SeriesHeader><Book Language="En"><BookInfo MediaType="eBook" Language="En" BookProductType="Proceedings" TocLevels="0" NumberingStyle="Unnumbered"><BookID>3540592008</BookID><BookTitle>Rewriting Techniques and Applications</BookTitle><BookSubTitle>6th International Conference, RTA-95 Kaiserslautern, Germany, April 5–7, 1995 Proceedings</BookSubTitle><BookVolumeNumber>914</BookVolumeNumber><BookDOI>10.1007/3-540-59200-8</BookDOI><BookTitleID>42669</BookTitleID><BookPrintISBN>978-3-540-59200-6</BookPrintISBN><BookElectronicISBN>978-3-540-49223-8</BookElectronicISBN><BookChapterCount>41</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1995</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I14037" Priority="1" Type="Secondary">Programming Languages, Compilers, Interpreters</BookSubject><BookSubject Code="I1603X" Priority="2" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I16048" Priority="3" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><BookSubject Code="I17052" Priority="4" Type="Secondary">Symbolic and Algebraic Manipulation</BookSubject><BookSubject Code="I21017" Priority="5" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup></BookInfo><BookHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Jieh</GivenName><FamilyName>Hsiang</FamilyName></EditorName></Editor></EditorGroup></BookHeader><Chapter ID="Chap7" Language="En"><ChapterInfo ChapterType="ReviewPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ChapterID>7</ChapterID><ChapterDOI>10.1007/3-540-59200-8_48</ChapterDOI><ChapterSequenceNumber>7</ChapterSequenceNumber><ChapterTitle Language="En">Completion for multiple reduction orderings</ChapterTitle><ChapterCategory>Regular Papers</ChapterCategory><ChapterFirstPage>71</ChapterFirstPage><ChapterLastPage>85</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>1995</CopyrightYear></ChapterCopyright><ChapterHistory><OnlineDate><Year>2005</Year><Month>6</Month><Day>1</Day></OnlineDate></ChapterHistory><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><BookID>3540592008</BookID><BookTitle>Rewriting Techniques and Applications</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Masahito</GivenName><FamilyName>Kurihara</FamilyName></AuthorName><Contact><Email>kurihara@huie.hokudai.ac.jp</Email></Contact></Author><Author AffiliationIDS="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Hisashi</GivenName><FamilyName>Kondo</FamilyName></AuthorName><Contact><Email>kondo@lily.dse.ibaraki.ac.jp</Email></Contact></Author><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Azuma</GivenName><FamilyName>Ohuchi</FamilyName></AuthorName><Contact><Email>ohuchi]@huie.hokudai.ac.jp</Email></Contact></Author><Affiliation ID="Aff1"><OrgDivision>Department of Information Engineering</OrgDivision><OrgName>Hokkaido University</OrgName><OrgAddress><Postcode>060</Postcode><City>Sapporo</City><Country>Japan</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgDivision>Department of Systems Engineering</OrgDivision><OrgName>Ibaraki University</OrgName><OrgAddress><Postcode>316</Postcode><City>Hitachi</City><Country>Japan</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>We present a completion procedure (called MKB) which works with multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard Kuuth-Bendix completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structure consisting of a pair <Emphasis Type="Italic">s: t</Emphasis> of terms associated with the information to show which processes contain the rule <Emphasis Type="Italic">s → t</Emphasis> (or <Emphasis Type="Italic">t → s</Emphasis>) and which processes contain the equation <Emphasis Type="Italic">s ↔ t</Emphasis>. The idea is based on the observation that some of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Completion for multiple reduction orderings</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Completion for multiple reduction orderings</title></titleInfo><name type="personal"><namePart type="given">Masahito</namePart><namePart type="family">Kurihara</namePart><affiliation>Department of Information Engineering, Hokkaido University, 060, Sapporo, Japan</affiliation><affiliation>E-mail: kurihara@huie.hokudai.ac.jp</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Hisashi</namePart><namePart type="family">Kondo</namePart><affiliation>Department of Systems Engineering, Ibaraki University, 316, Hitachi, Japan</affiliation><affiliation>E-mail: kondo@lily.dse.ibaraki.ac.jp</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Azuma</namePart><namePart type="family">Ohuchi</namePart><affiliation>Department of Information Engineering, Hokkaido University, 060, Sapporo, Japan</affiliation><affiliation>E-mail: ohuchi]@huie.hokudai.ac.jp</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="ReviewPaper" 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">1995</dateIssued><copyrightDate encoding="w3cdtf">1995</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: We present a completion procedure (called MKB) which works with multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard Kuuth-Bendix completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structure consisting of a pair s: t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s ↔ t. The idea is based on the observation that some of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough.</abstract><relatedItem type="host"><titleInfo><title>Rewriting Techniques and Applications</title><subTitle>6th International Conference, RTA-95 Kaiserslautern, Germany, April 5–7, 1995 Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Jieh</namePart><namePart type="family">Hsiang</namePart><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">1995</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="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><topic authority="SpringerSubjectCodes" authorityURI="I17052">Symbolic and Algebraic Manipulation</topic><topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic></subject><identifier type="DOI">10.1007/3-540-59200-8</identifier><identifier type="ISBN">978-3-540-59200-6</identifier><identifier type="eISBN">978-3-540-49223-8</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">42669</identifier><identifier type="BookID">3540592008</identifier><identifier type="BookChapterCount">41</identifier><identifier type="BookVolumeNumber">914</identifier><part><date>1995</date><detail type="volume"><number>914</number><caption>vol.</caption></detail><extent unit="pages"><start>71</start><end>85</end></extent></part><recordInfo><recordOrigin>Springer-Verlag, 1995</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><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Juris</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jan</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">1995</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag, 1995</recordOrigin></recordInfo></relatedItem><identifier type="istex">197B9AB55250430EA80D66CCF5A77337B0A3BC6D</identifier><identifier type="ark">ark:/67375/HCB-F56CR514-2</identifier><identifier type="DOI">10.1007/3-540-59200-8_48</identifier><identifier type="ChapterID">7</identifier><identifier type="ChapterID">Chap7</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag, 1995</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, 1995</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-F56CR514-2/record.json</uri></json:item></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000565 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000565 | 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:197B9AB55250430EA80D66CCF5A77337B0A3BC6D
|texte= Completion for multiple reduction orderings
}}
| This area was generated with Dilib version V0.6.33. |  |