{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:55:30Z","timestamp":1725663330240},"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_70","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:30:03Z","timestamp":1330183803000},"page":"180-190","source":"Crossref","is-referenced-by-count":7,"title":["Proving inductive theorems based on term rewriting systems"],"prefix":"10.1007","author":[{"given":"Dieter","family":"Hofbauer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf-Detlef","family":"Kutsche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"18_CR1","unstructured":"B\u00fcchi, J.R., Mahr, B. and Siefkes, D. Manual on REC \u2014 a language for use and cost analysis of recursion over arbitrary data structures, Techn. Report 84-06, TU Berlin, FB 20 (1984)."},{"key":"18_CR2","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, 13th ICALP,Lecture Notes in Comp. Sci., Vol.226 (1986), pp.105\u201315.","journal-title":"13th ICALP,Lecture Notes in Comp. Sci."},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-10009-1_27","volume":"87","author":"J. Goguen","year":"1980","unstructured":"Goguen, J. How to prove algebraic inductive hypotheses without induction, with applications to the correctness of data type implementation, Lecture Notes in Comput. Sci., Vol.87, Springer-Verlag (1980), pp.356\u201373.","journal-title":"Lecture Notes in Comput. Sci."},{"key":"18_CR4","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, J.ACM, Vol.27 (1980), pp.797\u2013821.","journal-title":"J.ACM"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"Huet, G. and Hullot, J.M. Proofs by induction in equational theories with constructors, J. Comp. and Syst. Sci., Vol.25 (1982), pp.239\u201366.","journal-title":"J. Comp. and Syst. Sci."},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Hofbauer, D. and Kutsche, R.-D. Proving inductive theorems based on term rewriting systems, Techn. Report 88-12, TU Berlin (1988).","DOI":"10.1007\/3-540-50667-5_70"},{"key":"18_CR7","unstructured":"Jouannaud, J.P. and Kounalis, E. Automatic proofs by induction in theories without constructors, CNRS Rapport de Recherche No.295 (1986). Preliminary version in Proc. 1st LICS (1986)."},{"key":"18_CR8","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"Kapur, D. and Musser, D.R. Proof by consistency, Artificial Intelligence, 31 (1987), pp.125\u2013157.","journal-title":"Artificial Intelligence"},{"key":"18_CR9","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P. and Zhang, H. On sufficient-completeness and related properties of term rewriting systems, Acta Informatica, Vol.24 (1987), pp.395\u2013415.","journal-title":"Acta Informatica"},{"key":"18_CR10","first-page":"279","volume":"33","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Narendran, P., Rosenkrantz, D. and Zhang, H. Sufficient-completeness, quasireducibility, and their complexity, Bull. of the EATCS 33 (1987), pp.279\u201381.","journal-title":"Bull. of the EATCS"},{"key":"18_CR11","first-page":"282","volume":"170","author":"H. Kirchner","year":"1985","unstructured":"Kirchner, H., A general inductive completion algorithm and application to abstract data types, Lecture Notes in Comp. Sci., Vol.170, Springer Verlag (1985), pp.282\u2013302.","journal-title":"Lecture Notes in Comp. Sci."},{"key":"18_CR12","series-title":"Techn. Report","volume-title":"Inductive completion by ground proof transformation","author":"W. K\u00fcchlin","year":"1987","unstructured":"K\u00fcchlin, W. Inductive completion by ground proof transformation, Techn. Report No. 87-08, Comp. and Inform. Sci., Univ. of Delaware, Newark, DE 19716 (1987)."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Musser, D.R. On proving inductive properties of abstract data types, Proc. 7th ACM Symp. on Principles of prog. languages (1980), pp.154\u201362.","DOI":"10.1145\/567446.567461"},{"key":"18_CR14","unstructured":"Padawitz, P. Foundations of specification & programming with Horn clauses, Habilitations-schrift, Universit\u00e4t Passau (1987), to appear as EATCS monograph."},{"key":"18_CR15","unstructured":"Paul, E. Proof by induction in equational theories with relations between constructors, 9th Coll. on trees in algebra and programming, Ed. Courcelle,B., Cambridge Univ. Press (1984), pp.211\u201325."},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/3-540-16780-3_84","volume":"230","author":"Y. Toyama","year":"1986","unstructured":"Toyama, Y. How to prove equivalence of term rewriting systems without induction, Lecture Notes in Comp. Sci., Vol.230, Springer Verlag (1986), pp.118\u201327.","journal-title":"Lecture Notes in Comp. Sci."}],"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_70","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,24]],"date-time":"2019-06-24T06:08:13Z","timestamp":1561356493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-50667-5_70"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540506676","9783540460633"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-50667-5_70","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1988]]}}}