{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T10:40:46Z","timestamp":1776854446844,"version":"3.51.2"},"reference-count":46,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1989,7,1]],"date-time":"1989-07-01T00:00:00Z","timestamp":615254400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":8782,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[1989,7]]},"DOI":"10.1016\/0890-5401(89)90062-x","type":"journal-article","created":{"date-parts":[[2004,12,2]],"date-time":"2004-12-02T00:24:20Z","timestamp":1101947060000},"page":"1-33","source":"Crossref","is-referenced-by-count":81,"title":["Automatic proofs by induction in theories without constructors"],"prefix":"10.1016","volume":"82","author":[{"given":"Jean-Pierre","family":"Jouannaud","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emmanuel","family":"Kounalis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0890-5401(89)90062-X_BIB1","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","article-title":"Process algebra for synchronous communication","volume":"60","author":"Bergstra","year":"1984","journal-title":"Inform. and Control"},{"key":"10.1016\/0890-5401(89)90062-X_BIB2","author":"Boyer-Moore","year":"1979"},{"key":"10.1016\/0890-5401(89)90062-X_BIB3","series-title":"Proceedings, 8th CADE","article-title":"Sufficient completeness, term rewriting systems and \u201cAnti-Unification\u201d","author":"Common","year":"1986"},{"key":"10.1016\/0890-5401(89)90062-X_BIB4","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1016\/S0019-9958(85)80003-6","article-title":"Computing with term rewriting systems","volume":"65","author":"Dershowitz","year":"1985","journal-title":"Inform. and Control"},{"key":"10.1016\/0890-5401(89)90062-X_BIB5","series-title":"Proceedings 1st RTA","article-title":"Termination","volume":"Vol. 222","author":"Dershowitz","year":"1985"},{"key":"10.1016\/0890-5401(89)90062-X_BIB6","series-title":"Proceedings S\u00e9minaire d'Informatique Th\u00e9orique","article-title":"Applications of the Knuth-Bendix completion procedure","author":"Dershowitz","year":"1982"},{"key":"10.1016\/0890-5401(89)90062-X_BIB7","series-title":"Proceedings 14th ICALP","article-title":"A strong restriction of the inductive completion procedure","author":"Fribourg","year":"1986"},{"key":"10.1016\/0890-5401(89)90062-X_BIB8","series-title":"Proceedings, 13th POPL","article-title":"Principles of OBJ2","author":"Futatsugi","year":"1985"},{"key":"10.1016\/0890-5401(89)90062-X_BIB9","series-title":"A first Introduction to PLUSS","author":"Gaudel","year":"1984"},{"key":"10.1016\/0890-5401(89)90062-X_BIB10","series-title":"Proceedings 5th CADE","article-title":"How to prove algebraic inductive hypothesis without induction, with application to the correctness of data types implementation","author":"Goguen","year":"1980"},{"key":"10.1016\/0890-5401(89)90062-X_BIB11","series-title":"Proceedings 13th ICALP","article-title":"Operational semantics for order-sorted algebras","author":"Goguen","year":"1985"},{"key":"10.1016\/0890-5401(89)90062-X_BIB12","series-title":"Application of Algebra to Language Definition and Compilation","article-title":"Initiality, induction and computability","author":"Goguen","year":"1983"},{"key":"10.1016\/0890-5401(89)90062-X_BIB13","series-title":"Proceedings 14th ICALP","article-title":"On word problems in equational theories","author":"Hsiang","year":"1987"},{"key":"10.1016\/0890-5401(89)90062-X_BIB14","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","article-title":"A complete proof of the Knuth-Bendix completion procedure","volume":"23","author":"Huet","year":"1981","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/0890-5401(89)90062-X_BIB15","series-title":"Proceedings 23th FOCS","first-page":"239","article-title":"Proofs by induction in equational theories with constructors","volume":"25","author":"Huet","year":"1980"},{"key":"10.1016\/0890-5401(89)90062-X_BIB16","series-title":"Formal Languages: Perspectives and Open Problems","article-title":"Equations and rewrite rules: A survey","author":"Huet","year":"1980"},{"key":"10.1016\/0890-5401(89)90062-X_BIB17","series-title":"Proceedings, 12th POPL","first-page":"1155","article-title":"Completion of a set of rules modulo a set of equations","volume":"15","author":"Jouannaud","year":"1984"},{"key":"10.1016\/0890-5401(89)90062-X_BIB18","series-title":"Proceedings 1st IEEE Symposium on Logic in Computer Science","article-title":"Automatic proofs by induction in equational theories without constructors","author":"Jouannaud","year":"1986"},{"key":"10.1016\/0890-5401(89)90062-X_BIB19","series-title":"Proceedings 3rd IFIP Conference on Formalization of Programming Concepts","article-title":"Reductive conditional term rewriting systems","author":"Jouannaud","year":"1986"},{"key":"10.1016\/0890-5401(89)90062-X_BIB20","doi-asserted-by":"crossref","unstructured":"Kaplan, S. Symplifying conditional term rewriting systems: Unification termination and confluence, J. Symb. Comput. 4, 295\u2013334.","DOI":"10.1016\/S0747-7171(87)80010-X"},{"key":"10.1016\/0890-5401(89)90062-X_BIB21","author":"Kapur","year":"1986","journal-title":"On Sufficient Completeness and Related Properties of Term Rewriting Systems"},{"key":"10.1016\/0890-5401(89)90062-X_BIB22","series-title":"Proceedings 7th CADE","article-title":"A new equational unification method","volume":"Vol. 180","author":"Kirchener","year":"1984"},{"key":"10.1016\/0890-5401(89)90062-X_BIB23","series-title":"Proceedings, 7th CADE","article-title":"A general inductive algorithm and application to ADTs","volume":"Vol. 180","author":"Kirchner","year":"1984"},{"key":"10.1016\/0890-5401(89)90062-X_BIB24","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/0167-6423(87)90004-9","article-title":"Reveur-3: Implementation of a general completion procedure parametrized by built-in theories and strategies","volume":"8","author":"Kirchner","year":"1987","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0890-5401(89)90062-X_BIB25","series-title":"Computational Problems in Abstract Algebra","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/0890-5401(89)90062-X_BIB26","article-title":"Validation de Sp\u00e9cifications Alg\u00e9briques par Compl\u00e9tion Inductive","author":"Kounalis","year":"1985","journal-title":"Th\u00e8se de l'Universit\u00e9 Nancy 1"},{"key":"10.1016\/0890-5401(89)90062-X_BIB27","unstructured":"Kounalis, E. Completeness in data type specifications, in \u201cProceedings 3rd EUROCAL\u201d, Lect. Notes in Comput. Sci. Vol. 204, Springer-Verlag, New York\/Berlin."},{"key":"10.1016\/0890-5401(89)90062-X_BIB28","series-title":"Proceedings, Hungarian Conference of Computer Science","article-title":"A general completeness check for equational specifications","author":"Kounalis","year":"1985"},{"key":"10.1016\/0890-5401(89)90062-X_BIB29","series-title":"Inductive completion using ground confluence, research report","author":"Kuchlin","year":"1986"},{"key":"10.1016\/0890-5401(89)90062-X_BIB30","author":"Lankford","year":"1981"},{"key":"10.1016\/0890-5401(89)90062-X_BIB31","series-title":"Proceedings 3rd Hawaiian Conference on Systems and Sciences","article-title":"On the termination of Markov algorithms","author":"Manna","year":"1970"},{"key":"10.1016\/0890-5401(89)90062-X_BIB32","series-title":"Proceedings 7th POPL Conference","article-title":"On proving inductive properties of abstract data types","author":"Musser","year":"1980"},{"key":"10.1016\/0890-5401(89)90062-X_BIB33","series-title":"Proceedings, NSF Workshop","article-title":"Proof by consistency","author":"Musser","year":"1984"},{"key":"10.1016\/0890-5401(89)90062-X_BIB34","series-title":"Proceedings, IEEE Symposium on Logic in Computer Science","article-title":"Proofs by induction for incomplete specifications","author":"Musser","year":"1986"},{"key":"10.1016\/0890-5401(89)90062-X_BIB35","series-title":"Proceedings, 12th POPL","article-title":"Implementation of an interpretor of abstract equations","author":"O'Donnell","year":"1984"},{"key":"10.1016\/0890-5401(89)90062-X_BIB36","first-page":"267","article-title":"A decidability Result about axiomatically specified abstract data types","volume":"Vol. 155","author":"Nipkof","year":"1983"},{"key":"10.1016\/0890-5401(89)90062-X_BIB37","series-title":"Proceedings, CAAP","article-title":"Proof by induction in equational theories with relations between constructors","author":"Paul","year":"1984"},{"key":"10.1016\/0890-5401(89)90062-X_BIB38","series-title":"Proceedings, EUROCAL","article-title":"On solving the equality problem in theories defined by Horn clauses","author":"Paul","year":"1985"},{"key":"10.1016\/0890-5401(89)90062-X_BIB39","series-title":"Proceedings, 9th CAAP","article-title":"Proof in the final algebra","author":"Puel","year":"1984"},{"key":"10.1016\/0890-5401(89)90062-X_BIB40","first-page":"256","article-title":"Complete sets of reductions for equational theories with complete unification algorithms","volume":"31","author":"Peterson","year":"1981","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/0890-5401(89)90062-X_BIB41","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1016\/S0019-9958(85)80005-X","article-title":"Semantic confluence tests and completion methods","volume":"65","author":"Plaisted","year":"1985","journal-title":"Inform. and Control"},{"key":"10.1016\/0890-5401(89)90062-X_BIB42","article-title":"Etude des Syst\u00e8mes de R\u00e9\u00e9criture Conditionels et Application aux Types Abstraits Alg\u00e9briques","author":"R\u00e9my","year":"1982","journal-title":"Th\u00e8se de doctorat d'\u00e9tat"},{"key":"10.1016\/0890-5401(89)90062-X_BIB43","series-title":"Proceedings, 1st International Conference on Rewriting Techniques et Applications","article-title":"Contextual rewriting","author":"R\u00e9my","year":"1985"},{"key":"10.1016\/0890-5401(89)90062-X_BIB44","series-title":"Proceedings, 12th POPL","article-title":"Stop losing sleep over uncompleteness of data type specifications","author":"Thiel","year":"1984"},{"key":"10.1016\/0890-5401(89)90062-X_BIB45","series-title":"Proceedings, 8th CADE","article-title":"How to prove equivalence of term rewriting systems without induction","author":"Toyama","year":"1986"},{"key":"10.1016\/0890-5401(89)90062-X_BIB46","author":"Hsiang","year":"1987"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:089054018990062X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:089054018990062X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T12:49:32Z","timestamp":1586004572000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/089054018990062X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,7]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1989,7]]}},"alternative-id":["089054018990062X"],"URL":"https:\/\/doi.org\/10.1016\/0890-5401(89)90062-x","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[1989,7]]}}}