{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:50Z","timestamp":1725663530837},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540192428"},{"type":"electronic","value":"9783540391661"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-19242-5_6","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T20:05:09Z","timestamp":1330200309000},"page":"62-83","source":"Crossref","is-referenced-by-count":17,"title":["A completion procedure for conditional equations"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"6_CR1","unstructured":"Solvable cases of the decision problem. North-Holland, 1954."},{"key":"6_CR2","unstructured":"Bachmair, L.: Proof methods for equational theories. PhD-Thesis, U. of Illinois, Urbana Champaign, 1987."},{"key":"6_CR3","unstructured":"Bachmair, L., Dershowitz, N. and Hsiang, J.: Proof orderings for equational proofs. Proc. LICS 86, 346\u2013357."},{"key":"6_CR4","unstructured":"Bertling, H., Ganzinger, H. and Sch\u00e4fers, R.: CEC: A system for conditional equation completion. User Manual, U. Dortmund, 1987."},{"key":"6_CR5","volume-title":"Conditional rewrite rules: Confluence and termination. Report IW 198\/82","author":"J. Bergstra","year":"1982","unstructured":"Bergstra, J. and Klop, J.W.: Conditional rewrite rules: Confluence and termination. Report IW 198\/82, Mathematisch Centrum, Amsterdam, 1982."},{"key":"6_CR6","first-page":"180","volume":"202","author":"N. Dershowitz","year":"1985","unstructured":"Dershowitz, N.: Termination. Proc. RTA 1985, LNCS 202 1985, 180\u2013224.","journal-title":"LNCS"},{"key":"6_CR7","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N. and Manna, Z.: Proving termination with multiset orderings. CACM 22 (1979), 465\u2013476.","journal-title":"CACM"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Ganzinger, H.: Ground term confluence in parametric conditional equational specifications. Proc. STACS 1987, LNCS 247, 1987.","DOI":"10.1007\/BFb0039613"},{"key":"6_CR9","first-page":"349","volume-title":"Formal Languages: Perspectives and open Problems","author":"G. Huet","year":"1980","unstructured":"Huet, G. and Oppen, D.C.: Equations and Rewrite Rules. A Survey. In: R. Book (ed): Formal Languages: Perspectives and open Problems. Academic Press, New York, 1980, 349\u2013405."},{"key":"6_CR10","first-page":"11","volume":"23","author":"G. Huet","year":"1981","unstructured":"Huet, G.: A complete proof of the correctness of the Knuth-Bendix completion algorithm. JCSS 23 (1981), 11\u201321.","journal-title":"JCSS"},{"key":"6_CR11","first-page":"543","volume":"204","author":"H. Hussmann","year":"1985","unstructured":"Hussmann, H.: Unification in conditional-equational theories. Proc. Eurocal 1985, LNCS 204, 1985, 543\u2013553.","journal-title":"LNCS"},{"key":"6_CR12","unstructured":"Jouannaud, J.P. and Waldmann, B.: Reductive conditional term rewriting systems. Proc. 3rd TC2 Working Conference on the Formal Description of Prog. Concepts, Ebberup, Denmark, Aug. 1986, North-Holland, to appear."},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/0304-3975(84)90087-2","volume":"33","author":"St. Kaplan","year":"1984","unstructured":"Kaplan, St.: Conditional rewrite rules. TCS 33 (1984), 175\u2013193.","journal-title":"TCS"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Kaplan, St.: Fair conditional term rewrite systems: unification, termination and confluence. Report 194, U. de Paris-Sud, Centre d'Orsay, Nov. 1984.","DOI":"10.1007\/978-3-662-09691-8_11"},{"key":"6_CR15","first-page":"25","volume":"256","author":"St. Kaplan","year":"1987","unstructured":"Kaplan, St.: A compiler for conditional term rewriting. Proc. RTA 1987, LNCS 256, 1987, 25\u201341.","journal-title":"LNCS"},{"key":"6_CR16","unstructured":"Kaplan, St. and Remy J.-L.: Completion algorithms for conditional rewriting systems. MCC Workshop on Resolution of Equations in Algebraic Structures, Austin, May 1987."},{"key":"6_CR17","unstructured":"Kounalis, E. and Rusinowitch, M.: On word problems in Horn logic. This volume."},{"key":"6_CR18","first-page":"390","volume":"204","author":"W. K\u00fcchlin","year":"1985","unstructured":"K\u00fcchlin, W.: A confluence criterion based on the generalised Newman lemma. Proc. Eurocal 1985, LNCS 204, 1985, 390\u2013399.","journal-title":"LNCS"},{"key":"6_CR19","unstructured":"K\u00fcchlin, W.: Equational completion by proof transformation. Ph.D. thesis, Dep't. of Mathematics, ETH Z\u00fcrich, 1986."},{"key":"6_CR20","unstructured":"Orejas, F.: Theorem Proving in Conditional-Equational Theories. This volume."},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Winkler, F. and Buchberger, B.: A criterion for eliminating unnecessary reductions in the Knuth-Bendix algorithm. Coll. on Algebra, Combinatorics and Logic in Comp. Sci., Gy\u00f6r, 1983.","DOI":"10.1145\/1089338.1089341"},{"key":"6_CR22","unstructured":"Remy, J.L. and Zhang, H.: REVEUR 4: A system for validating conditional algebraic specifications of abstract data types. Proc. 6th ECAI, Pisa 1984, 563\u2013572."},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Zhang, H. and Remy, J.L.: Contextual rewriting. Conf. on Rewriting Techniques and Applications, Dijon 1985, LNCS 202.","DOI":"10.1007\/3-540-15976-2_2"}],"container-title":["Lecture Notes in Computer Science","Conditional Term Rewriting Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-19242-5_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:16:52Z","timestamp":1605644212000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-19242-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540192428","9783540391661"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-19242-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}