{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,6]],"date-time":"2023-02-06T20:31:32Z","timestamp":1675715492383},"reference-count":45,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1998,2,1]],"date-time":"1998-02-01T00:00:00Z","timestamp":886291200000},"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":5645,"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":[[1998,2]]},"DOI":"10.1016\/s0304-3975(97)00147-3","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T01:04:53Z","timestamp":1027645493000},"page":"107-161","source":"Crossref","is-referenced-by-count":20,"title":["Combination of constraint solvers for free and quasi-free structures"],"prefix":"10.1016","volume":"192","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus U.","family":"Schulz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(97)00147-3_BIB1","article-title":"Non-well-founded sets","author":"Aczel","year":"1988"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB2","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0304-3975(94)90209-7","article-title":"A feature-based constraint system for logic programming with entailment","volume":"122","author":"Ait-Kaci","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(97)00147-3_BIB3_1","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1006\/jsco.1996.0009","article-title":"Unification in the union of disjoint equational theories: combining decision procedures","volume":"21","author":"Baader","year":"1996","journal-title":"J. Symbol. Comput."},{"key":"10.1016\/S0304-3975(97)00147-3_BIB3_2","article-title":"Proc. CADE'92","volume":"vol. 607","author":"Baader","year":"1992"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB4","series-title":"Proc. RTA-93","first-page":"301","article-title":"Combination techniques and decision problems for disunification","volume":"vol. 690","author":"Baader","year":"1993"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB5_1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-59200-8_69","article-title":"Combination of constraint solving techniques: an algebraic point of view","author":"Baader","year":"1994"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB5_2","series-title":"Proc. RTA-95","first-page":"352","volume":"vol. 914","author":"Baader","year":"1995"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB6","series-title":"Proc. CP'95","first-page":"380","article-title":"On the combination of symbolic constraints, solution domains, and constraint solvers","volume":"vol. 976","author":"Baader","year":"1995"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB7","article-title":"On the combination of symbolic constraints, solution domains, and constraint solvers, extended version of [6]","author":"Baader","year":"1995"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB8","series-title":"Constraints in Computational Logics, Proc. CCL-94","first-page":"320","article-title":"How to win a game with features","volume":"vol. 845","author":"Backofen","year":"1994"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB9","article-title":"\u00c4quivalenzbeweis zweier Definitionen zur Kombination freier Strukturen","author":"Khalifa","year":"1996"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB10","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1006\/jsco.1993.1066","article-title":"Combining unification algorithms","volume":"16","author":"Boudet","year":"1993","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/S0304-3975(97)00147-3_BIB11","article-title":"A resolution principle for a logic with restricted quantifiers","volume":"vol. 568","author":"B\u00fcrckert","year":"1991"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB12","article-title":"Model theoretic algebra: selected topics","volume":"vol. 521","author":"Cherlin","year":"1976"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB13","series-title":"Universal Algebra","author":"Cohn","year":"1965"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB14","series-title":"Proc. 2nd Internat. Conf. on Fifth Generation Computer Systems","first-page":"85","article-title":"Equations and inequations on finite and infinite trees","author":"Colmerauer","year":"1984"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB15","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/79204.79210","article-title":"An introduction to PROLOG III","volume":"33","author":"Colmerauer","year":"1990","journal-title":"Comm. ACM"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB16","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","article-title":"Equational problems and disunification","volume":"7","author":"Comon","year":"1989","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/S0304-3975(97)00147-3_BIB17","series-title":"Colloquium on Trees in Algebra and Programming (CAAP)","first-page":"1","article-title":"Ordering constraints on trees","volume":"vol. 787","author":"Comon","year":"1994"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB18","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."},{"key":"10.1016\/S0304-3975(97)00147-3_BIB19","series-title":"Logic Programming: Proc. 8th Internat. Conf., The MIT Press","article-title":"{log}: A logic programming language with finite sets","author":"Dovier","year":"1991"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB20","series-title":"Proc. Internat. Logic Programming Symp.","first-page":"540","article-title":"Embedding extensional finite sets in CLP","author":"Dovier","year":"1993"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB21","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1017\/S0960129500000177","article-title":"Universal domains and the amalgamation property","volume":"3","author":"Droste","year":"1993","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/S0304-3975(97)00147-3_BIB22","series-title":"Proc. 7th Internat. Conf. on Automated Deduction","first-page":"194","article-title":"Associative-commutative unification","volume":"vol. 170","author":"Fages","year":"1984"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB23","series-title":"Proc. 14th ACM Symp. on Principles of Programming Languages","first-page":"111","article-title":"Constraint logic programming","author":"Jaffar","year":"1987"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB24","series-title":"Proc. CP-96","first-page":"282","article-title":"Combination of constraint solvers II: rational amalgamation","volume":"vol. 1118","author":"Kepser","year":"1996"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB25","series-title":"Proc. SIGSAM 1989 Internat. Symp. on Symbolic and Algebraic Computation, ACM Press","article-title":"Constrained equational reasoning","author":"Kirchner","year":"1989"},{"issue":"2","key":"10.1016\/S0304-3975(97)00147-3_BIB26","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1006\/jsco.1994.1040","article-title":"Combining symbolic constraint solvers on algebraic domains","volume":"18","author":"Kirchner","year":"1994","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/S0304-3975(97)00147-3_BIB27","series-title":"Proc. 3rd Annual Symp. on Logic in Computer Science, LICS'88","first-page":"348","article-title":"Complete axiomatizations of the algebras of finite, rational and infinite trees","author":"Maher","year":"1988"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB28","article-title":"The metamathematics of Algebraic Systems","volume":"vol. 66","author":"Mal'cev","year":"1971"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB29","article-title":"Algebraic Systems","volume":"vol. 192","author":"Mal'cev","year":"1973"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB30","first-page":"189","article-title":"Universal algebra","volume":"vol. 1","author":"Meinke","year":"1992"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB31","article-title":"Constraint logic programming and the unification of information","author":"Mukai","year":"1991"},{"issue":"2","key":"10.1016\/S0304-3975(97)00147-3_BIB32","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","article-title":"Simplification by cooperating decision procedures","volume":"1","author":"Nelson","year":"1979","journal-title":"ACM TOPLAS"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB33","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","article-title":"Complexity, convexity and combination of theories","volume":"12","author":"Oppen","year":"1980","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(97)00147-3_BIB34","series-title":"Proc. LPAR'92","article-title":"Unification in a combination of equational theories with shared constants and its application to primal algebras","volume":"vol. 624","author":"Ringeissen","year":"1992"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB35","article-title":"Set values for unification based grammar formalisms and logic programming","author":"Rounds","year":"1988","journal-title":"Research Report CSLI-88\u2013129"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB36","article-title":"Unification algebras: an axiomatic approach to unification, equation solving and constraint solving","author":"Schmidt-Schau\u00df","year":"1988"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB37","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","article-title":"Unification in a combination of arbitrary disjoint equational theories","volume":"8","author":"Schmidt-Schau\u00df","year":"1989","journal-title":"J. Symbolic Comput."},{"issue":"3","key":"10.1016\/S0304-3975(97)00147-3_BIB38","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0743-1066(94)90044-2","article-title":"Records for logic programming","volume":"18","author":"Smolka","year":"1994","journal-title":"J. Logic Programming"},{"issue":"2","key":"10.1016\/S0304-3975(97)00147-3_BIB39","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","article-title":"A practical decision procedure for arithmetic with function symbols","volume":"26","author":"Shostak","year":"1979","journal-title":"J. ACM"},{"issue":"3","key":"10.1016\/S0304-3975(97)00147-3_BIB40","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1145\/322261.322262","article-title":"A unification algorithm for associative commutative functions","volume":"28","author":"Stickel","year":"1981","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB41","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1070\/SM1983v044n01ABEH000954","article-title":"Decidability of the positive theory of a free countably generated semigroup","volume":"44","author":"Vazhenin","year":"1983","journal-title":"Math. USSR Sbornik"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB42","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/BF01196548","article-title":"Generalized varieties","volume":"30","author":"Weaver","year":"1993","journal-title":"Algebra Universalis"},{"key":"10.1016\/S0304-3975(97)00147-3_BIB43","article-title":"Instantiation Theory: on the foundation of automated deduction","volume":"vol. 518","author":"Williams","year":"1991"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597001473?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597001473?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T04:50:05Z","timestamp":1555390205000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397597001473"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,2]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1998,2]]}},"alternative-id":["S0304397597001473"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(97)00147-3","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1998,2]]}}}