{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,10,28]],"date-time":"2023-10-28T05:40:23Z","timestamp":1698471623961},"reference-count":19,"publisher":"Wiley","issue":"6","license":[{"start":{"date-parts":[[2007,3,21]],"date-time":"2007-03-21T00:00:00Z","timestamp":1174435200000},"content-version":"vor","delay-in-days":4097,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Systems &amp;amp; Computers in Japan"],"published-print":{"date-parts":[[1996,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The Knuth\u2010Bendix 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\u2010rewriting 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.<\/jats:p><jats: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.<\/jats:p><jats: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.<\/jats:p>","DOI":"10.1002\/scj.4690270604","type":"journal-article","created":{"date-parts":[[2007,7,8]],"date-time":"2007-07-08T11:18:39Z","timestamp":1183893519000},"page":"33-44","source":"Crossref","is-referenced-by-count":0,"title":["Completion of term\u2010rewriting systems with multiple reduction orderings"],"prefix":"10.1002","volume":"27","author":[{"given":"Hisashi","family":"Kondo","sequence":"first","affiliation":[]},{"given":"Masahito","family":"Kurihara","sequence":"additional","affiliation":[]},{"given":"Azuma","family":"Ohuchi","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2007,3,21]]},"reference":[{"issue":"1","key":"e_1_2_1_2_2","first-page":"47","article-title":"Basis of algebraic specification description for abstract data type (1)","volume":"25","author":"Ingaki Y.","year":"1984","journal-title":"Inf. Proc."},{"issue":"8","key":"e_1_2_1_3_2","first-page":"817","article-title":"Computation models for functional programming","volume":"29","author":"Togashi A.","year":"1988","journal-title":"Inf. Proc."},{"key":"e_1_2_1_4_2","unstructured":"A.Osuga K.SakaiandS.Honiden.A procedure to prove inductive theorem for equation theory. 9th Conv. Jap. Soc. Software Sci. pp.297\u2013300(1992)."},{"issue":"2","key":"e_1_2_1_5_2","first-page":"133","article-title":"Term rewriting systems and their applications","volume":"24","author":"Futatsugi K.","year":"1983","journal-title":"Inf. Proc."},{"key":"e_1_2_1_6_2","first-page":"223","volume-title":"Basic Theory of Computational Model","author":"Ida T.","year":"1991"},{"key":"e_1_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"issue":"4","key":"e_1_2_1_8_2","first-page":"520","article-title":"Inductive inference of term\u2010rewriting systems realizing algebras","volume":"6","author":"Togashi A.","year":"1991","journal-title":"Jour. Soc. Artif. Intel."},{"key":"e_1_2_1_9_2","first-page":"369","article-title":"How to prove equivalence of term rewriting systems without induction","volume":"90","author":"Toyama Y.","year":"1991","journal-title":"Theo. Comp. Sci."},{"issue":"9","key":"e_1_2_1_10_2","first-page":"1046","article-title":"Efficient termination verification of term\u2010rewriting systems based on reason maintenance system","volume":"32","author":"Kondo H.","year":"1991","journal-title":"Trans. Inf. Proc. Soc."},{"key":"e_1_2_1_11_2","first-page":"263","volume-title":"Simple Word Problems in Abstract Algebra","author":"Knuth D. E.","year":"1970"},{"issue":"1","key":"e_1_2_1_12_2","first-page":"2","article-title":"Knuth\u2010Bendix completion procedure and its application","volume":"4","author":"Sakai K.","year":"1987","journal-title":"Comput. Soft."},{"key":"e_1_2_1_13_2","unstructured":"M.Hermann.Vademecum of Divergent Term Rewriting Systems. Technical Report 88\u2010R\u2010022 Centre de Recherche en Infomatique de Nancy 1988"},{"key":"e_1_2_1_14_2","first-page":"1","volume-title":"Resolution of Equations in Algebraic Structures","author":"Bachmair L.","year":"1989"},{"key":"e_1_2_1_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(86)90081-0"},{"key":"e_1_2_1_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80022-6"},{"key":"e_1_2_1_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90002-7"},{"key":"e_1_2_1_18_2","unstructured":"L.Bachmair N.DershowitzandJ.Hsiang.Orderings for Equational Proofs. Proc. Sympo. on Logic in Computer Science Cambridge MA pp.346\u2013357(1986)."},{"key":"e_1_2_1_19_2","doi-asserted-by":"crossref","unstructured":"P.Lescanne.Computer Experiments with the REVE Term Rewriting System Generator. Proc. 10th ACM Sympo. on Principles of Programming Languages Austin TX pp.99\u2013108(1983).","DOI":"10.1145\/567067.567078"},{"key":"e_1_2_1_20_2","unstructured":"D.KapurandG.Sivakumar.Architecture of and Experiments with RRL a Rewrite Rule Laboratory. Proc. NSF Workshop on the Rewrite Rule Laboratory Rensellaervill NT pp.33\u201356(1984)."}],"container-title":["Systems and Computers in Japan"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fscj.4690270604","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/scj.4690270604","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,27]],"date-time":"2023-10-27T11:15:15Z","timestamp":1698405315000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/scj.4690270604"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,1]]},"references-count":19,"journal-issue":{"issue":"6","published-print":{"date-parts":[[1996,1]]}},"alternative-id":["10.1002\/scj.4690270604"],"URL":"https:\/\/doi.org\/10.1002\/scj.4690270604","archive":["Portico"],"relation":{},"ISSN":["0882-1666","1520-684X"],"issn-type":[{"value":"0882-1666","type":"print"},{"value":"1520-684X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,1]]}}}