{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:21Z","timestamp":1761611181512},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643012"},{"type":"electronic","value":"9783540697213"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0052362","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T01:31:11Z","timestamp":1149643871000},"page":"76-90","source":"Crossref","is-referenced-by-count":21,"title":["Unification in extensions of shallow equational theories"],"prefix":"10.1007","author":[{"given":"Florent","family":"Jacquemard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,18]]},"reference":[{"issue":"2","key":"7_CR1","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L. Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C. & Snyder, W. (1995), \u2018Basic paramodulation', Information and Computation 121(2), 172\u2013192.","journal-title":"Information and Computation"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Bogaert, B. & Tison, S. (1992), Equality and disequality constraints on direct subterms in tree automata, in A. Finkel & M. Jantzen, eds, \u2018Proceedings of 9th Annual Symposium on Theoretical Aspects of Computer Science, STACS92', Vol. 577 of LNCS, Springer, pp. 161\u2013171.","DOI":"10.1007\/3-540-55210-3_181"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Comon, H. (1995), Sequentially, second order monadic logic and tree automata, in \u2018Proceedings 10th IEEE Symposium on Logic in Computer Science, LICS'95', IEEE Computer Society Press, pp. 508\u2013517.","DOI":"10.1109\/LICS.1995.523285"},{"issue":"1","key":"7_CR4","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1006\/inco.1994.1043","volume":"111","author":"H. Comon","year":"1994","unstructured":"Comon, H., Haberstrau, M. & Jouannaud, J.-P. (1994), \u2018Syntacticness, cyclesyntacticness and shallow theories', Information and Computation 111(1), 154\u2013191.","journal-title":"Information and Computation"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Dershowitz, N. & Jouannaud, J.-P. (1990), Rewrite systems, in J. van Leeuwen, ed., \u2018Handbook of Theoretical Computer Science', Vol. B, Elsevier Science Publishers, chapter 6, pp. 243\u2013320.","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"7_CR6","first-page":"4","volume-title":"LNCS 1249","author":"I. Durand","year":"1997","unstructured":"Durand, I. & Middeldorp, A. (1997), Decidable call by need computations in term rewriting (extended abstract), in W. McCune, ed., \u2018Automated Deduction \u2014 CADE-14, 14th International Conference on Automated Deduction', LNCS 1249, Springer-Verlag, Townsville, North Queensland, Australia, pp. 4\u201318."},{"key":"7_CR7","volume-title":"Vol. 1139 of Lecture notes in computer science","author":"H. Fassbender","year":"1996","unstructured":"Fassbender, H. & Maneth, S. (1996), A strict border for the decidability of e-unification for recursive functions, in M. Hanus & M. Rodr\u00edguez-Artalejo, eds, \u2018Algebraic and Logic Programming (ALP-5):5th international conference, Aachen, Germany, September 25\u201327, 1996', Vol. 1139 of Lecture notes in computer science, Springer, Berlin."},{"key":"7_CR8","first-page":"321","volume-title":"Vol. 1249 of LNAI","author":"H. Ganzinger","year":"1997","unstructured":"Ganzinger, H., Meyer, C. & Weidenbach, C. (1997), Soft typing for ordered resolution, in \u2018Proceedings of the 14th International Conference on Automated Deduction, CADE-14', Vol. 1249 of LNAI, Springer, Townsville, Australia, pp. 321\u2013335."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Jacquemard, F. (1996), Decidable approximations of term rewriting systems, in H. Ganzinger, ed., \u2018Rewriting Techniques and Applications, 7th International Conference, RTA-96', Vol. 1103 of LNCS, Springer, pp. 362\u2013376.","DOI":"10.1007\/3-540-61464-8_65"},{"key":"7_CR10","volume-title":"MPI-Report MPI-I-98-2-002","author":"F. Jacquemard","year":"1998","unstructured":"Jacquemard, F., Meyer, C. & Weidenbach, C. (1998), Unification in extensions of shallow equational theories, MPI-Report MPI-I-98-2-002, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany."},{"key":"7_CR11","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1006\/jsco.1996.0077","volume":"23","author":"Y. Kaji","year":"1997","unstructured":"Kaji, Y., Toru, F. & Kasami, T. (1997), \u2018Solving a unification problem under constrained substitutions using tree automata', Journal of Symbolic Computation\n                        23, 79\u2013117.","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR12","unstructured":"Kirchner, C. (1986), Computing unification algorithms, in \u2018Proceedings of the First Symposium on Logic in Computer Science', Cambridge, Massachusetts, pp. 206\u2013216."},{"key":"7_CR13","volume-title":"E-unification by means of tree tuple synchronized grammars","author":"S. Limet","year":"1997","unstructured":"Limet, S. & R\u00e9ty, P. (1997), E-unification by means of tree tuple synchronized grammars, in M. Bidoit & M. Dauchet, eds, \u2018TAPSOFT '97: Proceedings of the Seventh Joint Conference on Theory and Practice of Software Development, 7th International Joint Conference CAAP\/FASE, Lille, France', Vol. 1214, Springer-Verlag, Lille, France."},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R. (1996), Basic paramodulation and decidable theories (extended abstract), in \u2018Proceedings 11th IEEE Symposium on Logic in Computer Science, LICS'96', IEEE Computer Society Press, pp. 473\u2013482.","DOI":"10.1109\/LICS.1996.561464"},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1006\/jsco.1995.1020","volume":"19","author":"R. Nieuwenhuis","year":"1995","unstructured":"Nieuwenhuis, R. & Rubio, A. (1995), \u2018Theorem proving with ordering and equality constrained clauses', Journal of Symbolic Computation\n                        19, 321\u2013351.","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR16","first-page":"367","volume-title":"LNCS 914","author":"F. Otto","year":"1995","unstructured":"Otto, F., Narendran, P. & Dougherty, D. J. (1995), Some independence results for equational unification, in J. Hsiang, ed., \u2018Rewriting Techniques and Applications, 6th International Conference, RTA-95', LNCS 914, Springer-Verlag, Kaiserslautern, Germany, pp. 367\u2013381."},{"issue":"5","key":"7_CR17","first-page":"718","volume":"73","author":"M. Oyamaguchi","year":"1990","unstructured":"Oyamaguchi, M. (1990), \u2018On the word problem for right-ground term-rewriting systems', The Transactions of the IEICE 73(5), 718\u2013723.","journal-title":"The Transactions of the IEICE"},{"issue":"2","key":"7_CR18","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"18","author":"C. Weidenbach","year":"1997","unstructured":"Weidenbach, C. (1997), \u2018Spass version 0.49', Journal of Automated Reasoning 18(2), 247\u2013252.","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR19","unstructured":"Weidenbach, C. (1998), Sorted unification and tree automata, in W. Bibel & P. H. Schmitt, eds, \u2018Automated Deduction, A Basis for Applications', Vol. 1, Kluwer, chapter 2."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052362","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,10]],"date-time":"2019-02-10T17:29:12Z","timestamp":1549819752000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052362"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643012","9783540697213"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0052362","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}