{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:50:48Z","timestamp":1725663048357},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540167617"},{"type":"electronic","value":"9783540398592"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16761-7_60","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T13:51:03Z","timestamp":1330177863000},"page":"105-115","source":"Crossref","is-referenced-by-count":28,"title":["A Strong restriction of the inductive completion procedure"],"prefix":"10.1007","author":[{"given":"L.","family":"Fribourg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"12_CR1","first-page":"329","volume":"9","author":"R. Aubin","year":"1979","unstructured":"Aubin R., \"Mechanizing Structural induction\", T.C.S. 9, 1979, pp 329\u2013345 and 347\u2013362.","journal-title":"T.C.S."},{"unstructured":"Boyer R., Moore J.S., A computational logic, Academic press, 1979.","key":"12_CR2"},{"key":"12_CR3","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/comjnl\/12.1.41","volume":"12","author":"R.M. Burstall","year":"1969","unstructured":"Burstall R.M., \"Proving properties of program by structural induction\", Comput. J 12, 1969, pp 41\u201348.","journal-title":"Comput. J"},{"unstructured":"Fay M., \"First-Order Unification in an Equational Theory\", Proc. 4th Workshop on Automated Deduction, Austin, 1979, pp 161\u2013167.","key":"12_CR4"},{"unstructured":"Fribourg L., \"Refutation par Superposition de Clauses Equationnelles\", These de 3eme cycle, U. Paris 7, Sept. 1982.","key":"12_CR5"},{"doi-asserted-by":"crossref","unstructured":"Fribourg L., \"A Narrowing Procedure for Theories with Constructors\", 7th Conf. on Automated Deduction, May 1984, pp 259\u2013281.","key":"12_CR6","DOI":"10.1007\/978-0-387-34768-4_16"},{"doi-asserted-by":"crossref","unstructured":"Goguen J.A., \"How to Prove Algebraic Inductive Hypotheses Without Induction, with Applications to the Correctness of Data Type Implementation\", 5th Conf. on Automated Deduction, Les Arcs, July 1980, pp 356\u2013373.","key":"12_CR7","DOI":"10.1007\/3-540-10009-1_27"},{"doi-asserted-by":"crossref","unstructured":"Hullot J.M., \"Canonical Form and Unification\", 5th Conf. on Automated Deduction, Les Arcs, July 1980, pp 318\u2013334.","key":"12_CR8","DOI":"10.21236\/ADA087640"},{"doi-asserted-by":"crossref","unstructured":"Huet G., Hullot J.M., \"Proofs by induction in equational theories with constructors\", 21st FOCS, 1980, pp 96\u2013107","key":"12_CR9","DOI":"10.1109\/SFCS.1980.37"},{"doi-asserted-by":"crossref","unstructured":"Huet G., Oppen D., \"Equations and Rewrite Rules: A Survey\", Formal Languages Perspective and Open Problems, Ed. Book R, Academic Press, 1980, pp 349\u2013406","key":"12_CR10","DOI":"10.1016\/B978-0-12-115350-2.50017-8"},{"doi-asserted-by":"crossref","unstructured":"Huet G., \"A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm\", T.R. 25, INRIA, July 1980 (also in JCSS 23:1, Aug. 1981, pp 11\u201321).","key":"12_CR11","DOI":"10.1016\/0022-0000(81)90002-7"},{"issue":"4","key":"12_CR12","doi-asserted-by":"crossref","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 27:4, Oct. 1980, pp 797\u2013821.","journal-title":"J.ACM"},{"doi-asserted-by":"crossref","unstructured":"Jouannaud J.P., Kirchner H., \"Completion of a Set of Rules Modulo a Set of Equations\", Proc 11th POPL, Salt Lake City, Jan. 1984.","key":"12_CR13","DOI":"10.1145\/800017.800519"},{"key":"12_CR14","first-page":"49","volume":"27","author":"J.P. Jouannaud","year":"1985","unstructured":"Jouannaud J.P., Kounalis E., \"Proofs by Induction in Equational Theories Without Constructors\", Bulletin of EATCS 27, Oct. 1985, pp 49\u201355.","journal-title":"Bulletin of EATCS"},{"key":"12_CR15","first-page":"175","volume":"33","author":"S. Kaplan","year":"1984","unstructured":"Kaplan S., \"Conditional Rewrite Rules\", T.C.S. 33, Dec.1984, pp 175\u2013193.","journal-title":"T.C.S."},{"doi-asserted-by":"crossref","unstructured":"Kaplan S., \"Fair Conditional Term Rewriting Systems: Unification, Termination and Confluence\", TR no 194, LRI, Orsay, Nov.1984.","key":"12_CR16","DOI":"10.1007\/978-3-662-09691-8_11"},{"doi-asserted-by":"crossref","unstructured":"Knuth D., Bendix P., \"Simple Word Problems in Universal Algebras\", Computational Problems in Abstract Algebras, Pergamon Press, 1970, pp 263\u2013297.","key":"12_CR17","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"unstructured":"Kamin S., Levy J.-J., \"Two Generalisations of the Recursive Path Ordering\", Unpublished Note, Dept of Computer Science, U. Illinois, Feb. 1980.","key":"12_CR18"},{"unstructured":"Lankford D, \"Canonical Inference\", Report ATP-32, U. of Texas, 1975.","key":"12_CR19"},{"unstructured":"Manna Z., Ness N., \"On the Termination of Markov Algorithms\", Proc. 3rd Hawaii Intl. Conf. on Systems and Science, Jan. 1970, pp. 789\u2013792.","key":"12_CR20"},{"doi-asserted-by":"crossref","unstructured":"Musser D.L., \"On Proving Inductive Properties of Abstract Data Types\", Proc. 7th POPL, Las Vegas, 1980, pp 154\u2013162.","key":"12_CR21","DOI":"10.1145\/567446.567461"},{"key":"12_CR22","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. Peterson","year":"1981","unstructured":"Peterson G., Stickel M.E., \"Complete Sets of Reductions for Some Equational Theories\", J.ACM 28, 1981, pp 233\u2013264.","journal-title":"J.ACM"},{"key":"12_CR23","volume-title":"Etude des Systemes de Reecriture Conditionnels et Application aux Types Abstraits Algebriques","author":"J.L. Remy","year":"1982","unstructured":"Remy J.L. \"Etude des Systemes de Reecriture Conditionnels et Application aux Types Abstraits Algebriques\", These d'Etat, Nancy, 1982."},{"unstructured":"Remy J.L., Zhang H., \"REVEUR4: A System for Validating Conditional Algebraic Specifications of Abstract Data Types\", Proc. ECAI, Pisa, 1984, pp 563\u2013572.","key":"12_CR24"},{"issue":"4","key":"12_CR25","doi-asserted-by":"crossref","first-page":"622","DOI":"10.1145\/321850.321859","volume":"21","author":"J.R. Slagle","year":"1974","unstructured":"Slagle J.R., \"Automated Theorem Proving for Theories with Simplifiers, Commutativity and Associativity\", J.ACM 21:4, Oct 1974, pp 622\u2013642.","journal-title":"J.ACM"},{"unstructured":"Smith D.R., \"Reasoning by Cases and the Formation of Conditional Programs\", Intl. Joint Conf. on Artificial Intelligence, Los Angeles., Aug. 1985, pp. 215\u2013218.","key":"12_CR26"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16761-7_60.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:10:51Z","timestamp":1605625851000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16761-7_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540167617","9783540398592"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-16761-7_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1986]]}}}