{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:16:17Z","timestamp":1725664577152},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540629504"},{"type":"electronic","value":"9783540690511"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-62950-5_78","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:57:57Z","timestamp":1330297077000},"page":"284-298","source":"Crossref","is-referenced-by-count":1,"title":["A criterion for intractability of E-unification with free function symbols and its relevance for combination of unification algorithms"],"prefix":"10.1007","author":[{"given":"Klaus U.","family":"Schulz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"22_CR1","first-page":"50","volume":"607","author":"F. Baader","year":"1992","unstructured":"F. Baader, K.U. Schulz, \u201cUnification in the union of disjoint equational theories: Combining decision procedures,\u201d in: Proc. CADE-11, LNAI 607, 1992, pp. 50\u201365.","journal-title":"LNAI"},{"key":"22_CR2","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1006\/jsco.1996.0009","volume":"21","author":"F. Baader","year":"1996","unstructured":"F. Baader, K.U. Schulz, \u201cUnification in the union of disjoint equational theories: Combining decision procedures,\u201d Journal of Symbolic Computation, 21 (1996), pp. 211\u2013243.","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR3","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":"F. Baader, J. Siekmann, \u201cUnification Theory,\u201d in D.M. Gabbay, C. Hogger, and J. Robinson, Editors, Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press, Oxford, UK, 1994, pp. 41\u2013125."},{"key":"22_CR4","volume-title":"Progress in Theoretical Computer Science","author":"L. Bachmair","year":"1991","unstructured":"L. Bachmair, Canonical equational proofs, Progress in Theoretical Computer Science, Birkh\u00e4user, Boston, 1991."},{"key":"22_CR5","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1006\/jsco.1993.1066","volume":"16","author":"A. Boudet","year":"1993","unstructured":"A. Boudet, \u201cCombining Unification Algorithms,\u201d Journal of Symbolic Computation 16 (1993) pp. 597\u2013626.","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR6","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M.R. Garey","year":"1979","unstructured":"M.R. Garey, D.S. Johnson, \u201cComputers and Intractability: A Guide to the Theory of NP-Completeness,\u201d W.H. Freeman and Co. San Francisco (1979)."},{"doi-asserted-by":"crossref","unstructured":"Q. Guo, P. Narendran, and D.A. Wolfram \u201cUnification and Matching modulo Nilpotence,\u201d manuscript, received from Qing Guo, guo@cs.albany.edu, 1996.","key":"22_CR7","DOI":"10.1007\/3-540-61511-3_90"},{"doi-asserted-by":"crossref","unstructured":"M. Hermann, P.G. Kolaitis, \u201cUnification Algorithms Cannot be Combined in Polynomial Time,\u201d in Proceedings of the 13th International Conference on Automated Deduction, M.A. McRobbie and J.K. Slaney (Eds.), Springer LNAI 1104, 1996, pp. 246\u2013260.","key":"22_CR8","DOI":"10.1007\/3-540-61511-3_89"},{"key":"22_CR9","first-page":"450","volume":"230","author":"A. Herold","year":"1986","unstructured":"A. Herold, \u201cCombination of Unification Algorithms,\u201d Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986, pp. 450\u2013469.","journal-title":"LNCS"},{"key":"22_CR10","doi-asserted-by":"crossref","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.P. Jouannaud","year":"1986","unstructured":"J.P. Jouannaud, H. Kirchner, \u201cCompletion of a set of rules modulo a set of equations.\u201d SIAM J. Computing 15, 1986, pp. 1155\u20131194.","journal-title":"SIAM J. Computing"},{"key":"22_CR11","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/BF00245463","volume":"9","author":"D. Kapur","year":"1992","unstructured":"D. Kapur, P. Narendran, \u201cComplexity of Unification Problems with Associative-Commutative Operators,\u201d J. Automated Reasoning 9, 1992, pp. 261\u2013288.","journal-title":"J. Automated Reasoning"},{"unstructured":"S. Kepser, J. Richts, \u201cOptimization Techniques for the Combination of Unification Algorithms,\u201d to be submitted.","key":"22_CR12"},{"key":"22_CR13","volume-title":"Th\u00e8se d'Etat","author":"C. Kirchner","year":"1985","unstructured":"C. Kirchner, \u201cM\u00e9thodes et outils de conception syst\u00e9matique d'algorithmes d'unification dans les th\u00e9ories \u00e9quationelles,\u201d Th\u00e8se d'Etat, Universit\u00e9 de Nancy 1, France, 1985."},{"key":"22_CR14","first-page":"545","volume-title":"LNAI","author":"R. Niewenhuis","year":"1994","unstructured":"R. Niewenhuis, A. Rubio, \u201cAC-superposition with constraints: No AC-unifiers needed,\u201d in Proceedings of the 12th International Conference on Automated Deduction, Nancy, France, A. Bundy (Ed.), Springer LNAI 1994, pp.545\u2013559."},{"key":"22_CR15","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin, \u201cBuilding in equational theories,\u201d Machine Intelligence 7, 1972, pp. 73\u201390.","journal-title":"Machine Intelligence"},{"key":"22_CR16","first-page":"452","volume-title":"LNCS 1092","author":"A. Rubio","year":"1995","unstructured":"A. Rubio, \u201cTheorem Proving modulo Associativity,\u201d in Proceedings Computer Science Logic CSL'95, Paderborn, Germany, H. Kleine B\u00fcning (Ed.), Springer LNCS 1092 (1995), pp. 452\u2013467."},{"key":"22_CR17","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, \u201cCombination of Unification Algorithms,\u201d J. Symbolic Computation 8, 1989, pp. 51\u201399.","journal-title":"J. Symbolic Computation"},{"unstructured":"K.U. Schulz, \u201cCombination of Unification and Disunification Algorithms: Tractable and Intractable Instances,\u201d Research Paper, available under ftp.cis.uni-muenchen.de, in directory pub\/schulz. File name: ComplexityCombination.ps.gz","key":"22_CR18"},{"key":"22_CR19","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"M. Stickel, \u201cAutomated deduction by theory resolution,\u201d J. Automated Reasoning 1, 1985, pp. 333\u2013356.","journal-title":"J. Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"E. Tiden, \u201cUnification in Combinations of Collapse Free Theories with Disjoint Sets of Function Symbols,\u201d Proceedings of the 8th International Conference on Automated Deduction, LNCS 230, 1986.","key":"22_CR20","DOI":"10.1007\/3-540-16780-3_110"},{"doi-asserted-by":"crossref","unstructured":"K. Yelick, \u201cUnification in Combinations of Collapse Free Regular Theories,\u201d J. Symbolic Computation 3, 1987.","key":"22_CR21","DOI":"10.1016\/S0747-7171(87)80025-1"}],"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-62950-5_78.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T18:00:23Z","timestamp":1713636023000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-62950-5_78"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540629504","9783540690511"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-62950-5_78","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}