Completion of term‐rewriting systems with multiple reduction orderings
Identifieur interne : 000143 ( Istex/Corpus ); précédent : 000142; suivant : 000144Completion of term‐rewriting systems with multiple reduction orderings
Auteurs : Hisashi Kondo ; Masahito Kurihara ; Azuma OhuchiSource :
- Systems and Computers in Japan [ 0882-1666 ] ; 1996.
English descriptors
- Teeft :
- Algorithm, Appropriate reduction, Artificial intelligence, Atm, Atms node, Azuma ohuchi, Completion algorithm, Completion procedure, Computer science, Confluence, Critical pair, Critical pairs, Data structure, Equation system, Execution time, Function symbols, Functional procedure, Functional programming, Hokkaido univ, Ibaraki univ, Inadequate reduction, Inference rule, Inference rules, Lexicographic path, Local confluence, Multiple context, Multiple reduction, Multiple reduction orderings, Node, Normal form, Ordinary completion procedure, Other words, Parallel execution, Precedence orderings, Proc, Procedure diverges, Reduction orderings, Rule laboratory, Single node, Substitution, Substitution instance, Third label, Trivial equation, Univ, Unnecessary nodes.
Abstract
The Knuth‐Bendix completion procedure results in one of the following, when the reduction ordering and the set of equations are given: (1) the procedure succeeds by generating a complete term‐rewriting system; (2) the procedure fails by not giving the orientation to an equation by the reduction ordering; and (3) the procedure diverges without being terminated. The success or failure of the completion procedure depends greatly on the reduction ordering. This paper proposes a completion procedure with multiple reduction orderings to reduce the burden of the user in determining the reduction ordering and to prevent the procedure from diverging due to the inadequate reduction ordering. To improve the efficiency, the data called node are used, based on the data structure of ATMS, which is an architecture proposed in the artificial intelligence. The parallel execution of the ordinary completion procedure is simulated under each reduction ordering. The property of ATMS to handle the multiple context is utilized, and the duplication of the inference is avoided by sharing the result of inference among the reduction orderings.
Url:
DOI: 10.1002/scj.4690270604
Links to Exploration step
ISTEX:06B7BCFB778A05D21BC2AC0ECA280A2A8A63FD4DLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Completion of term‐rewriting systems with multiple reduction orderings</title><author><name sortKey="Kondo, Hisashi" sort="Kondo, Hisashi" uniqKey="Kondo H" first="Hisashi" last="Kondo">Hisashi Kondo</name><affiliation><mods:affiliation>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</mods:affiliation></affiliation></author><author><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name><affiliation><mods:affiliation>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</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>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:06B7BCFB778A05D21BC2AC0ECA280A2A8A63FD4D</idno><date when="1996" year="1996">1996</date><idno type="doi">10.1002/scj.4690270604</idno><idno type="url">https://api.istex.fr/ark:/67375/WNG-X0RQM6Z0-P/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000143</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000143</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Completion of term‐rewriting systems with multiple reduction orderings</title><author><name sortKey="Kondo, Hisashi" sort="Kondo, Hisashi" uniqKey="Kondo H" first="Hisashi" last="Kondo">Hisashi Kondo</name><affiliation><mods:affiliation>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</mods:affiliation></affiliation></author><author><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name><affiliation><mods:affiliation>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</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>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j" type="main">Systems and Computers in Japan</title><title level="j" type="alt">SYSTEMS AND COMPUTERS IN JAPAN</title><idno type="ISSN">0882-1666</idno><idno type="eISSN">1520-684X</idno><imprint><biblScope unit="vol">27</biblScope><biblScope unit="issue">6</biblScope><biblScope unit="page" from="33">33</biblScope><biblScope unit="page" to="44">44</biblScope><biblScope unit="page-count">12</biblScope><publisher>Wiley Subscription Services, Inc., A Wiley Company</publisher><pubPlace>New York</pubPlace><date type="published" when="1996">1996</date></imprint><idno type="ISSN">0882-1666</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0882-1666</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Algorithm</term><term>Appropriate reduction</term><term>Artificial intelligence</term><term>Atm</term><term>Atms node</term><term>Azuma ohuchi</term><term>Completion algorithm</term><term>Completion procedure</term><term>Computer science</term><term>Confluence</term><term>Critical pair</term><term>Critical pairs</term><term>Data structure</term><term>Equation system</term><term>Execution time</term><term>Function symbols</term><term>Functional procedure</term><term>Functional programming</term><term>Hokkaido univ</term><term>Ibaraki univ</term><term>Inadequate reduction</term><term>Inference rule</term><term>Inference rules</term><term>Lexicographic path</term><term>Local confluence</term><term>Multiple context</term><term>Multiple reduction</term><term>Multiple reduction orderings</term><term>Node</term><term>Normal form</term><term>Ordinary completion procedure</term><term>Other words</term><term>Parallel execution</term><term>Precedence orderings</term><term>Proc</term><term>Procedure diverges</term><term>Reduction orderings</term><term>Rule laboratory</term><term>Single node</term><term>Substitution</term><term>Substitution instance</term><term>Third label</term><term>Trivial equation</term><term>Univ</term><term>Unnecessary nodes</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">The Knuth‐Bendix completion procedure results in one of the following, when the reduction ordering and the set of equations are given: (1) the procedure succeeds by generating a complete term‐rewriting system; (2) the procedure fails by not giving the orientation to an equation by the reduction ordering; and (3) the procedure diverges without being terminated. The success or failure of the completion procedure depends greatly on the reduction ordering. This paper proposes a completion procedure with multiple reduction orderings to reduce the burden of the user in determining the reduction ordering and to prevent the procedure from diverging due to the inadequate reduction ordering. To improve the efficiency, the data called node are used, based on the data structure of ATMS, which is an architecture proposed in the artificial intelligence. The parallel execution of the ordinary completion procedure is simulated under each reduction ordering. The property of ATMS to handle the multiple context is utilized, and the duplication of the inference is avoided by sharing the result of inference among the reduction orderings.</div></front></TEI><istex><corpusName>wiley</corpusName><keywords><teeft><json:string>node</json:string><json:string>completion procedure</json:string><json:string>reduction orderings</json:string><json:string>confluence</json:string><json:string>proc</json:string><json:string>critical pairs</json:string><json:string>atm</json:string><json:string>other words</json:string><json:string>univ</json:string><json:string>multiple reduction orderings</json:string><json:string>precedence orderings</json:string><json:string>execution time</json:string><json:string>functional procedure</json:string><json:string>inference rule</json:string><json:string>hokkaido univ</json:string><json:string>atms node</json:string><json:string>multiple reduction</json:string><json:string>critical pair</json:string><json:string>substitution instance</json:string><json:string>procedure diverges</json:string><json:string>function symbols</json:string><json:string>lexicographic path</json:string><json:string>inference rules</json:string><json:string>data structure</json:string><json:string>algorithm</json:string><json:string>parallel execution</json:string><json:string>single node</json:string><json:string>third label</json:string><json:string>completion algorithm</json:string><json:string>artificial intelligence</json:string><json:string>substitution</json:string><json:string>ibaraki univ</json:string><json:string>normal form</json:string><json:string>ordinary completion procedure</json:string><json:string>trivial equation</json:string><json:string>local confluence</json:string><json:string>appropriate reduction</json:string><json:string>inadequate reduction</json:string><json:string>multiple context</json:string><json:string>unnecessary nodes</json:string><json:string>functional programming</json:string><json:string>equation system</json:string><json:string>computer science</json:string><json:string>rule laboratory</json:string><json:string>azuma ohuchi</json:string></teeft></keywords><author><json:item><name>Hisashi Kondo</name><affiliations><json:string>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</json:string></affiliations></json:item><json:item><name>Masahito Kurihara</name><affiliations><json:string>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</json:string></affiliations></json:item><json:item><name>Azuma Ohuchi</name><affiliations><json:string>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Knuth‐Bendix completion procedure</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>termination</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>confluence</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>term‐rewriting</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>ATMS (assumption‐based TMS)</value></json:item></subject><articleId><json:string>SCJ4690270604</json:string></articleId><arkIstex>ark:/67375/WNG-X0RQM6Z0-P</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>article</json:string></originalGenre><abstract>The Knuth‐Bendix completion procedure results in one of the following, when the reduction ordering and the set of equations are given: (1) the procedure succeeds by generating a complete term‐rewriting system; (2) the procedure fails by not giving the orientation to an equation by the reduction ordering; and (3) the procedure diverges without being terminated. The success or failure of the completion procedure depends greatly on the reduction ordering. This paper proposes a completion procedure with multiple reduction orderings to reduce the burden of the user in determining the reduction ordering and to prevent the procedure from diverging due to the inadequate reduction ordering. To improve the efficiency, the data called node are used, based on the data structure of ATMS, which is an architecture proposed in the artificial intelligence. The parallel execution of the ordinary completion procedure is simulated under each reduction ordering. The property of ATMS to handle the multiple context is utilized, and the duplication of the inference is avoided by sharing the result of inference among the reduction orderings.</abstract><qualityIndicators><score>9.076</score><pdfWordCount>6143</pdfWordCount><pdfCharCount>31385</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>12</pdfPageCount><pdfPageSize>612 x 792 pts (letter)</pdfPageSize><refBibsNative>true</refBibsNative><abstractWordCount>173</abstractWordCount><abstractCharCount>1134</abstractCharCount><keywordCount>5</keywordCount></qualityIndicators><title>Completion of term‐rewriting systems with multiple reduction orderings</title><genre><json:string>article</json:string></genre><host><title>Systems and Computers in Japan</title><language><json:string>unknown</json:string></language><doi><json:string>10.1002/(ISSN)1520-684X</json:string></doi><issn><json:string>0882-1666</json:string></issn><eissn><json:string>1520-684X</json:string></eissn><publisherId><json:string>SCJ</json:string></publisherId><volume>27</volume><issue>6</issue><pages><first>33</first><last>44</last><total>12</total></pages><genre><json:string>journal</json:string></genre><subject><json:item><value>Article</value></json:item></subject></host><namedEntities><unitex><date></date><geogName></geogName><orgName></orgName><orgName_funder></orgName_funder><orgName_provider></orgName_provider><persName></persName><placeName></placeName><ref_url></ref_url><ref_bibl></ref_bibl><bibl></bibl></unitex></namedEntities><ark><json:string>ark:/67375/WNG-X0RQM6Z0-P</json:string></ark><categories><wos></wos><scienceMetrix><json:string>1 - applied sciences</json:string><json:string>2 - information & communication technologies</json:string><json:string>3 - artificial intelligence & image processing</json:string></scienceMetrix><scopus><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - Computational Theory and Mathematics</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - Hardware and Architecture</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - Information Systems</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Mathematics</json:string><json:string>3 - Theoretical Computer Science</json:string></scopus><inist><json:string>1 - sciences appliquees, technologies et medecines</json:string><json:string>2 - sciences exactes et technologie</json:string><json:string>3 - sciences et techniques communes</json:string><json:string>4 - mathematiques</json:string></inist></categories><publicationDate>1996</publicationDate><copyrightDate>1996</copyrightDate><doi><json:string>10.1002/scj.4690270604</json:string></doi><id>06B7BCFB778A05D21BC2AC0ECA280A2A8A63FD4D</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/WNG-X0RQM6Z0-P/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/WNG-X0RQM6Z0-P/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/WNG-X0RQM6Z0-P/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Completion of term‐rewriting systems with multiple reduction orderings</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>Wiley Subscription Services, Inc., A Wiley Company</publisher><pubPlace>New York</pubPlace><availability><licence>Copyright © 1996 Wiley Periodicals, Inc., A Wiley Company</licence></availability><date type="published" when="1996"></date></publicationStmt><notesStmt><note type="content-type" subtype="article" source="article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-6N5SZHKN-D">article</note><note type="publication-type" subtype="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note></notesStmt><sourceDesc><biblStruct type="article"><analytic><title level="a" type="main" xml:lang="en">Completion of term‐rewriting systems with multiple reduction orderings</title><title level="a" type="short" xml:lang="en">Completion of Term‐Rewriting Systems with Multiple Reduction Orderings</title><author xml:id="author-0000"><persName><forename type="first">Hisashi</forename><surname>Kondo</surname></persName><affiliation><orgName type="department">Faculty of Engineering</orgName><orgName type="institution">Hokkaido University</orgName><address><addrLine>Sapporo</addrLine><addrLine>Japan 060</addrLine><country key="JP"></country></address></affiliation><affiliation>Note: Currently, Dept. Systems Eng., Fac. Eng., Ibaraki Univ.</affiliation><note type="foot">Hisashi Kondo received his Master's degree (Inf. Eng.) in 1991 and his Ph.D. degree (Inf. Eng.) in 1994 from Hokkaido Univ. He was a Research Associate in 1994 in the Dept. System Eng., Ibaraki Univ. He is engaged in research on term‐rewriting system and program synthesis. He is a member of Inf. Proc. Soc.; and Soc. Artif. Intel.</note></author><author xml:id="author-0001"><persName><forename type="first">Masahito</forename><surname>Kurihara</surname></persName><affiliation><orgName type="department">Faculty of Engineering</orgName><orgName type="institution">Hokkaido University</orgName><address><addrLine>Sapporo</addrLine><addrLine>Japan 060</addrLine><country key="JP"></country></address></affiliation><note type="foot">Masahito Kurihara graduated in 1978 from the Dept. Electrical Eng., Hokkaido Univ., where he received his Master's degree (Id Eng.) in 1980 and became a Research Associate in the Dept. Electrical Eng., Hokkaido Univ. He also has a Ph.D. degree. He was a Lecturer in 1989 and Assoc. Prof. in 1990 in the Dept. Inf. Eng. He is engaged in research on system engineering, automated reasoning and term‐rewriting system. He is a member of Inf. Proc. Soc.; Jap. Soc. Software Sci.; Soc. Artif. Intel.; and EATCS (European Association Theoretical Computer Science).</note></author><author xml:id="author-0002"><persName><forename type="first">Azuma</forename><surname>Ohuchi</surname></persName><affiliation><orgName type="department">Faculty of Engineering</orgName><orgName type="institution">Hokkaido University</orgName><address><addrLine>Sapporo</addrLine><addrLine>Japan 060</addrLine><country key="JP"></country></address></affiliation><note type="foot">Azuma Ohuchi received his Dr. of Eng. degree (Electrical Eng.) in 1974 from Hokkaido Univ. At present, he is a Professor in the Dept. Inf. Eng., Hokkaido Univ. He is engaged in research on system information engineering, applied artificial intelligence and medical system. He is a member of Inf. Proc. Soc.; Soc. Artif. Intel.; IEEJ; Soc. Instr. Contr. Eng.; Jap. OR Soc.; Soc. Med. Inf.; Soc. Hosp. Manag.; and IEEE.</note></author><idno type="istex">06B7BCFB778A05D21BC2AC0ECA280A2A8A63FD4D</idno><idno type="ark">ark:/67375/WNG-X0RQM6Z0-P</idno><idno type="DOI">10.1002/scj.4690270604</idno><idno type="unit">SCJ4690270604</idno><idno type="toTypesetVersion">file:SCJ.SCJ4690270604.pdf</idno></analytic><monogr><title level="j" type="main">Systems and Computers in Japan</title><title level="j" type="alt">SYSTEMS AND COMPUTERS IN JAPAN</title><idno type="pISSN">0882-1666</idno><idno type="eISSN">1520-684X</idno><idno type="book-DOI">10.1002/(ISSN)1520-684X</idno><idno type="book-part-DOI">10.1002/scj.v27:6</idno><idno type="product">SCJ</idno><imprint><biblScope unit="vol">27</biblScope><biblScope unit="issue">6</biblScope><biblScope unit="page" from="33">33</biblScope><biblScope unit="page" to="44">44</biblScope><biblScope unit="page-count">12</biblScope><publisher>Wiley Subscription Services, Inc., A Wiley Company</publisher><pubPlace>New York</pubPlace><date type="published" when="1996"></date></imprint></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en" style="main"><head>Abstract</head><p>The Knuth‐Bendix completion procedure results in one of the following, when the reduction ordering and the set of equations are given: (1) the procedure succeeds by generating a complete term‐rewriting system; (2) the procedure fails by not giving the orientation to an equation by the reduction ordering; and (3) the procedure diverges without being terminated. The success or failure of the completion procedure depends greatly on the reduction ordering.</p><p>This paper proposes a completion procedure with multiple reduction orderings to reduce the burden of the user in determining the reduction ordering and to prevent the procedure from diverging due to the inadequate reduction ordering. To improve the efficiency, the data called node are used, based on the data structure of ATMS, which is an architecture proposed in the artificial intelligence. The parallel execution of the ordinary completion procedure is simulated under each reduction ordering.</p><p>The property of ATMS to handle the multiple context is utilized, and the duplication of the inference is avoided by sharing the result of inference among the reduction orderings.</p></abstract><textClass><keywords xml:lang="en"><term xml:id="kwd1">Knuth‐Bendix completion procedure</term><term xml:id="kwd2">termination</term><term xml:id="kwd3">confluence</term><term xml:id="kwd4">term‐rewriting</term><term xml:id="kwd5">ATMS (assumption‐based TMS)</term></keywords><keywords rend="articleCategory"><term>Article</term></keywords><keywords rend="tocHeading1"><term>Articles</term></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/WNG-X0RQM6Z0-P/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Wiley, elements deleted: body"><istex:xmlDeclaration>version="1.0" encoding="UTF-8" standalone="yes"</istex:xmlDeclaration><istex:document><component version="2.0" type="serialArticle" xml:lang="en"><header><publicationMeta level="product"><publisherInfo><publisherName>Wiley Subscription Services, Inc., A Wiley Company</publisherName><publisherLoc>New York</publisherLoc></publisherInfo><doi registered="yes">10.1002/(ISSN)1520-684X</doi><issn type="print">0882-1666</issn><issn type="electronic">1520-684X</issn><idGroup><id type="product" value="SCJ"></id></idGroup><titleGroup><title type="main" xml:lang="en" sort="SYSTEMS AND COMPUTERS IN JAPAN">Systems and Computers in Japan</title><title type="short">Syst. Comp. Jpn.</title></titleGroup></publicationMeta><publicationMeta level="part" position="60"><doi origin="wiley" registered="yes">10.1002/scj.v27:6</doi><numberingGroup><numbering type="journalVolume" number="27">27</numbering><numbering type="journalIssue">6</numbering></numberingGroup><coverDate startDate="1996">1996</coverDate></publicationMeta><publicationMeta level="unit" type="article" position="4" status="forIssue"><doi origin="wiley" registered="yes">10.1002/scj.4690270604</doi><idGroup><id type="unit" value="SCJ4690270604"></id></idGroup><countGroup><count type="pageTotal" number="12"></count></countGroup><titleGroup><title type="articleCategory">Article</title><title type="tocHeading1">Articles</title></titleGroup><copyright ownership="publisher">Copyright © 1996 Wiley Periodicals, Inc., A Wiley Company</copyright><eventGroup><event type="firstOnline" date="2007-03-21"></event><event type="publishedOnlineFinalForm" date="2007-03-21"></event><event type="xmlConverted" agent="Converter:JWSART34_TO_WML3G version:2.3.2 mode:FullText source:HeaderRef result:HeaderRef" date="2010-03-04"></event><event type="xmlConverted" agent="Converter:WILEY_ML3G_TO_WILEY_ML3GV2 version:3.8.8" date="2014-02-08"></event><event type="xmlConverted" agent="Converter:WML3G_To_WML3G version:4.1.7 mode:FullText,remove_FC" date="2014-11-04"></event></eventGroup><numberingGroup><numbering type="pageFirst">33</numbering><numbering type="pageLast">44</numbering></numberingGroup><linkGroup><link type="toTypesetVersion" href="file:SCJ.SCJ4690270604.pdf"></link></linkGroup></publicationMeta><contentMeta><countGroup><count type="figureTotal" number="5"></count><count type="tableTotal" number="2"></count><count type="referenceTotal" number="19"></count></countGroup><titleGroup><title type="main" xml:lang="en">Completion of term‐rewriting systems with multiple reduction orderings</title><title type="short" xml:lang="en">Completion of Term‐Rewriting Systems with Multiple Reduction Orderings</title></titleGroup><creators><creator xml:id="au1" creatorRole="author" affiliationRef="#af1" noteRef="#fn1 #fn2"><personName><givenNames>Hisashi</givenNames><familyName>Kondo</familyName></personName><jobTitle>Nonmember</jobTitle></creator><creator xml:id="au2" creatorRole="author" affiliationRef="#af1" noteRef="#fn3"><personName><givenNames>Masahito</givenNames><familyName>Kurihara</familyName></personName><jobTitle>Member</jobTitle></creator><creator xml:id="au3" creatorRole="author" affiliationRef="#af1" noteRef="#fn4"><personName><givenNames>Azuma</givenNames><familyName>Ohuchi</familyName></personName><jobTitle>Member</jobTitle></creator></creators><affiliationGroup><affiliation xml:id="af1" countryCode="JP" type="organization"><unparsedAffiliation>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</unparsedAffiliation></affiliation></affiliationGroup><keywordGroup xml:lang="en" type="author"><keyword xml:id="kwd1">Knuth‐Bendix completion procedure</keyword><keyword xml:id="kwd2">termination</keyword><keyword xml:id="kwd3">confluence</keyword><keyword xml:id="kwd4">term‐rewriting</keyword><keyword xml:id="kwd5">ATMS (assumption‐based TMS)</keyword></keywordGroup><abstractGroup><abstract type="main" xml:lang="en"><title type="main">Abstract</title><p>The Knuth‐Bendix completion procedure results in one of the following, when the reduction ordering and the set of equations are given: (1) the procedure succeeds by generating a complete term‐rewriting system; (2) the procedure fails by not giving the orientation to an equation by the reduction ordering; and (3) the procedure diverges without being terminated. The success or failure of the completion procedure depends greatly on the reduction ordering.</p><p>This paper proposes a completion procedure with multiple reduction orderings to reduce the burden of the user in determining the reduction ordering and to prevent the procedure from diverging due to the inadequate reduction ordering. To improve the efficiency, the data called node are used, based on the data structure of ATMS, which is an architecture proposed in the artificial intelligence. The parallel execution of the ordinary completion procedure is simulated under each reduction ordering.</p><p>The property of ATMS to handle the multiple context is utilized, and the duplication of the inference is avoided by sharing the result of inference among the reduction orderings.</p></abstract></abstractGroup></contentMeta><noteGroup><note xml:id="fn1"><p>Currently, Dept. Systems Eng., Fac. Eng., Ibaraki Univ.</p></note><note xml:id="fn2"><p>Hisashi Kondo received his Master's degree (Inf. Eng.) in 1991 and his Ph.D. degree (Inf. Eng.) in 1994 from Hokkaido Univ. He was a Research Associate in 1994 in the Dept. System Eng., Ibaraki Univ. He is engaged in research on term‐rewriting system and program synthesis. He is a member of Inf. Proc. Soc.; and Soc. Artif. Intel.</p></note><note xml:id="fn3"><p>Masahito Kurihara graduated in 1978 from the Dept. Electrical Eng., Hokkaido Univ., where he received his Master's degree (Id Eng.) in 1980 and became a Research Associate in the Dept. Electrical Eng., Hokkaido Univ. He also has a Ph.D. degree. He was a Lecturer in 1989 and Assoc. Prof. in 1990 in the Dept. Inf. Eng. He is engaged in research on system engineering, automated reasoning and term‐rewriting system. He is a member of Inf. Proc. Soc.; Jap. Soc. Software Sci.; Soc. Artif. Intel.; and EATCS (European Association Theoretical Computer Science).</p></note><note xml:id="fn4"><p>Azuma Ohuchi received his Dr. of Eng. degree (Electrical Eng.) in 1974 from Hokkaido Univ. At present, he is a Professor in the Dept. Inf. Eng., Hokkaido Univ. He is engaged in research on system information engineering, applied artificial intelligence and medical system. He is a member of Inf. Proc. Soc.; Soc. Artif. Intel.; IEEJ; Soc. Instr. Contr. Eng.; Jap. OR Soc.; Soc. Med. Inf.; Soc. Hosp. Manag.; and IEEE.</p></note></noteGroup></header></component></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Completion of term‐rewriting systems with multiple reduction orderings</title></titleInfo><titleInfo type="abbreviated" lang="en"><title>Completion of Term‐Rewriting Systems with Multiple Reduction Orderings</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Completion of term‐rewriting systems with multiple reduction orderings</title></titleInfo><name type="personal"><namePart type="given">Hisashi</namePart><namePart type="family">Kondo</namePart><affiliation>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</affiliation><description>Note: Currently, Dept. Systems Eng., Fac. Eng., Ibaraki Univ.</description><description>Hisashi Kondo received his Master's degree (Inf. Eng.) in 1991 and his Ph.D. degree (Inf. Eng.) in 1994 from Hokkaido Univ. He was a Research Associate in 1994 in the Dept. System Eng., Ibaraki Univ. He is engaged in research on term‐rewriting system and program synthesis. He is a member of Inf. Proc. Soc.; and Soc. Artif. Intel.</description><role><roleTerm type="text">author</roleTerm></role><description>Nonmember</description></name><name type="personal"><namePart type="given">Masahito</namePart><namePart type="family">Kurihara</namePart><affiliation>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</affiliation><description>Masahito Kurihara graduated in 1978 from the Dept. Electrical Eng., Hokkaido Univ., where he received his Master's degree (Id Eng.) in 1980 and became a Research Associate in the Dept. Electrical Eng., Hokkaido Univ. He also has a Ph.D. degree. He was a Lecturer in 1989 and Assoc. Prof. in 1990 in the Dept. Inf. Eng. He is engaged in research on system engineering, automated reasoning and term‐rewriting system. He is a member of Inf. Proc. Soc.; Jap. Soc. Software Sci.; Soc. Artif. Intel.; and EATCS (European Association Theoretical Computer Science).</description><role><roleTerm type="text">author</roleTerm></role><description>Member</description></name><name type="personal"><namePart type="given">Azuma</namePart><namePart type="family">Ohuchi</namePart><affiliation>Faculty of Engineering, Hokkaido University, Sapporo, Japan 060</affiliation><description>Azuma Ohuchi received his Dr. of Eng. degree (Electrical Eng.) in 1974 from Hokkaido Univ. At present, he is a Professor in the Dept. Inf. Eng., Hokkaido Univ. He is engaged in research on system information engineering, applied artificial intelligence and medical system. He is a member of Inf. Proc. Soc.; Soc. Artif. Intel.; IEEJ; Soc. Instr. Contr. Eng.; Jap. OR Soc.; Soc. Med. Inf.; Soc. Hosp. Manag.; and IEEE.</description><role><roleTerm type="text">author</roleTerm></role><description>Member</description></name><typeOfResource>text</typeOfResource><genre type="article" displayLabel="article" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-6N5SZHKN-D">article</genre><originInfo><publisher>Wiley Subscription Services, Inc., A Wiley Company</publisher><place><placeTerm type="text">New York</placeTerm></place><dateIssued encoding="w3cdtf">1996</dateIssued><copyrightDate encoding="w3cdtf">1996</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><physicalDescription><extent unit="figures">5</extent><extent unit="tables">2</extent><extent unit="references">19</extent></physicalDescription><abstract lang="en">The Knuth‐Bendix completion procedure results in one of the following, when the reduction ordering and the set of equations are given: (1) the procedure succeeds by generating a complete term‐rewriting system; (2) the procedure fails by not giving the orientation to an equation by the reduction ordering; and (3) the procedure diverges without being terminated. The success or failure of the completion procedure depends greatly on the reduction ordering. This paper proposes a completion procedure with multiple reduction orderings to reduce the burden of the user in determining the reduction ordering and to prevent the procedure from diverging due to the inadequate reduction ordering. To improve the efficiency, the data called node are used, based on the data structure of ATMS, which is an architecture proposed in the artificial intelligence. The parallel execution of the ordinary completion procedure is simulated under each reduction ordering. The property of ATMS to handle the multiple context is utilized, and the duplication of the inference is avoided by sharing the result of inference among the reduction orderings.</abstract><subject lang="en"><genre>keywords</genre><topic>Knuth‐Bendix completion procedure</topic><topic>termination</topic><topic>confluence</topic><topic>term‐rewriting</topic><topic>ATMS (assumption‐based TMS)</topic></subject><relatedItem type="host"><titleInfo><title>Systems and Computers in Japan</title></titleInfo><titleInfo type="abbreviated"><title>Syst. Comp. Jpn.</title></titleInfo><genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><subject><genre>article-category</genre><topic>Article</topic></subject><identifier type="ISSN">0882-1666</identifier><identifier type="eISSN">1520-684X</identifier><identifier type="DOI">10.1002/(ISSN)1520-684X</identifier><identifier type="PublisherID">SCJ</identifier><part><date>1996</date><detail type="volume"><caption>vol.</caption><number>27</number></detail><detail type="issue"><caption>no.</caption><number>6</number></detail><extent unit="pages"><start>33</start><end>44</end><total>12</total></extent></part></relatedItem><identifier type="istex">06B7BCFB778A05D21BC2AC0ECA280A2A8A63FD4D</identifier><identifier type="ark">ark:/67375/WNG-X0RQM6Z0-P</identifier><identifier type="DOI">10.1002/scj.4690270604</identifier><identifier type="ArticleID">SCJ4690270604</identifier><accessCondition type="use and reproduction" contentType="copyright">Copyright © 1996 Wiley Periodicals, Inc., A Wiley Company</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-L0C46X92-X">wiley</recordContentSource><recordOrigin>Wiley Subscription Services, Inc., A Wiley Company</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/WNG-X0RQM6Z0-P/record.json</uri></json:item></metadata><serie></serie></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 000143 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000143 | 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:06B7BCFB778A05D21BC2AC0ECA280A2A8A63FD4D
|texte= Completion of term‐rewriting systems with multiple reduction orderings
}}
| This area was generated with Dilib version V0.6.33. |  |