{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:12:23Z","timestamp":1725664343197},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540592006"},{"type":"electronic","value":"9783540492238"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59200-8_69","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:06:14Z","timestamp":1330257974000},"page":"352-366","source":"Crossref","is-referenced-by-count":7,"title":["Combination of constraint solving techniques: An algebraic point of view"],"prefix":"10.1007","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":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1006\/jsco.1993.1066","volume":"16","author":"A. Boudet","year":"1993","unstructured":"A. Boudet. Combining unification algorithms. J. Symbolic Computation, 16:597\u2013626, 1993.","journal-title":"J. Symbolic Computation"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"F. Baader and K.U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Proceedings of CADE-11, LNCS 607, 1992.","DOI":"10.1007\/3-540-55602-8_155"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"F. Baader and K.U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures, 1993. Extended version, submitted for publication.","DOI":"10.1007\/3-540-55602-8_155"},{"key":"28_CR4","doi-asserted-by":"crossref","unstructured":"F. Baader and K.U. Schulz. Combination techniques and decision problems for disunification. In Proceedings of RTA-93, LNCS 690, 1993.","DOI":"10.1007\/3-540-56868-9_23"},{"key":"28_CR5","unstructured":"F. Baader and K.U. Schulz. Combination of Constraint Solving Techniques: An Algebraic Point of View. Research Report CIS-Rep-94-75, CIS, University Munich, 1994. This report is available via anonymous ftp from \u201ccantor.informatik.rwth-aachen.de\u201d in the directory \u201cpub\/papers.\u201d"},{"key":"28_CR6","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert. A Resolution Principle for a Logic with Restricted Quantifiers, LNCS 568, 1991.","DOI":"10.1007\/3-540-55034-8"},{"key":"28_CR7","volume-title":"Universal Algebra","author":"P.M. Cohn","year":"1965","unstructured":"P.M. Cohn. Universal Algebra. Harper & Row, New York, 1965."},{"key":"28_CR8","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"H. Comon and P. Lescanne. Equational problems and disunification. J. Symbolic Computation, 7:371\u2013425, 1989.","journal-title":"J. Symbolic Computation"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"H. Comon and R. Treinen. Ordering constraints on trees. In Colloquium on Trees in Algebra and Programming (CAAP), LNCS, 1994.","DOI":"10.1007\/BFb0017470"},{"key":"28_CR10","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of rewriting. J. Symbolic Computation, 3:69\u2013116, 1987.","journal-title":"J. Symbolic Computation"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"E. Domenjoud, F. Klay, and Ch. Ringeissen. Combination techniques for non-disjoint theories. In Proceedings of CADE-12, LNCS 814, 1994.","DOI":"10.1007\/3-540-58156-1_19"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"C. Kirchner and H. Kirchner. Constrained equational reasoning. In Proceedings of SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation. ACM Press, 1989.","DOI":"10.1145\/74540.74585"},{"issue":"2","key":"28_CR13","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1006\/jsco.1994.1040","volume":"18","author":"H. Kirchner","year":"1994","unstructured":"H. Kirchner and Ch. Ringeissen. Combining symbolic constraint solvers on algebraic domains. J. Symbolic Computation, 18(2):113\u2013155, 1994.","journal-title":"J. Symbolic Computation"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"M.J. Maher. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Proceedings of LICS'88, IEEE Computer Society, 1988.","DOI":"10.1109\/LICS.1988.5132"},{"key":"28_CR15","volume-title":"volume 66 of Studies in Logic and the Foundation of Mathematics","author":"A.I. Mal'cev","year":"1971","unstructured":"A.I. Mal'cev. The Metamathematics of Algebraic Systems, volume 66 of Studies in Logic and the Foundation of Mathematics. North Holland, Amsterdam, London, 1971."},{"key":"28_CR16","volume-title":"volume 192 of Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen","author":"A.I. Mal'cev","year":"1973","unstructured":"A.I. Mal'cev. Algebraic Systems, volume 192 of Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen. Springer, Berlin, 1973."},{"issue":"2","key":"28_CR17","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D.C. Oppen. Simplification by cooperating decision procedures. ACM TOPLAS, 1(2):245\u2013257, 1979.","journal-title":"ACM TOPLAS"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Ch. Ringeissen. Unification in a combination of equational theories with shared constants and its application to primal algebras. In Proceedings of LPAR'92, LNCS 624, 1992.","DOI":"10.1007\/BFb0013067"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"R. Nieuwenhuis and A. Rubio, \u201cAC-superposition with constraints: No ACunifiers needed,\u201d in: Proceedings CADE-12, Springer LNAI 814, 1994.","DOI":"10.1007\/3-540-58156-1_40"},{"issue":"1","key":"28_CR20","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M. Schmidt-Schau\u00df","year":"1989","unstructured":"M. Schmidt-Schau\u00df. Unification in a combination of arbitrary disjoint equational theories. J. Symbolic Computation, 8(1,2):51\u201399, 1989.","journal-title":"J. Symbolic Computation"},{"key":"28_CR21","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF01196548","volume":"30","author":"N. Weaver","year":"1993","unstructured":"N. Weaver. Generalized varieties. Algebra Universalis, 30:27\u201352, 1993.","journal-title":"Algebra Universalis"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59200-8_69.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T14:50:45Z","timestamp":1687272645000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59200-8_69"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540592006","9783540492238"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-59200-8_69","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}