{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:49:29Z","timestamp":1725551369577},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662013"},{"type":"electronic","value":"9783540486855"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48685-2_2","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:41Z","timestamp":1269897221000},"page":"16-29","source":"Crossref","is-referenced-by-count":6,"title":["Jeopardy"],"prefix":"10.1007","author":[{"given":"Nachum","family":"Dershowitz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Subrata","family":"Mitra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,11,5]]},"reference":[{"key":"2_CR1","unstructured":"Aguzzi, G., Modigliani, U.: A criterion to decide the semantic matching problem. Proc. Intl. Conf. on Logic and Algebra, Italy (1995)."},{"key":"2_CR2","series-title":"Lecture Notes in Artificial Intelligence","first-page":"582","volume-title":"Proc. 11th Intl. Conf. on Automated Deduction, Saratoga Springs, NY","author":"J. Christian","year":"1992","unstructured":"Christian, J.: Some termination criteria for narrowing and E-narrowing. Proc. 11th Intl. Conf. on Automated Deduction, Saratoga Springs, NY. Lecture Notes in Artificial Intelligence 607:582\u2013588, Springer-Verlag, Berlin (1992)."},{"key":"2_CR3","unstructured":"Comon, H.: On unification of terms with integer exponents. Tech. Rep. 770, Universit\u00e9 de Paris-Sud, Laboratoire de R\u00e9ch\u00e9rche en Informatique (1992)."},{"key":"2_CR4","unstructured":"Comon, H., Haberstrau, M., Jouannaud, J.P.: Decidable problems in shallow equational theories. Tech. Rep. 718, Universit\u00e9 de Paris-Sud, Laboratoire de R\u00e9ch\u00e9rche en Informatique (1991)."},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In J. van Leeuwen, ed., Handbook of Theoretical Computer Science B: 243\u2013320, North-Holland, Amsterdam (1990).","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"2_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/3-540-57529-4_49","volume-title":"Proc. 13th Conf. on Foundations of Software Technology and Theoretical Computer Science, Bombay, India","author":"N. Dershowitz","year":"1993","unstructured":"Dershowitz, N., Mitra, S.: Higher-order and semantic unification. Proc. 13th Conf. on Foundations of Software Technology and Theoretical Computer Science, Bombay, India. Lecture Notes in Artificial Intelligence 761:139\u2013150, Springer-Verlag, Berlin (1993)."},{"key":"2_CR7","series-title":"Lecture Notes in Artificial Intelligence","first-page":"589","volume-title":"Proc. 11th Conference on Automated Deduction, Saratoga Springs, NY","author":"N. Dershowitz","year":"1992","unstructured":"Dershowitz, N., Mitra, S., Sivakumar., G.: Decidable matching for convergent systems (Preliminary version). Proc. 11th Conference on Automated Deduction, Saratoga Springs, NY. Lecture Notes in Artificial Intelligence 607:589\u2013602, Springer-Verlag, Berlin (1992)."},{"key":"2_CR8","first-page":"21","volume-title":"Machine Intelligence","author":"N. Dershowitz","year":"1988","unstructured":"Dershowitz, N., Plaisted, D. A.: Equational programming. In: J. E. Hayes, D. Michie, J. Richards, eds., Machine Intelligence 11: The logic and acquisition of knowledge, 21\u201356. Oxford Press, Oxford (1988)."},{"key":"2_CR9","volume-title":"Calendrical Calculations","author":"N. Dershowitz","year":"1997","unstructured":"Dershowitz, N., Reingold, E. M.: Calendrical Calculations. Cambridge University Press, Cambridge (1997)."},{"key":"2_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/3-540-12727-5_12","volume-title":"Proc. 8th Colloq. on Trees in Algebra and Programming, L\u2019Aquila, Italy","author":"F. Fages","year":"1983","unstructured":"Fages, F., Huet, G.: Unification and matching in equational theories. Proc. 8th Colloq. on Trees in Algebra and Programming, L\u2019Aquila, Italy. Lecture Notes in Computer Science 159:205\u2013220, Springer-Verlag, Berlin (1983)."},{"issue":"2","key":"2_CR11","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/BF00264362","volume":"24","author":"S. Heilbrunner","year":"1987","unstructured":"Heilbrunner, S., H\u00f6lldobler, S.: The undecidability of the unification and matching problem for canonical theories. Acta Informatica 24(2):157\u2013171 (1987).","journal-title":"Acta Informatica"},{"key":"2_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"Proc. 5th Intl. Conf. on Automated Deduction, Les Arcs, France","author":"J.-M. Hullot","year":"1980","unstructured":"Hullot, J.-M.: Canonical forms and unification. Proc. 5th Intl. Conf. on Automated Deduction, Les Arcs, France, Lecture Notes in Computer Science 87:318\u2013334, Springer-Verlag, Berlin (1980)."},{"key":"2_CR13","series-title":"Lect Notes Comput Sci","first-page":"362","volume-title":"Proc. 7th Intl. Conf. on Rewriting Techniques and Applications, New Brunswick, NJ","author":"F. Jacquemard","year":"1966","unstructured":"Jacquemard, F.: Decidable approximations of term rewriting systems. Proc. 7th Intl. Conf. on Rewriting Techniques and Applications, New Brunswick, NJ. Lecture Notes in Computer Science 1103:362\u2013376, Springer-Verlag, Berlin (1966)."},{"key":"2_CR14","series-title":"Tech. Rep.","volume-title":"Semantic unification for convergent systems","author":"S. Mitra","year":"1994","unstructured":"Mitra, S.: Semantic unification for convergent systems. Ph.D. thesis, Dept. of Computer Science, University of Illinois, Urbana, IL, Tech. Rep. UIUCDCS-R-94-1855 (1994)."},{"issue":"2","key":"2_CR15","doi-asserted-by":"publisher","first-page":"636","DOI":"10.2307\/2275552","volume":"62","author":"P. Narendran","year":"1997","unstructured":"Narendran, P., Pfenning, F., Statman, R.: On the unification problem for Cartesian closed categories. J. Symbolic Logic 62(2):636\u2013647 (1997).","journal-title":"J. Symbolic Logic"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R.: Decidability and complexity analysis by basic paramodulation. Information and Computation 147:1\u201321 (1998).","DOI":"10.1006\/inco.1998.2730"},{"key":"2_CR17","first-page":"182","volume":"65","author":"D. A. Plaisted","year":"1985","unstructured":"Plaisted, D. A.: Semantic confluence tests and completion methods. Information and Computation 65:182\u2013215 (1985).","journal-title":"Information and Computation"}],"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-48685-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:02:33Z","timestamp":1558983753000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48685-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662013","9783540486855"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48685-2_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}