{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:57:49Z","timestamp":1725663469571},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540510819"},{"type":"electronic","value":"9783540461494"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/3-540-51081-8_100","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T15:38:39Z","timestamp":1330184319000},"page":"59-75","source":"Crossref","is-referenced-by-count":12,"title":["Computing ground reducibility and inductively complete positions"],"prefix":"10.1007","author":[{"given":"Reinhard","family":"B\u00fcndgen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"issue":"1","key":"6_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0747-7171(88)80018-X","volume":"6","author":"L. Bachmair","year":"1988","unstructured":"Leo Bachmair and Nachum Dershowitz. Critical pair criteria for completion. Journ. Symbolic Computation, 6(1):1\u201318, August 1988.","journal-title":"Journ. Symbolic Computation"},{"key":"6_CR2","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1979","unstructured":"Robert S. Boyer and J Strother Moore. A Computational Logic. Academic Press, Orlando, Florida, 1979."},{"key":"6_CR3","volume-title":"Design, implementation, and application of an extended ground-reducibility test","author":"R. B\u00fcndgen","year":"1987","unstructured":"Reinhard B\u00fcndgen. Design, implementation, and application of an extended ground-reducibility test. Master's thesis, Computer and Information Sciences, University of Delaware, Newark, DE 19716, 1987."},{"key":"6_CR4","series-title":"Technical Report","volume-title":"Design, implementation, and application of an extended ground-reducibility test","author":"R. B\u00fcndgen","year":"1987","unstructured":"Reinhard B\u00fcndgen. Design, implementation, and application of an extended ground-reducibility test. Technical Report 88-05, Computer and Information Sciences, University of Delaware, Newark, DE 19716, December 1987."},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"B. F. Caviness, editor. Eurocal'85, volume 204 of LNCS. Springer-Verlag, 1985. (European Conference on Computer Algebra, Linz, Austria, April 1985).","DOI":"10.1007\/3-540-15984-3"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Laurent Fribourg. A strong restriction of the inductive completion procedure. In Proc. 13th ICALP, volume 226 of LNCS, Rennes, France, 1986. Springer-Verlag. (To appear in J. Symbolic Computation.).","DOI":"10.1007\/3-540-16761-7_60"},{"key":"6_CR7","volume-title":"Logic for Computer Science","author":"J. H. Gallier","year":"1986","unstructured":"Jean H. Gallier. Logic for Computer Science. Harper & Row, New York, 1986."},{"key":"6_CR8","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"G\u00e9rard Huet and Jean-Marie Hullot. Proofs by induction in equational theories with constructors. J. Computer and System Sciences, 25:239\u2013266, 1982.","journal-title":"J. Computer and System Sciences"},{"key":"6_CR9","unstructured":"G\u00e9rard Huet and Derek C. Oppen. Equations and rewrite rules: A survey. In Ron Book, editor, Formal Languages: Perspectives and Open Problems, pages 349\u2013405. Academic Press, 1980."},{"key":"6_CR10","series-title":"Rapport de Recherche","volume-title":"Proofs by induction in equational theories without constructors","author":"J. Jouannaud","year":"1986","unstructured":"Jean-Pierre Jouannaud and Emmanuel Kounalis. Proofs by induction in equational theories without constructors. Rapport de Recherche 295, Laboratoire de Recherche en Informatique, Universit\u00e9 Paris 11, Orsay, France, September 1986. (To appear in Information and Computation, 1989.)."},{"issue":"2","key":"6_CR11","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"Deepak Kapur and David R. Musser. Proof by consistency. Artificial Intelligence, 31(2):125\u2013157, February 1987.","journal-title":"Artificial Intelligence"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Deepak Kapur, Paliath Narendran, and Hantao Zhang. Proof by induction using test sets. In J\u00f6rg H. Siekmann, editor, 8th International Conference on Automated Deduction, volume 230 of LNCS, pages 99\u2013117. Springer-Verlag, 1986.","DOI":"10.1007\/3-540-16780-3_83"},{"issue":"4","key":"6_CR13","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/BF00292110","volume":"24","author":"D. Kapur","year":"1987","unstructured":"Deepak Kapur, Paliath Narendran, and Hantao Zhang. On sufficient-completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395\u2013415, 1987.","journal-title":"Acta Informatica"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Emmanuel Kounalis. Completeness in data type specifications. In Caviness [Cav85], pages 348\u2013362.","DOI":"10.1007\/3-540-15984-3_291"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Wolfgang K\u00fcchlin. A confluence criterion based on the generalised Knuth-Bendix algorithm. In Caviness [Cav85], pages 390\u2013399.","DOI":"10.1007\/3-540-15984-3_294"},{"key":"6_CR16","volume-title":"Equational Completion by Proof Transformation","author":"W. K\u00fcchlin","year":"1986","unstructured":"Wolfgang K\u00fcchlin. Equational Completion by Proof Transformation. PhD thesis, Swiss Federal Institute of Technology (ETH), CH-8092 Z\u00fcrich, Switzerland, June 1986."},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Wolfgang K\u00fcchlin. Inductive completion by ground proof transformation. In H. A\u00eft-Kaci and M. Nivat, editors, Rewriting Techniques, volume 2 of Resolution of Equations in Algebraic Structures, chapter 7. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046371-8.50013-4"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow and G. Weikum. A decidability result about sufficient completeness of axiomatically specified abstract data types. In Sixth GI Conference on Theoretical Computer Science, volume 145 of LNCS, pages 257\u2013268, 1982.","DOI":"10.1007\/BFb0036486"},{"key":"6_CR19","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. Plaisted","year":"1985","unstructured":"David Plaisted. Semantic confluence and completion methods. Information and Control, 65:182\u2013215, 1985.","journal-title":"Information and Control"},{"key":"6_CR20","unstructured":"Jean-Jacques Thiel. Stop loosing sleep over incomplete data type specifications. In Proc. 11th PoPL, Salt Lake City, Utah, 1984. ACM."},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Hantao Zhang, Deepak Kapur, and Mukkai S. Krishnamoorthy. A mechanizable induction principle for equational specifications. In E. Lusk and R. Overbeek, editors, 9th International Conference on Automated Deduction, volume 310 of LNCS, pages 162\u2013181. Springer-Verlag, 1988.","DOI":"10.1007\/BFb0012831"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-51081-8_100.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:19:23Z","timestamp":1605629963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-51081-8_100"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540510819","9783540461494"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-51081-8_100","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]}}}