{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T08:13:44Z","timestamp":1742976824655,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319214009"},{"type":"electronic","value":"9783319214016"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_38","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"557-571","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Regular Patterns in Second-Order Unification"],"prefix":"10.1007","author":[{"given":"Tomer","family":"Libal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"issue":"4","key":"38_CR1","first-page":"331","volume":"35","author":"H Abdulrab","year":"2001","unstructured":"Abdulrab, H., Goralcik, P., Makanin, G.S.: Towards parametrizing word equations. ITA 35(4), 331\u2013350 (2001)","journal-title":"ITA"},{"key":"38_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1007\/BFb0012885","volume-title":"9th International Conference on Automated Deduction","author":"P Andrews","year":"1988","unstructured":"Andrews, P., Issar, S., Nesmith, D., Pfenning, F.: The tps theorem proving system. In: Lusk, E.R., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 760\u2013761. Springer, Heidelberg (1988)"},{"key":"38_CR3","unstructured":"Barendregt, H.P.: The Lambda Calculus - Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1984)"},{"key":"38_CR4","unstructured":"Benzm\u00fcller, C., Paulson, L., Theiss, F., Fietzke, A.: The LEO-II project. In: Proceedings of the Fourteenth Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice. Imperial College, London (2007)"},{"issue":"2","key":"38_CR5","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"issue":"4","key":"38_CR6","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1006\/jsco.1997.0185","volume":"25","author":"H Comon","year":"1998","unstructured":"Comon, H.: Completion of rewrite systems with membership constraints. part i: deduction rules. J. Symb. Comput. 25(4), 397\u2013419 (1998)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"38_CR7","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0168-0072(88)90015-2","volume":"39","author":"WM Farmer","year":"1988","unstructured":"Farmer, W.M.: A unification algorithm for second-order monadic terms. Ann. Pure Appl. Logic 39(2), 131\u2013174 (1988)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1","key":"38_CR8","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0304-3975(06)80003-4","volume":"87","author":"WM Farmer","year":"1991","unstructured":"Farmer, W.M.: Simple second-order languages for which unification is undecidable. Theor. Comput. Sci. 87(1), 25\u201341 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"38_CR9","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"GP Huet","year":"1975","unstructured":"Huet, G.P.: A unification algorithm for typed lambda-calculus. Theor. Comput. Sci. 1(1), 27\u201357 (1975)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"38_CR10","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/78935.78938","volume":"37","author":"J Jaffar","year":"1990","unstructured":"Jaffar, J.: Minimal and complete word unification. J. ACM (JACM) 37(1), 47\u201385 (1990)","journal-title":"J. ACM (JACM)"},{"key":"38_CR11","unstructured":"Le Chenadec, P.: The finite automaton of an elementary cyclic set. Technical Report RR-0824, INRIA, April 1988"},{"key":"38_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/3-540-61464-8_63","volume-title":"Rewriting Techniques and Applications","author":"J Levy","year":"1996","unstructured":"Levy, J.: Linear second-order unification. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 332\u2013346. Springer, Heidelberg (1996)"},{"key":"38_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/BFb0052360","volume-title":"Rewriting Techniques and Applications","author":"J Levy","year":"1998","unstructured":"Levy, J.: Decidable and undecidable second-order unification problems. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 47\u201360. Springer, Heidelberg (1998)"},{"key":"38_CR14","unstructured":"Makanin, G.S.: On the decidability of the theory of free groups. In: FCT, pp. 279\u2013284 (1985). (in Russian)"},{"key":"38_CR15","unstructured":"Miller, D.: Unification of simply typed lambda-terms as logic programming. In: 8th International Logic Programming Conference, pp. 255\u2013269. MIT Press (1991)"},{"key":"38_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1007\/BFb0012891","volume-title":"9th International Conference on Automated Deduction","author":"L Paulson","year":"1988","unstructured":"Paulson, L.: Isabelle: the next seven hundred theorem provers. In: Lusk, E.R., Overbeek, R. (eds.) CADE 1988. LNCS, vol. 310, pp. 772\u2013773. Springer, Heidelberg (1988)"},{"key":"38_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1007\/3-540-58156-1_46","volume-title":"Automated Deduction - CADE-12","author":"C Prehofer","year":"1994","unstructured":"Prehofer, C.: Decidable higher-order unification problems. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 635\u2013649. Springer, Heidelberg (1994)"},{"issue":"6","key":"38_CR18","doi-asserted-by":"publisher","first-page":"929","DOI":"10.1093\/logcom\/12.6.929","volume":"12","author":"M Schmidt-Schau\u00df","year":"2002","unstructured":"Schmidt-Schau\u00df, M.: A decision algorithm for stratified context unification. J. Log. Comput. 12(6), 929\u2013953 (2002)","journal-title":"J. Log. Comput."},{"key":"38_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0052361","volume-title":"Rewriting Techniques and Applications","author":"M Schmidt-Schau\u00df","year":"1998","unstructured":"Schmidt-Schau\u00df, M., Schulz, K.U.: On the exponent of periodicity of minimal solutions of context equations. In: Nipkow, T. (ed.) RTA 1998. LNCS, vol. 1379, pp. 61\u201375. Springer, Heidelberg (1998)"},{"issue":"1","key":"38_CR20","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1006\/jsco.2001.0438","volume":"33","author":"M Schmidt-Schau\u00df","year":"2002","unstructured":"Schmidt-Schau\u00df, M., Schulz, K.U.: Solvability of context equations with two context variables is decidable. J. Symb. Comput. 33(1), 77\u2013122 (2002)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"38_CR21","doi-asserted-by":"publisher","first-page":"905","DOI":"10.1016\/j.jsc.2005.01.005","volume":"40","author":"M Schmidt-Schau\u00df","year":"2005","unstructured":"Schmidt-Schau\u00df, M., Schulz, K.U.: Decidability of bounded higher-order unification. J. Symb. Comput. 40(2), 905\u2013954 (2005)","journal-title":"J. Symb. Comput."},{"issue":"1\/2","key":"38_CR22","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W Snyder","year":"1989","unstructured":"Snyder, W., Gallier, J.H.: Higher-order unification revisited: complete sets of transformations. J. Symb. Comput. 8(1\/2), 101\u2013140 (1989)","journal-title":"J. Symb. Comput."},{"key":"38_CR23","unstructured":"Snyder, W.S.: Complete sets of transformations for general unification. Ph.D. thesis, Philadelphia, PA, USA (1988). AAI8824793"},{"key":"38_CR24","unstructured":"Wisnieski, M., Steen, A., Benzm\u00fcller, C.: The Leo-III project. In: Bolotov, A., Kerber, M. (eds) Joint Automated Reasoning Workshop and Deduktionstreffen, p. 38 (2014)"},{"key":"38_CR25","doi-asserted-by":"crossref","first-page":"309","DOI":"10.3233\/FI-1987-10304","volume":"X","author":"M Zaionc","year":"1987","unstructured":"Zaionc, M.: The regular expression descriptions of unifier sets in the typed lambda calculus. Fundamenta Informaticae X, 309\u2013322 (1987). North-Holland","journal-title":"Fundamenta Informaticae"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T09:46:59Z","timestamp":1676972819000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}