{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T02:37:02Z","timestamp":1768271822380,"version":"3.49.0"},"reference-count":63,"publisher":"Elsevier BV","issue":"2-3","license":[{"start":{"date-parts":[[1990,5,1]],"date-time":"1990-05-01T00:00:00Z","timestamp":641520000000},"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":8478,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1990,5]]},"DOI":"10.1016\/0304-3975(90)90034-f","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:47:37Z","timestamp":1027655257000},"page":"169-202","source":"Crossref","is-referenced-by-count":19,"title":["Equational completion in order-sorted algebras"],"prefix":"10.1016","volume":"72","author":[{"given":"Isabelle","family":"Gnaedig","sequence":"first","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]},{"given":"H\u00e9l\u00e9ne","family":"Kirchner","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(90)90034-F_BIB1","series-title":"PhD thesis","article-title":"Proof methods for equational theories","author":"Bachmair","year":"1988"},{"key":"10.1016\/0304-3975(90)90034-F_BIB2","series-title":"Proc. 2nd Conf. on Rewriting Techniques and Applications","article-title":"Completion for rewriting module a congruence","author":"Bachmair","year":"1987"},{"key":"10.1016\/0304-3975(90)90034-F_BIB3","first-page":"346","article-title":"Orderings for equational proofs","author":"Bachmair","year":"1986","journal-title":"Proc. Symp. Logic in Computer Science"},{"key":"10.1016\/0304-3975(90)90034-F_BIB4","doi-asserted-by":"crossref","first-page":"136","DOI":"10.1145\/800087.802799","article-title":"Hope: an experimental applicative language","author":"Burstall","year":"1980","journal-title":"Conf. Record of the 1980 LISP Conference"},{"key":"10.1016\/0304-3975(90)90034-F_BIB5","series-title":"Technical Report","article-title":"Rewrite systems on a lattice of types","author":"Cunningham","year":"1983"},{"key":"10.1016\/0304-3975(90)90034-F_BIB6","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term-rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoret. Comput. Sci."},{"issue":"1, 2","key":"10.1016\/0304-3975(90)90034-F_BIB7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","article-title":"Termination of rewriting","volume":"3","author":"Dershowitz","year":"1987","journal-title":"J. Symbolic Comput."},{"issue":"8","key":"10.1016\/0304-3975(90)90034-F_BIB8","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1145\/359138.359142","article-title":"Proving termination with multiset orderings","volume":"22","author":"Dershowitz","year":"1979","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(90)90034-F_BIB9","series-title":"Machine Intelligence 11: The Logic and Acquisition of Knowledge","first-page":"21","article-title":"Equational programming","author":"Dershowitz","year":"1988"},{"key":"10.1016\/0304-3975(90)90034-F_BIB10","series-title":"Proc. EUROCAL Conf.","article-title":"ERIL equational reasoning: an interactive laboratory","author":"Dick","year":"1985"},{"key":"10.1016\/0304-3975(90)90034-F_BIB11","series-title":"Proc. 12th ACM Symp. on Principles of Programming Languages","first-page":"52","article-title":"Principles of OBJ-2","author":"Futatsugi","year":"1985"},{"key":"10.1016\/0304-3975(90)90034-F_BIB12","series-title":"Proc. Internat. Joint Conf. on Theory and Practice of Software Development: Colloquium on Software Engineering","article-title":"Order-sorted completion: the many-sorted way","author":"Ganzinger","year":"1989"},{"key":"10.1016\/0304-3975(90)90034-F_BIB13","series-title":"Proc. 13th Colloquium on Trees in Algebra and Programming","first-page":"165","article-title":"Equational completion in order-sorted algebras","author":"Gnaedig","year":"1988"},{"key":"10.1016\/0304-3975(90)90034-F_BIB14","series-title":"Internet Bericht FB-169","article-title":"Algebraic specifications with partially ordered sorts and declarations","author":"Gogolla","year":"1983"},{"key":"10.1016\/0304-3975(90)90034-F_BIB15","article-title":"Order sorted algebras: exceptions and error sorts, coercions and overloaded operators","volume":"14","author":"Goguen","year":"1978"},{"key":"10.1016\/0304-3975(90)90034-F_BIB16","series-title":"Proc. 1st Internat. Workshop on Conditional Term Rewriting Systems","article-title":"An introduction to OBJ-3","author":"Goguen","year":"1988"},{"key":"10.1016\/0304-3975(90)90034-F_BIB17","series-title":"Technical Report","article-title":"Order-sorted algebra I: partial and overloaded operations, errors and inheritance","author":"Goguen","year":"1983"},{"key":"10.1016\/0304-3975(90)90034-F_BIB18","series-title":"Proc. 2nd Symp. on Logic in Computer Science","first-page":"18","article-title":"Order-sorted algebra solves the constructor-selector, multiple representation and coercion problem","author":"Goguen","year":"1987"},{"key":"10.1016\/0304-3975(90)90034-F_BIB19","first-page":"163","article-title":"Programming with parameterized abstract objects in OBJ","author":"Goguen","year":"1982","journal-title":"Theory Practice Software Technol."},{"key":"10.1016\/0304-3975(90)90034-F_BIB20","series-title":"Proc. 12th Internat. Colloquium on Automata, Languages and Programming","first-page":"221","article-title":"Operational semantics for order-sorted algebra","author":"Goguen","year":"1985"},{"key":"10.1016\/0304-3975(90)90034-F_BIB21","series-title":"Technical Report CSLI-84-15","article-title":"Completeness of many-sorted equational logic","author":"Goguen","year":"1984"},{"key":"10.1016\/0304-3975(90)90034-F_BIB22","series-title":"Proc. Internat. Joint Conf. on Theory and Practice of Software Development","first-page":"1","article-title":"Models and equality for logical programming","author":"Goguen","year":"1987"},{"issue":"30","key":"10.1016\/0304-3975(90)90034-F_BIB23","first-page":"66","article-title":"Remarks on remarks on many-sorted equational logic","volume":"1","author":"Goguen","year":"1986","journal-title":"EATCS Bull."},{"issue":"1","key":"10.1016\/0304-3975(90)90034-F_BIB24","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1145\/357153.357158","article-title":"Programming with equations","volume":"4","author":"Hoffman","year":"1982","journal-title":"Trans. Programming Languages Systems"},{"key":"10.1016\/0304-3975(90)90034-F_BIB25","series-title":"Proc. 10th Internat. Colloquium on Automata, Languages and Programming","first-page":"331","article-title":"Rewrite methods for clausal and non-clausal theorem proving","author":"Hsiang","year":"1983"},{"key":"10.1016\/0304-3975(90)90034-F_BIB26","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","article-title":"A complete proof of corectness of the Knuth and Bendix completion algorithm","volume":"23","author":"Huet","year":"1981","journal-title":"J. Comput. System Sci."},{"issue":"4","key":"10.1016\/0304-3975(90)90034-F_BIB27","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","article-title":"Confluent reductions: abstract properties and applications to term rewriting systems","volume":"27","author":"Huet","year":"1980","journal-title":"J. ACM"},{"issue":"2","key":"10.1016\/0304-3975(90)90034-F_BIB28","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/0022-0000(82)90006-X","article-title":"Proofs by induction in equational theories with constructors","volume":"25","author":"Huet","year":"1982","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/0304-3975(90)90034-F_BIB29","series-title":"Formal Language Theory: Perspectives and Open Problems","first-page":"349","article-title":"Equations and rewrite rules: a survey","author":"Huet","year":"1980"},{"key":"10.1016\/0304-3975(90)90034-F_BIB30","article-title":"Congruence closure in order-sorted algebra","author":"Isakowitz","year":"1988","journal-title":"Technical report"},{"key":"10.1016\/0304-3975(90)90034-F_BIB31","series-title":"Proc. Logic Programming Conf.","article-title":"Rewriting in order-sorted equational logic","author":"Isakowitz","year":"1988"},{"key":"10.1016\/0304-3975(90)90034-F_BIB32","series-title":"Proc. 8th Colloquium on Trees in Algebra and Programming","article-title":"Confluent and coherent equational term rewriting systems","author":"Jouannaud","year":"1983"},{"key":"10.1016\/0304-3975(90)90034-F_BIB33","article-title":"Proof algebras","author":"Jouannaud","year":"1987","journal-title":"Rewriting Techniques and Applications Conference"},{"issue":"4","key":"10.1016\/0304-3975(90)90034-F_BIB34","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","article-title":"Completion of a set of rules modulo a set of equations","volume":"15","author":"Jouannaud","year":"1986","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0304-3975(90)90034-F_BIB35","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0020-0190(82)90107-7","article-title":"On multiset orderings","volume":"10","author":"Jouannaud","year":"1982","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/0304-3975(90)90034-F_BIB36","series-title":"Proc. 7th Conf. on Automated Deduction","article-title":"Termination of a set of rules modulo a set of equations","author":"Jouannaud","year":"1984"},{"key":"10.1016\/0304-3975(90)90034-F_BIB37","first-page":"206","article-title":"Computing unification algorithms","author":"Kirchner","year":"1986","journal-title":"Proc. 1st Symp. on Logic in Computer Science"},{"key":"10.1016\/0304-3975(90)90034-F_BIB38","article-title":"M\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationnelles","volume":"1","author":"Kirchner","year":"1985","journal-title":"Th\u00e9se d'\u00e9tat de l'Universite de Nancy"},{"key":"10.1016\/0304-3975(90)90034-F_BIB39","article-title":"Methods and tools for equational unification","author":"Kirchner","year":"1987","journal-title":"Proc. Colloquium on Resolution of Equations in Algebraic Structures"},{"key":"10.1016\/0304-3975(90)90034-F_BIB40","article-title":"Order-sorted equational unification","author":"Kirchner","year":"1988","journal-title":"Rapport de Recherche INRIA 954, Dec. 88"},{"issue":"8","key":"10.1016\/0304-3975(90)90034-F_BIB41","article-title":"Reveur-3: implementation of a general completion procedure parametrized by built-in theories and strategies","volume":"20","author":"Kirchner","year":"1986","journal-title":"Sci. Comput. Programming"},{"key":"10.1016\/0304-3975(90)90034-F_BIB42","series-title":"Technical Report 87-R-87","article-title":"Operational semantics of OBJ-3","author":"Kirchner","year":"1987"},{"key":"10.1016\/0304-3975(90)90034-F_BIB43","series-title":"Proc. 15th Internat. Colloquium on Automata, Languages and Programming","first-page":"287","article-title":"Operational semantics of OBJ-3","author":"Kirchner","year":"1988"},{"key":"10.1016\/0304-3975(90)90034-F_BIB44","series-title":"Proc. 7th Internat. Conf. on Automated Deduction","first-page":"282","article-title":"A general inductive completion algorithm and application to abstract data types","author":"Kirchner","year":"1984"},{"key":"10.1016\/0304-3975(90)90034-F_BIB45","article-title":"Preuves par compl\u00e9tion dans les vari\u00e9t\u00e9s d'alg\u00e9bres","volume":"1","author":"Kirchner","year":"1985","journal-title":"Th\u00e9se d'\u00e9tat de l'Universit\u00e9 de Nancy"},{"key":"10.1016\/0304-3975(90)90034-F_BIB46","series-title":"Computational Problems in Abstract Algebras","first-page":"263","article-title":"Simple word problems in universal algebra","author":"Knuth","year":"1970"},{"key":"10.1016\/0304-3975(90)90034-F_BIB47","series-title":"Technical Report","article-title":"Decision procedures for simple equational theories with associative commutative axioms: complete sets of associative commutative reductions","author":"Lankford","year":"1977"},{"key":"10.1016\/0304-3975(90)90034-F_BIB48","series-title":"Technical Report","article-title":"Decision procedures for simple equational theories with commutative axioms: complete sets of commutative reductions","author":"Lankford","year":"1977"},{"key":"10.1016\/0304-3975(90)90034-F_BIB49","series-title":"Technical Report","article-title":"Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions","author":"Lankford","year":"1977"},{"key":"10.1016\/0304-3975(90)90034-F_BIB50","series-title":"Proc. 10th ACM Symp. on Principles of Programming Languages","first-page":"99","article-title":"Computer experiments with the REVE term rewriting systems generator","author":"Lescanne","year":"1983"},{"key":"10.1016\/0304-3975(90)90034-F_BIB51","series-title":"Technical Report 89-R-58","article-title":"A logic of semi-functions, inclusion and equality. The setting","author":"Megrelis","year":"1989"},{"key":"10.1016\/0304-3975(90)90034-F_BIB52","series-title":"Algebraic Methods in Semantics","article-title":"Initiality, induction and computability","author":"Meseguer","year":"1985"},{"key":"10.1016\/0304-3975(90)90034-F_BIB53","article-title":"Order sorted unification","author":"Meseguer","year":"1987","journal-title":"Proc. Colloquium on Resolution of Equations in Algebraic Structures"},{"key":"10.1016\/0304-3975(90)90034-F_BIB54","doi-asserted-by":"crossref","first-page":"223","DOI":"10.2307\/1968867","article-title":"On theories with a combinatorial definition of Equivalence","author":"Newman","year":"1942","journal-title":"Ann. Math."},{"key":"10.1016\/0304-3975(90)90034-F_BIB55","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF01396685","article-title":"Untersuchungen zur mehrsortigen Quantorenlogik","volume":"145","author":"Oberschelp","year":"1962","journal-title":"Math. Ann."},{"key":"10.1016\/0304-3975(90)90034-F_BIB56","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1145\/322248.322251","article-title":"Complete sets of reductions for some equational theories","volume":"28","author":"Peterson","year":"1981","journal-title":"J. ACM"},{"key":"10.1016\/0304-3975(90)90034-F_BIB57","series-title":"Technical Report","article-title":"Parameterisation for order-sorted algebraic specifications","author":"Poign\u00e9","year":"1986"},{"key":"10.1016\/0304-3975(90)90034-F_BIB58","series-title":"Proc. 8th Conf. on Automated Deduction","article-title":"Unification in many sorted equational theories","author":"Schmidt-Schauss","year":"1986"},{"key":"10.1016\/0304-3975(90)90034-F_BIB59","series-title":"Technical Report seki-SR-86-17","article-title":"Order-sorted Horn logic semantics and deduction","author":"Smolka","year":"1986"},{"key":"10.1016\/0304-3975(90)90034-F_BIB60","article-title":"Order sorted equational computation","author":"Smolka","year":"1987","journal-title":"Proc. Colloquium on Resolution of Equations in Algebraic Structures"},{"key":"10.1016\/0304-3975(90)90034-F_BIB61","series-title":"Proc. 1st Internat Workshop on Conditional Term Rewriting Systems","first-page":"228","article-title":"Confluent term rewriting systems with membership conditions","author":"Toyama","year":"1987"},{"key":"10.1016\/0304-3975(90)90034-F_BIB62","series-title":"Proc. 2nd Conf. on Functional Programming Languages and Computer Architecture","first-page":"1","article-title":"MIRANDA: a non-strict functional language with polymorphic types","author":"Turner","year":"1985"},{"key":"10.1016\/0304-3975(90)90034-F_BIB63","series-title":"Technical Report 297","article-title":"Semantics of order-sorted specifications","author":"Waldmann","year":"1989"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759090034F?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759090034F?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T03:51:26Z","timestamp":1555127486000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759090034F"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990,5]]},"references-count":63,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[1990,5]]}},"alternative-id":["030439759090034F"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(90)90034-f","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1990,5]]}}}