{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,23]],"date-time":"2026-04-23T11:14:52Z","timestamp":1776942892831,"version":"3.51.4"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[1991,4,1]],"date-time":"1991-04-01T00:00:00Z","timestamp":670464000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1991,4]]},"DOI":"10.1007\/bf01893885","type":"journal-article","created":{"date-parts":[[2005,7,31]],"date-time":"2005-07-31T13:33:08Z","timestamp":1122816788000},"page":"311-350","source":"Crossref","is-referenced-by-count":45,"title":["Sufficient-completeness, ground-reducibility and their complexity"],"prefix":"10.1007","volume":"28","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[]},{"given":"Daniel J.","family":"Rosenkrantz","sequence":"additional","affiliation":[]},{"given":"Hantao","family":"Zhang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"BF01893885_CR1","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1145\/322290.322301","volume":"29","author":"R. Book","year":"1982","unstructured":"Book, R.: Confluent and other types of Thue systems. J. Assoc. Comput. Mach.29, 171\u2013182 (1982)","journal-title":"J. Assoc. Comput. Mach."},{"key":"BF01893885_CR2","volume-title":"A computational logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A computational logic. New York: Academic Press 1979"},{"key":"BF01893885_CR3","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/3-540-16780-3_85","volume-title":"Sufficient-completeness, term rewriting systems, and \u201canti-unification\u201d","author":"H. Comon","year":"1986","unstructured":"Comon, H.: Sufficient-completeness, term rewriting systems, and \u201canti-unification\u201d. Proc. of 8th Intl. Conf. on Automated Deduction (Lect. Notes Comput. Sci., Vol. 230, pp. 128\u2013140). Berlin Heidelberg New York: Springer 1986"},{"key":"BF01893885_CR4","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1145\/321623.321625","volume":"18","author":"S.A. Cook","year":"1971","unstructured":"Cook, S.A.: Characterizations of pushdown machines in terms of time-bounded computers. J. Assoc. Comput. Mach.18, 4\u201318 (1971)","journal-title":"J. Assoc. Comput. Mach."},{"key":"BF01893885_CR5","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1016\/S0019-9958(85)80003-6","volume":"65","author":"N. Dershowitz","year":"1985","unstructured":"Dershowitz, N.: Computing with rewrite systems. Inf. Control65, 122\u2013157 (1985)","journal-title":"Inf. Control"},{"key":"BF01893885_CR6","unstructured":"Garey, M.R., Johnson, D.S.: Computers and intractability. W.H. Freeman 1979"},{"key":"BF01893885_CR7","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1007\/3-540-10009-1_27","volume-title":"How to prove algebraic inductive hypotheses without induction","author":"J. Goguen","year":"1980","unstructured":"Goguen, J.: How to prove algebraic inductive hypotheses without induction. Proc. of the 5th Conference on Automated Deduction, Les Arcs, France. (Lect. Notes Comput. Sci., Vol. 87, pp. 356\u2013373) Berlin Heidelberg New York: Springer 1980"},{"key":"BF01893885_CR8","unstructured":"Guttag, J.: The specification and application to programming of abstract data types. Department of Computer Science, Univ. of Toronto, Ph.D. Thesis, CSRG-59 (1975)"},{"key":"BF01893885_CR9","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"J. Guttag","year":"1978","unstructured":"Guttag, J., Horning, J.J.: The algebraic specification of abstract data types. Acta Inf.10, 27\u201352 (1978)","journal-title":"Acta Inf."},{"key":"BF01893885_CR10","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","volume":"25","author":"G. Huet","year":"1982","unstructured":"Huet, G., Hullot, J.M.: Proofs by induction in equational theories with constructors. J. Comput. Syst. Sci.25, 239\u2013266 (1982)","journal-title":"J. Comput. Syst. Sci."},{"key":"BF01893885_CR11","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1016\/B978-0-12-115350-2.50017-8","volume-title":"Formal language theory: Perspectives and open problems","author":"G. Huet","year":"1980","unstructured":"Huet, G., Oppen, D.C.: Equations and rewrite rules: A survey. In: R. Book (ed.) Formal language theory: Perspectives and open problems, pp. 349\u2013405. New York: Academic Press 1980"},{"key":"BF01893885_CR12","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1016\/0022-0000(84)90021-7","volume":"28","author":"H.B. Hunt","year":"1984","unstructured":"Hunt, H.B., Rosenkrantz, D.J.: The complexity of monadic recursion schemes: Exponential time bounds. J. Comput. Syst. Sci.28, 395\u2013419 (1984)","journal-title":"J. Comput. Syst. Sci."},{"key":"BF01893885_CR13","unstructured":"Jouannaud, J.-P., Kounalis, E.: Automatic proofs by induction in equational theories without constructors. Proc. of the IEEE Symposium on Logic in Computer Science, Cambridge, Mass, pp. 358\u2013386, 1986"},{"key":"BF01893885_CR14","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0004-3702(87)90017-8","volume":"31","author":"D. Kapur","year":"1987","unstructured":"Kapur, D., Musser, D.R.: Proof by consistency. Artif. Intell. J.31, 125\u2013157 (1987)","journal-title":"Artif. Intell. J."},{"key":"BF01893885_CR15","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/3-540-16780-3_83","volume-title":"Proof by induction using test sets","author":"D. Kapur","year":"1986","unstructured":"Kapur, D., Narendran, P., Zhang, H.: Proof by induction using test sets. Proc. of 8th Intl. Conf. on Automated Deduction, Oxford England (Lect. Notes Comput. Sci., Vol. 230, pp. 99\u2013117) Berlin Heidelberg New York: Springer 1986a"},{"key":"BF01893885_CR16","doi-asserted-by":"crossref","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 Inf.24, 395\u2013416 (1987)","journal-title":"Acta Inf."},{"key":"BF01893885_CR17","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"426","DOI":"10.1007\/3-540-17179-7_26","volume-title":"Complexity of sufficient-completeness","author":"D. Kapur","year":"1986","unstructured":"Kapur, D., Narendran, P., Zhang, H.: Complexity of sufficient-completeness. Proc. of 6th Conf. on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India (Lect. Notes Comput. Sci., Vol. 241, pp. 426\u2013442) Berlin Heidelberg New York: Springer 1986b"},{"key":"BF01893885_CR18","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/B978-0-08-012975-4.50028-X","volume-title":"Computational problems in abstract algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: J. Leech (ed.). Computational problems in abstract algebra, pp. 263\u2013297. Oxford: Pergamon Press (1970)"},{"key":"BF01893885_CR19","first-page":"348","volume-title":"Completeness in data type specifications","author":"E. Kounalis","year":"1985","unstructured":"Kounalis, E.: Completeness in data type specifications. Proc. EUROCAL'85, LNCS 204 (Bob F. Caviness, ed.), pp. 348\u2013362. Berlin Heidelberg New York: Springer 1985"},{"key":"BF01893885_CR20","series-title":"Technical Report ATP-39","volume-title":"Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions","author":"D.S. Lankford","year":"1977","unstructured":"Lankford, D.S., Ballantyne, A.M.: Decision procedures for simple equational theories with commutative-associative axioms: Complete sets of commutative-associative reductions. Technical Report ATP-39, Dept. of Math. and Computer Science, Univ. of Texas at Austin, Texas, 1977"},{"key":"BF01893885_CR21","series-title":"Memo MTP-14","volume-title":"A simple explanation of inductionless induction","author":"D.S. Lankford","year":"1981","unstructured":"Lankford, D.S.: A simple explanation of inductionless induction. Memo MTP-14, Dept. of Mathematics, Louisiana Tech. University, Ruston, Louisiana, 1981"},{"key":"BF01893885_CR22","first-page":"301","volume":"3","author":"J.-L. Lassez","year":"1987","unstructured":"Lassez, J.-L., Marriott, K.: Explicit representation of terms defined by counter-examples. J Automat. Reasoning3, 301\u2013318 (1987)","journal-title":"J Automat. Reasoning"},{"key":"BF01893885_CR23","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H. Lewis","year":"1980","unstructured":"Lewis, H.: Complexity results for classes of quantificational formulas. J. Comput. System Sci.21, 317\u2013353 (1980)","journal-title":"J. Comput. System Sci."},{"key":"BF01893885_CR24","volume-title":"A note on the complexity of determining the reasonability and the existence of an explicit representation for an implicit generalization","author":"K. Marriott","year":"1988","unstructured":"Marriott, K.: A note on the complexity of determining the reasonability and the existence of an explicit representation for an implicit generalization. Draft manuscript. Computer Science Dept. University of Melbourne, Australia, 1988"},{"key":"BF01893885_CR25","doi-asserted-by":"crossref","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"M.L. Minsky","year":"1961","unstructured":"Minsky, M.L.: Recursive unsolvability of Post's problem of \u201cTag\u201d and other topics in theory of Turing machines. Ann. Math.74, 437\u2013455 (1961)","journal-title":"Ann. Math."},{"key":"BF01893885_CR26","doi-asserted-by":"crossref","unstructured":"Musser, D.R.: On proving inductive properties of abstract data types. Proc. 7th Principles of Programming Languages, Las Vegas, Nevada 1980","DOI":"10.1145\/567446.567461"},{"key":"BF01893885_CR27","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1007\/BFb0036486","volume-title":"A decidability result about sufficient-completeness of axiomatically specified abstract data types","author":"T. Nipkow","year":"1982","unstructured":"Nipkow, T., Weikum, G.: A decidability result about sufficient-completeness of axiomatically specified abstract data types. Proc. of the 6th GI Conf. on Theoretical Computer Science, (Lect. Notes Comput. Sci., Vol. 145, pp. 257\u2013268) Berlin Heidelberg New York: Springer 1982"},{"key":"BF01893885_CR28","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L., Stickel, M.E.: Complete set of reductions for some equational theoris. J. Assoc. Comput. Mach.28, 233\u2013264 (1981)","journal-title":"J. Assoc. Comput. Mach."},{"key":"BF01893885_CR29","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1016\/0022-0000(84)90010-2","volume":"29","author":"D. Plaisted","year":"1984","unstructured":"Plaisted, D.: Complete problems in the first-order predicate calculalus. J. Comput. System Sci.29, 8\u201335 (1984)","journal-title":"J. Comput. System Sci."},{"key":"BF01893885_CR30","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1016\/S0019-9958(85)80005-X","volume":"65","author":"D. Plaisted","year":"1985","unstructured":"Plaisted, D.: Semantic confluence tests and completion methods. Inf. Control65, 182\u2013215 (1985)","journal-title":"Inf. Control"},{"key":"BF01893885_CR31","doi-asserted-by":"crossref","unstructured":"Thiel, J.J.: Stop loosing sleep over incomplete data type specifications. Proc. of Eleventh Annual ACM Symposium on Principles of Programming Languages, Salt Lake City, Utah 1984","DOI":"10.1145\/800017.800518"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01893885.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01893885\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01893885","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T13:44:10Z","timestamp":1586353450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01893885"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,4]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1991,4]]}},"alternative-id":["BF01893885"],"URL":"https:\/\/doi.org\/10.1007\/bf01893885","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1991,4]]}}}