{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:55:32Z","timestamp":1725663332317},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540506676"},{"type":"electronic","value":"9783540460633"}],"license":[{"start":{"date-parts":[[1988,1,1]],"date-time":"1988-01-01T00:00:00Z","timestamp":567993600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/3-540-50667-5_72","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:30:10Z","timestamp":1330183810000},"page":"204-213","source":"Crossref","is-referenced-by-count":5,"title":["A new quasi-reducibility testing algorithm and its application to proofs by induction"],"prefix":"10.1007","author":[{"given":"G. A.","family":"Kucherov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"20_CR1","unstructured":"Boyer, R., Moore, J.S.: A computational logic. Academic Press 1979."},{"key":"20_CR2","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/3-540-16780-3_85","volume":"230","author":"C. H","year":"1986","unstructured":"Comon, H.: Sufficient completeness, term rewriting systems and \u201canti-unification\u201d. Lect. Notes Comput. Sci. 230, 1986, 128\u2013140.","journal-title":"Lect. Notes Comput. Sci."},{"key":"20_CR3","first-page":"323","volume-title":"Hilberts tenth problem: positive aspects of a negative solution. Mathematical Development Arising from Hilbert Problems","author":"M. Davis","year":"1976","unstructured":"Davis. M., Matijasevic. Y., Robinson, J.: Hilberts tenth problem: positive aspects of a negative solution. Mathematical Development Arising from Hilbert Problems. American Math. Society, Providence, RI, 1976, 323\u2013378."},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-16761-7_60","volume":"226","author":"L. Fribourg","year":"1986","unstructured":"Fribourg, L.: A strong restriction of the inductive completion procedure. Lect. Notes Comput. Sci. 226, 1986, 105\u2013115.","journal-title":"Lect. Notes Comput. Sci."},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-10009-1_27","volume":"87","author":"J.A. Goguen","year":"1980","unstructured":"Goguen, J.A.: How to prove algebraic inductive hypothesis without induction. with application to the correctness of data type implementation. Lect. Notes Comput. Sci. 87, 1980, 356\u2013373.","journal-title":"Lect. Notes Comput. Sci."},{"issue":"4","key":"20_CR6","doi-asserted-by":"publisher","first-page":"797","DOI":"10.1145\/322217.322230","volume":"27","author":"G. Huet","year":"1980","unstructured":"Huet, G.: Confluent reductions: abstract properties and applications to term rewriting systems. Journ. ACM 27 (1980) No.4, 797\u2013821.","journal-title":"Journ. ACM"},{"issue":"2","key":"20_CR7","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"H. G","year":"1982","unstructured":"Huet, G., Hullot, J.-M.: Proofs by induction in equational theories with constructors. Journ. Comput. System Sci. 25 (1982) No.2, 239\u2013266.","journal-title":"Journ. Comput. System Sci."},{"key":"20_CR8","unstructured":"Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in equational theories without constructors. Proc. Symp. Logic in Comput. Sci., Cambridge, Mass., June 16\u201318, 1986, 358\u2013366."},{"key":"20_CR9","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P., Zhang, H.: On sufficient-completeness and related properties of term rewriting systems. Acta Informatica 24 (1987) Fasc. 4, 395\u2013415.","journal-title":"Acta Informatica"},{"key":"20_CR10","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-15984-3_291","volume":"204","author":"E. Kounalis","year":"1985","unstructured":"Kounalis, E.: Completeness in data type specifications. Lect. Notes Comput. Sci. 204, 1985, 348\u2013362.","journal-title":"Lect. Notes Comput. Sci."},{"key":"20_CR11","first-page":"19","volume":"122","author":"G.A. Kucherov","year":"1987","unstructured":"Kucherov, G.A.: A quasi-reducibility testing algorithm for linear term rewriting systems. Computer systems 122. Novosibirsk 1987. 19\u201337. (in Russian)","journal-title":"Computer systems"},{"key":"20_CR12","unstructured":"Lazrek, A., Lescanne, P., Thiel, J.-J.: Proving inductive equalities algorithms and implementation. INRIA, Rapports de Recherche, No.682, Juin 1987."},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Musser, D.: On proving inductive properties of abstract data types. Proc. 7th ACM Symp. on Princ. Progr. Lang., 1980, Las Vegas, 154\u2013162.","DOI":"10.1145\/567446.567461"},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/BFb0036486","volume":"145","author":"T. Nipkow","year":"1982","unstructured":"Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types, Lect. Notes Comput. Sci. 145, 1982, 257\u2013267.","journal-title":"Lect. Notes Comput. Sci."},{"issue":"2","key":"20_CR15","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D.A. Plaisted","year":"1985","unstructured":"Plaisted, D.A.: Semantic confluence tests and completion methods. Inf. and Cont. 65 (1985) 2, 182\u2013215.","journal-title":"Inf. and Cont."},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Thiel, J.J.: Stop losing sleep over incomplete data type specifications. Proc. 11th ACM Symp. on Princ. Prog. Lang., 1984, Salt-Lake-City, 76\u201382.","DOI":"10.1145\/800017.800518"}],"container-title":["Lecture Notes in Computer Science","Algebraic and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-50667-5_72","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,21]],"date-time":"2019-01-21T05:56:47Z","timestamp":1548050207000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50667-5_72"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540506676","9783540460633"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-50667-5_72","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}