{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:22:02Z","timestamp":1725495722365},"publisher-location":"Berlin, Heidelberg","reference-count":16,"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\/bfb0052360","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T05:31:11Z","timestamp":1149658271000},"page":"47-60","source":"Crossref","is-referenced-by-count":13,"title":["Decidable and undecidable second-order unification problems"],"prefix":"10.1007","author":[{"given":"Jordi","family":"Levy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,18]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"H. Comon. Completion of rewrite systems with membership constraints. Technical report, CNRS and LRI, Universit\u00e9 de Paris Sud, 1993.","DOI":"10.1007\/3-540-55719-9_91"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Reduction of second-order unification to simultaneous rigid E-unification. Technical Report 109, Computer Science Department, Uppsala University, 1995.","DOI":"10.1007\/3-540-61377-3_38"},{"issue":"1\u20132","key":"5_CR3","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","volume":"166","author":"A. Degtyarev","year":"1996","unstructured":"A. Degtyarev and A. Voronkov. The undecidability of simultaneous rigid E-unification. Theoretical Computer Science, 166(1\u20132):291\u2013300, 1996.","journal-title":"Theoretical Computer Science"},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0168-0072(88)90015-2","volume":"39","author":"W. M. Farmer","year":"1988","unstructured":"W. M. Farmer. A unification algorithm for second-order monadic terms. Annals of Pure and Applied Logic, 39:131\u2013174, 1988.","journal-title":"Annals of Pure and Applied Logic"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"J. H. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification is NP-complete. In Proc. IEEE Conf. on Logic in Computer Science, LICS'88, pages 338\u2013346, 1988.","DOI":"10.1109\/LICS.1988.5121"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. D. Goldfarb","year":"1981","unstructured":"W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225\u2013230, 1981.","journal-title":"Theoretical Computer Science"},{"key":"5_CR7","unstructured":"J. H. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification: Equational matings. In Proc. IEEE Conf. on Logic in Computer Science, LICS'87, pages 338\u2013346, 1987."},{"key":"5_CR8","first-page":"273","volume":"40","author":"J. H. Gallier","year":"1990","unstructured":"J. H. Gallier and W. Snyder. Designing unification procedures using transformations: A survey. Bulletin of the EATCS, 40:273\u2013326, 1990.","journal-title":"Bulletin of the EATCS"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"J. Levy. Linear second-order unification. In 7th Int. Conf. on Rewriting Techniques and Applications, RTA '96, volume 1103 of LNCS, pages 332\u2013346, New Jersey, USA, 1996.","DOI":"10.1007\/3-540-61464-8_63"},{"issue":"2","key":"5_CR11","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"G. S. Makanin","year":"1977","unstructured":"G. S. Makanin. The problem of solvability of equations in a free semigroup. Math. USSR Sbornik, 32(2):129\u2013198, 1977.","journal-title":"Math. USSR Sbornik"},{"issue":"2","key":"5_CR12","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/321752.321764","volume":"20","author":"T. Pietrzykowski","year":"1973","unstructured":"T. Pietrzykowski. A complete mechanization of second-order logic. J. of the ACM, 20(2):333\u2013364, 1973.","journal-title":"J. of the ACM"},{"key":"5_CR13","unstructured":"K. U. Schulz. Makanin's algorithm, two improvements and a generalization. Technical Report CIS-Bericht-91-39, Centrum f\u00fcr Informations und Sprachverarbeitung, Universit\u00e4t M\u00fcnchen, 1991."},{"key":"5_CR14","unstructured":"A. Schubert. Second-order unification and type inference for church-style polymorphism. Technical Report TR 97-02(239), Institute of Informatics, Warsaw University, 1997."},{"key":"5_CR15","volume-title":"Technical Report 12\/94","author":"M. Schmidt-Schau\u00df","year":"1995","unstructured":"M. Schmidt-Schau\u00df. Unification of stratified second-order terms. Technical Report 12\/94, Johan Wolfgang-Goethe-Universit\u00e4t, Frankfurt, Germany, 1995."},{"key":"5_CR16","unstructured":"M. Veanes. The relation between second-order unification and simultaneous rigid E-unification. Technical Report MPI-I-98-2-005, Max-Planck Institut f\u00fcr Informatik, 1998."}],"container-title":["Lecture Notes in Computer Science","Rewriting Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052360","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T06:33:19Z","timestamp":1555655599000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052360"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643012","9783540697213"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0052360","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}