{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:48:44Z","timestamp":1767138524395,"version":"build-2238731810"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540568681","type":"print"},{"value":"9783662215517","type":"electronic"}],"license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/978-3-662-21551-7_23","type":"book-chapter","created":{"date-parts":[[2022,7,19]],"date-time":"2022-07-19T05:30:08Z","timestamp":1658208608000},"page":"301-315","source":"Crossref","is-referenced-by-count":5,"title":["Combination techniques and decision problems for disunification"],"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","reference":[{"key":"23_CR1","doi-asserted-by":"crossref","unstructured":"F. Baader, K.U. Schulz, \u201cUnification in the Union of Disjoint Equational Theories: Combining Decision Procedures,\u201d DFKI-Research Report RR-91-33; also in Proceedings of the 11th International Conference on Automated Deduction, LNCS 607, 1992.","DOI":"10.1007\/3-540-55602-8_155"},{"key":"23_CR2","unstructured":"F. Baader, K.U. Schulz, \u201cGeneral A-and AX-Unification via Optimized Combination Procedures,\u201d CIS-Report 92-58, CIS, University Munich; also to appear in the Proceedings of the Second Workshop on Word Equations and Related Topics IWWERT '91, Rouen 1991, LNCS."},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"F. Baader, K.U. Schulz, \u201cCombination Techniques and Decision Problems for Disunification,\u201d DFKI-Research Report RR-93-05, 1993.","DOI":"10.1007\/3-540-56868-9_23"},{"issue":"1","key":"23_CR4","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/BF02017493","volume":"26","author":"J. Richard B\u00fcchi","year":"1987","unstructured":"J.R. B\u00fcchi, S. Senger, \u201cCoding in the Existential Theory of Concatenation,\u201d Arch. math. Logik 26, 1986.","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"},{"key":"23_CR5","unstructured":"H.J. B\u00fcrckert, \u201cSolving Disequations in Equational Theories,\u201d Proceedings of the 9th International Conference on Automated Deduction, Argonne, LNCS 310, 1988."},{"key":"23_CR6","unstructured":"R. Buntine, H.-J. B\u00fcrckert, \u201cOn Solving Equations and Disequations,\u201d SEKI-Report SR-89-03, University Kaiserslautern, 1989."},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"H.-J. B\u00fcrckert, \u201cA Resolution Principle for Clauses with Constraints,\u201d Proceedings of the 10th International Conference on Automated Deduction, LNCS 449, 1990.","DOI":"10.1007\/3-540-52885-7_87"},{"key":"23_CR8","unstructured":"A. Colmerauer, \u201cEquations and Inequations on Finite and Infinite Trees,\u201d Proceedings of the FGCS'84, pp.85\u201399."},{"issue":"7","key":"23_CR9","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/79204.79210","volume":"33","author":"Alain Colmerauer","year":"1990","unstructured":"A. Colmerauer, \u201cAn Introduction to PROLOG III,\u201d C. ACM\n                33, 1990.","journal-title":"Communications of the ACM"},{"key":"23_CR10","volume-title":"PhD Thesis","author":"H. Comon","year":"1988","unstructured":"H. Comon, \u201cUnification et Disunification. Th\u00e9orie et Applications,\u201d PhD Thesis, Institut National Polytechnique de Grenoble, Grenoble, France, 1988."},{"key":"23_CR11","unstructured":"H. Comon, \u201cDisunification: a Survey,\u201d in J.-L. Lassez, G. Plotkin (editors), Computational Logic, MIT Press, 1991."},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, J.P. Jouannaud, \u201cRewrite Systems,\u201d in Volume B of \u201cHand-book of Theoretical Computer Science,\u201d North-Holland 1990.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"23_CR13","unstructured":"J.P. Jouannaud, C. Kirchner, \u201cSolving Equations in Abstract Algebras: A Rule-Based Survey of Unification,\u201d in J.-L. Lassez, G. Plotkin (editors), Computational Logic, MIT Press, 1991."},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"J. Jaffar, J.L. Lassez, \u201cConstraint Logic Programming,\u201d Proceedings of 14th POPL Conference, Munich, 1987.","DOI":"10.1145\/41625.41635"},{"issue":"2","key":"23_CR15","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BF00245463","volume":"9","author":"Deepak Kapur","year":"1992","unstructured":"D. Kapur, P. Narendran, \u201cComplexity of Unification Problems with Associative-Commutative Operators,\u201d J. Automated Reasoning\n                9, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"23_CR16","unstructured":"D. Kapur, P. Narendran, \u201cDouble Exponential Complexity of Computing Complete Sets of AC-unifiers,\u201d Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, Santa Cruz, California, 1992."},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"C. Kirchner, H. Kirchner, \u201cConstrained Equational Reasoning,\u201d Proceedings of SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, ACM Press, 1989.","DOI":"10.1145\/74540.74585"},{"key":"23_CR18","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schau\u00df, \u201cCombination of Unification Algorithms,\u201d J. Symbolic Computation\n                8, 1989.","DOI":"10.1016\/S0747-7171(89)80037-9"},{"issue":"5","key":"23_CR19","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1016\/0747-7171(92)90016-W","volume":"14","author":"Ralf Treinen","year":"1992","unstructured":"R. Treinen, \u201cA New Method for Undecidability Proofs of First Order Theories,\u201d J. Symbolic Computation\n                14, 1992.","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-21551-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,19]],"date-time":"2022-07-19T05:31:48Z","timestamp":1658208708000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-21551-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540568681","9783662215517"],"references-count":19,"aliases":["10.1007\/3-540-56868-9_23"],"URL":"https:\/\/doi.org\/10.1007\/978-3-662-21551-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}