{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:35:19Z","timestamp":1742960119677,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631040"},{"type":"electronic","value":"9783540691402"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63104-6_3","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:04:13Z","timestamp":1330279453000},"page":"19-33","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["A New approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"3_CR1","volume-title":"Technical Report LTCS-Report 96-01","author":"F. Baader","year":"1996","unstructured":"F. Baader and C. Tinelli. A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method. Technical Report LTCS-Report 96-01, LuFG Theoretical Computer Science, RWTH-Aachen, Germany, 1996. Available via ftp as file Baader-Tinelli-LTCS-96.ps.gz in directory pub\/papers\/1996 on cantor.informatik.rwth-aachen.de."},{"key":"3_CR2","unstructured":"E. Domenjoud. Undecidability of the word problem in the union of theories sharing constructors. In Proceedings of the 10th International Workshop on Unification, UNIF'96. CIS-Report 96-9, CIS, Universit\u00e4t M\u00fcnchen, 1996."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"E. Domenjoud, F. Klay, and C. Ringeissen. Combination techniques for non-disjoint equational theories. In A. Bundy, editor, Proceedings 12th International Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 267\u2013281. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_19"},{"issue":"2","key":"3_CR4","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1006\/jsco.1994.1040","volume":"18","author":"H. Kirchner","year":"1994","unstructured":"H. Kirchner and C. Ringeissen. Combining symbolic constraint solvers on algebraic domains. Journal of Symbolic Computation, 18(2):113\u2013155, 1994.","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"D. E. Knuth and P. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"issue":"2","key":"3_CR6","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258\u2013282, 1982.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"3_CR7","first-page":"555","volume":"8","author":"J. Matijasevic","year":"1967","unstructured":"J. Matijasevic. Simple examples of undecidable associative calculi. Soviet Mathematics (Doklady), 8(2):555\u2013557, 1967.","journal-title":"Soviet Mathematics (Doklady)"},{"issue":"2","key":"3_CR8","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 Transactions on Programming Languages and Systems, 1(2):245\u2013257, Oct. 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"3_CR9","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D. C. Oppen. Fast decision procedures based on congruence closure. J. ACM, 27(2):356\u2013364, 1980.","journal-title":"J. ACM"},{"key":"3_CR10","first-page":"343","volume-title":"volume 335 of Lecture Notes in Computer Science","author":"T. Nipkow","year":"1989","unstructured":"T. Nipkow. Combining matching algorithms: The regular case. In N. Dershowitz, editor, Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, Chapel Hill (N.C., USA), volume 335 of Lecture Notes in Computer Science, pages 343\u2013358. Springer-Verlag, Apr. 1989."},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"D. C. Oppen","year":"1980","unstructured":"D. C. Oppen. Complexity, convexity and combinations of theories. Theoretical Computer Science, 12:291\u2013302, 1980.","journal-title":"Theoretical Computer Science"},{"key":"3_CR12","first-page":"121","volume-title":"Applied Logic","author":"C. Ringeissen","year":"1996","unstructured":"C. Ringeissen. Cooperation of decision procedures for the satisfiability problem. In Proceedings of the 1st International Workshop \u201cFrontiers of Combining Systems\u201d, Munich (Germany), Applied Logic, pages 121\u2013139. Kluwer, 1996."},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"J. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12:23\u201341, 1965.","journal-title":"J. ACM"},{"issue":"1\u20132","key":"3_CR14","doi-asserted-by":"publisher","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. Combination of unification algorithms. Journal of Symbolic Computation, 8(1\u20132):51\u2013100, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"3_CR15","volume-title":"Phd thesis","author":"E. Tid\u00e9n","year":"1986","unstructured":"E. Tid\u00e9n. First-Order Unification in Combinations of Equational Theories. Phd thesis, The Royal Institute of Technology, Stockholm, 1986."},{"key":"3_CR16","first-page":"103","volume-title":"Applied Logic","author":"C. Tinelli","year":"1996","unstructured":"C. Tinelli and M. Harandi. A new correctness proof of the Nelson-Oppen combination procedure. In Proceedings of the 1st International Workshop \u201cFrontiers of Combining Systems\u201d, Munich (Germany), Applied Logic, pages 103\u2013119. Kluwer, 1996."},{"key":"3_CR17","volume-title":"Technical report","author":"C. Tinelli","year":"1997","unstructured":"C. Tinelli and C. Ringeissen. Unions of theories and combinations of satisfiability procedures. Technical report, Department of Computer Science, University of Illinois at Urbana-Champaign, 1997. In preparation."},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1016\/0020-0190(87)90122-0","volume":"25","author":"Y. Toyama","year":"1987","unstructured":"Y. Toyama. Counterexamples to termination for the direct sum of term rewriting systems. Information Processing Letters, 25:141\u2013143, 1987.","journal-title":"Information Processing Letters"},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1145\/7531.7534","volume":"34","author":"Y. Toyama","year":"1987","unstructured":"Y. Toyama. On the Church-Rosser property for the direct sum of term rewriting systems. Journal of the ACM, 34(1):128\u2013143, 1987.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-14"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63104-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:45:36Z","timestamp":1558255536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}