{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:46:55Z","timestamp":1725475615539},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672814"},{"type":"electronic","value":"9783540464211"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10720084_15","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T14:36:30Z","timestamp":1167402990000},"page":"217-244","source":"Crossref","is-referenced-by-count":2,"title":["Why Combined Decision Problems Are Often Intractable"],"prefix":"10.1007","author":[{"given":"Klaus U.","family":"Schulz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"15_CR1","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/S0020-0190(98)00106-9","volume":"67","author":"F. Baader","year":"1998","unstructured":"Baader, F.: On the Complexity of Boolean Unification. Information Processing Letters\u00a067(4), 215\u2013220 (1998)","journal-title":"Information Processing Letters"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0304-3975(94)00277-0","volume":"142","author":"F. Baader","year":"1995","unstructured":"Baader, F., Schulz, K.U.: Combination techniques and decision problems for disunification. Theoretical Computer Science\u00a0142, 229\u2013255 (1995)","journal-title":"Theoretical Computer Science"},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F. Baader","year":"1996","unstructured":"Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. Journal of Symbolic Computation\u00a021, 211\u2013243 (1996)","journal-title":"Journal of Symbolic Computation"},{"key":"15_CR4","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1093\/oso\/9780198537465.003.0002","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"F. Baader","year":"1994","unstructured":"Baader, F., Siekmann, J.: Unification Theory. In: Gabbay, D.M., Hogger, C., Robinson, J. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 41\u2013125. Oxford University Press, Oxford (1994)"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1006\/jsco.1993.1066","volume":"16","author":"A. Boudet","year":"1993","unstructured":"Boudet, A.: Combining Unification Algorithms. Journal of Symbolic Computation\u00a016, 597\u2013626 (1993)","journal-title":"Journal of Symbolic Computation"},{"key":"15_CR6","series-title":"LNAI","first-page":"463","volume-title":"Automated Deduction - CADE-12","author":"D. Cyrluk","year":"1994","unstructured":"Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak\u2019s decision procedure for combinations of theories. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 463\u2013477. Springer, Heidelberg (1994)"},{"key":"15_CR7","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/3-540-58156-1_19","volume-title":"Automated Deduction - CADE-12","author":"E. Domenjoud","year":"1994","unstructured":"Domenjoud, E., Klay, F., Ringeissen, R.: Combination Techniques for Non-Disjoint Equational Theories. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 267\u2013281. Springer, Heidelberg (1994)"},{"issue":"4","key":"15_CR8","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1145\/322092.322104","volume":"25","author":"P. Downey","year":"1994","unstructured":"Downey, P., Sethi, R.: Assignment commands with array references. Journal of the ACM\u00a025 (4), 652\u2013666 (1994)","journal-title":"Journal of the ACM"},{"key":"15_CR9","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Co., San Francisco (1979)"},{"key":"15_CR10","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/3-540-61511-3_90","volume-title":"Proceedings of the 13th Conference on Automated Deduction","author":"Q. Guo","year":"1996","unstructured":"Guo, Q., Narendran, P., Wolfram, D.A.: Unification and Matching modulo Nilpotence. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 261\u2013274. Springer, Heidelberg (1996)"},{"key":"15_CR11","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/3-540-61511-3_89","volume-title":"Automated Deduction - Cade-13","author":"M. Hermann","year":"1996","unstructured":"Hermann, M., Kolaitis, P.G.: Unification Algorithms Cannot be Combined in Polynomial Time. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 246\u2013260. Springer, Heidelberg (1996)"},{"key":"15_CR12","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1007\/3-540-16780-3_111","volume-title":"8th International Conference on Automated Deduction","author":"Alexander Herold","year":"1986","unstructured":"Herold, A.: Combination of Unification Algorithms. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230. Springer, Heidelberg (1986)"},{"key":"15_CR13","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/BF00245463","volume":"9","author":"D. Kapur","year":"1992","unstructured":"Kapur, D., Narendran, P.: Complexity of Unification Problems with Associative-Commutative Operators. J. Automated Reasoning\u00a09, 261\u2013288 (1992)","journal-title":"J. Automated Reasoning"},{"key":"15_CR14","first-page":"117","volume-title":"Frontiers of Combining Systems 2, Papers presented at FroCoS 1998","author":"S. Kepser","year":"2000","unstructured":"Kepser, S.: Negation in Combining Constraint Systems. In: Gabbay, D.M., de Rijke, M. (eds.) Frontiers of Combining Systems 2, Papers presented at FroCoS 1998, pp. 117\u2013192. Research Studies Press\/Wiley, Amsterdam (2000)"},{"key":"15_CR15","first-page":"193","volume-title":"Frontiers of Combining Systems 2, Papers presented at FroCo 1998","author":"S. Kepser","year":"2000","unstructured":"Kepser, S., Richts, J.: Optimization Techniques for Combining Constraint Solvers. In: Gabbay, D.M., de Rijke, M. (eds.) Frontiers of Combining Systems 2, Papers presented at FroCo 1998, pp. 193\u2013210. Research Studies Press\/Wiley, Amsterdam (2000)"},{"key":"15_CR16","unstructured":"Kirchner, C.: M\u00e9thodes et outils de conception syst\u00e9matique d\u2019algorithms d\u2019unification dans les th\u00e9ories \u00e9quationelles. Th\u00e8se d\u2019Etat, Universit\u00e9 de Nancy 1, France (1985)"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"Lankford, D.S., Butler, G., Brady, B.: Abelian Group Unification Algorithms for Elementary Terms. Contemporary Mathematics\u00a029 (1984)","DOI":"10.1090\/conm\/029\/749246"},{"issue":"1","key":"15_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"2","author":"C.G. Nelson","year":"1979","unstructured":"Nelson, C.G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Programming Languages and Systems\u00a02(1), 245\u2013257 (1979)","journal-title":"ACM Trans. Programming Languages and Systems"},{"issue":"2","key":"15_CR19","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"C.G. Nelson","year":"1980","unstructured":"Nelson, C.G., Oppen, D.C.: Fast decision algorithms based on congruence closure. Journal of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"key":"15_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1007\/3-540-51081-8_118","volume-title":"Rewriting Techniques and Applications","author":"T. Nipkow","year":"1989","unstructured":"Nipkow, T.: Combining Matching Algorithms: The Regular Case. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol.\u00a0355, pp. 343\u2013358. Springer, Heidelberg (1989)"},{"key":"15_CR21","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, Convexity and Combination of Theories. Theoretical Computer Science \u00a012, 291\u2013302 (1980)","journal-title":"Theoretical Computer Science"},{"key":"15_CR22","doi-asserted-by":"crossref","first-page":"15","DOI":"10.4064\/cm-30-1-15-25","volume":"XXX","author":"D. Pigozzi","year":"1974","unstructured":"Pigozzi, D.: The Join of Equational Theories. Colloquium Mathematicum\u00a0XXX, 15\u201325 (1974)","journal-title":"Colloquium Mathematicum"},{"key":"15_CR23","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-94-009-0349-4_6","volume-title":"Frontiers of Combining Systems, Proceedings of the 1st International Workshop, FroCoS 1996","author":"C. Ringeissen","year":"1996","unstructured":"Ringeissen, C.: Cooperation of Decision Procedures for the Satisfiability Problem. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, Proceedings of the 1st International Workshop, FroCoS 1996, Munich, Germany. Applied Logic Series, vol.\u00a03, pp. 121\u2013141. Kluwer, Dordrecht (1996)"},{"key":"15_CR24","doi-asserted-by":"crossref","unstructured":"Schaefer, T.J.: The complexity of satisfiability problems. In: Proceedings 10th Symposium on Theory of Computing, San Diego, CA, pp. 216\u2013226 (1978)","DOI":"10.1145\/800133.804350"},{"key":"15_CR25","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/S0747-7171(89)80022-7","volume":"8","author":"M Schmidt-Schau","year":"1989","unstructured":"Schmidt-Schau\u03b2, M.: Combination of Unification Algorithms. J. Symbolic Computation\u00a08, 51\u201399 (1989)","journal-title":"J. Symbolic Computation"},{"key":"15_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/3-540-62950-5_78","volume-title":"Rewriting Techniques and Applications","author":"K.U. Schulz","year":"1997","unstructured":"Schulz, K.U.: A Criterion for Intractability of E-unification with Free Function Symbols and its Relevance for Combination of Unification Algorithms. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 284\u2013298. Springer, Heidelberg (1997)"},{"issue":"1","key":"15_CR27","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1093\/logcom\/10.1.105","volume":"10","author":"K. Schulz","year":"2000","unstructured":"Schulz, K.U.: Tractable and Intractable Instances of Combination Problems for Unification and Disunification. To appear in Journal of Logic and Computation\u00a010(1) (2000)","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"15_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding Combinations of Theories. Journal of the ACM\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the ACM"},{"key":"15_CR29","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/3-540-16780-3_110","volume-title":"8th International Conference on Automated Deduction","author":"Erik Tid\u00e9n","year":"1986","unstructured":"Tid\u00e9n, E.: Unification in Combinations of Collapse Free Theories with Disjoint Sets of Function Symbols. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 431\u2013449. Springer, Heidelberg (1986)"},{"key":"15_CR30","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Frontiers of Combining Systems, Proceedings of the 1st International Workshop, FroCoS 1996","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.: A New Correctness Proof of the Nelson-Oppen Combination Procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems, Proceedings of the 1st International Workshop, FroCoS 1996, Munich, Germany. Applied Logic Series, vol.\u00a03, pp. 103\u2013121. Kluwer, Dordrecht (1996)"},{"issue":"1-2","key":"15_CR31","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/S0747-7171(87)80025-1","volume":"3","author":"Katherine A. Yelick","year":"1987","unstructured":"Yelick, K.: Unification in Combinations of Collapse Free Regular Theories. J. Symbolic Computation\u00a03 (1987)","journal-title":"Journal of Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10720084_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T17:26:20Z","timestamp":1707499580000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10720084_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672814","9783540464211"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/10720084_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}