{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,13]],"date-time":"2025-09-13T15:51:01Z","timestamp":1757778661099},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540127277"},{"type":"electronic","value":"9783540387145"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1983]]},"DOI":"10.1007\/3-540-12727-5_16","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T12:54:49Z","timestamp":1330174489000},"page":"269-283","source":"Crossref","is-referenced-by-count":19,"title":["Confluent and coherent equational term rewriting systems application to proofs in abstract data types"],"prefix":"10.1007","author":[{"given":"Jean-Pierre","family":"Jouannaud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"DERSHOWITZ N.: \u201cOrderings for term-rewriting systems\u201d Proc 20th FOCS, pp 123\u2013131 (1979) and TCS 17-3 (1982)","DOI":"10.1016\/0304-3975(82)90026-3"},{"key":"16_CR2","unstructured":"DERSHOWITZ N.: \u201cComputing with term rewriting systems\u201d to be published"},{"key":"16_CR3","unstructured":"FAY M.: \u201cFirst order unification in an equational theory\u201d Proc. 4th CADE, Austin Texas (19\/9)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"GOGUEN J.A.: \u201cHow to prove algebraic inductive hypotheses without induction, with application to the correctness of data type implementation\u201d Proc. 5th CADE, les Arcs (1980)","DOI":"10.1007\/3-540-10009-1_27"},{"key":"16_CR5","unstructured":"HSIANG J. DERSHOWITZ N.: \u201cUsing rewrites methods for clausal and non clausal theorem proving\u201d Proc. 10th ICALP (1983)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"HUET G. HULLOT J.M.: \u201cProofs by induction in equational theories with constructors\u201d Proc. 21th FOCS (1980) and JCSS 25-2 (1982)","DOI":"10.1016\/0022-0000(82)90006-X"},{"key":"16_CR7","unstructured":"HSIANG J. PLAISTED D.A.: \u201cA deductive program generation system\u201d to be published"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"HUET G.: \u201cConfluent reductions: abstract properties and applications to term rewriting systems\u201d Proc. 18th. FOCS (19\/\/) and JACM 2\/\u20134 pp \/9\/\u2013821 (1980)","DOI":"10.1145\/322217.322230"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"HUET G.: \u201cA complete proof of correctness of the Knuth and Bendix completion algorithm\u201d JCSS 23, pp 11\u201321 (1981)","DOI":"10.1016\/0022-0000(81)90002-7"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"HULLOT J.M.: \u201cCanonical forms and unification\u201d Proc. 5th CADE, Les Arcs (1980)","DOI":"10.21236\/ADA087640"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"JEANROND H.J.: \u201cDeciding unique termination of permutative rewriting systems: choose your term algebra carefully\u201d Proc. 5th CADE, Les Arcs (1980)","DOI":"10.1007\/3-540-10009-1_26"},{"key":"16_CR12","unstructured":"JOUANNAUD J.P. KIRCHNER C. KIRCHNER H.: \u201cIncremental construction of unification algorithms in equationnal theories\u201d Proc. 10th ICALP, Barcelonna (1983)."},{"key":"16_CR13","unstructured":"JOUANNAUD J.P. KIRCHNER H. REMY J.L.: \u201cChurh-Rosser properties of equational term rewriting systems: new results\u201d to be published."},{"key":"16_CR14","unstructured":"JOUANNAUD J.P. LESCANNE P. REINIG F.: \u201cRecursive decomposition ordering\u201d in \u201cFormal description of programming concepts 2\u201d Ed. BJORNER D., North Holland (1982)"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"KNUTH D. BEND IX P.: \u201cSimple word problems in universal algebras\u201d in \u201cComputational problems in abstract algebra\u201d Leech J. ed. Pergamon Press, pp 263\u2013297 (1970)","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"16_CR16","unstructured":"KAMIN S. LEVY J.J.: \u201cAttempts for generalizing the recursive path ordering\u201d unpublished notes (1980)"},{"key":"16_CR17","unstructured":"LANKFORD D.S.: \u201cA simple explanation of inductionless induction\u201d Louisiana Tech. University, Math. Dept. Rep MTP-14 (1981)"},{"key":"16_CR18","unstructured":"LANKFORD D.S. BALLANTYNE A.M.: \u201cDecision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions\u201d Rep. ATP-3\/, Dpt. of Comp. Sc., Univ. of Texas at Austin"},{"key":"16_CR19","unstructured":"LANKFORD D.S. BALLANTYNE A.M.: \u201cDecision procedures for simple equational theories with commutative-associative axioms: complete sets of commutative-associative reductions\u201d Rep. ATP-39, Dpt. of Comp. Sc., Univ. of Texas at Austin"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"LESCANNE P.: \u201cComputer experiments with the REVE term rewriting system generator\u201d Proc. 10th POPL conference (1983)","DOI":"10.1145\/567067.567078"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"MUSSER D.R.: \u201cOn proving inductive properties of abstract data types\u201d Proc. 7th POPL Conference, Las Vegas (1980)","DOI":"10.1145\/567446.567461"},{"key":"16_CR22","unstructured":"PADAWITZ P.: \u201cEquational data type specification and recursive program scheme\u201d in \u201cFormal Description of Programming Concepts 2\u201d Ed. BJORNER D., North Holland (1982)"},{"issue":"2","key":"16_CR23","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G. E. Peterson","year":"1981","unstructured":"PETERSON G.E. STICKEL M.E.: \u201cComplete sets of reductions for equational theories with complete unification algorithms\u201d J.ACM 28, no.2, pp 233\u2013264 (1981)","journal-title":"J.ACM"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"STICKEL M.E.: \u201cA unification algorithm for associative-commutative functions\u201d J.ACM 28-3, pp 423\u2013434 (1981)","DOI":"10.1145\/322261.322262"}],"container-title":["Lecture Notes in Computer Science","CAAP'83"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-12727-5_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T15:06:11Z","timestamp":1605625571000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-12727-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1983]]},"ISBN":["9783540127277","9783540387145"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-12727-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1983]]}}}