{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:38:29Z","timestamp":1725557909656},"publisher-location":"Berlin, Heidelberg","reference-count":78,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540250517"},{"type":"electronic","value":"9783540322542"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32254-2_10","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T19:16:54Z","timestamp":1277234214000},"page":"154-168","source":"Crossref","is-referenced-by-count":1,"title":["Decidable Variants of Higher-Order Unification"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","volume-title":"An introduction to mathematical logic and type theory: to truth through proof","author":"P. Andrews","year":"1986","unstructured":"Andrews, P.: An introduction to mathematical logic and type theory: to truth through proof. Academic Press, London (1986)"},{"key":"10_CR2","series-title":"ch. 15","doi-asserted-by":"publisher","first-page":"965","DOI":"10.1016\/B978-044450813-3\/50017-5","volume-title":"Handbook of Automated Reasoning","author":"P. Andrews","year":"2001","unstructured":"Andrews, P.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 15, vol.\u00a02, pp. 965\u20131007. North-Holland, Amsterdam (2001)"},{"key":"10_CR3","volume-title":"The Lambda Calculus. Its Syntax and Semantics","author":"H.P. Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam (1984)"},{"key":"10_CR4","series-title":"ch. 7","first-page":"321","volume-title":"Handbook of Theoretical Computer Science: Formal Models and Semantics","author":"H.P. Barendregt","year":"1990","unstructured":"Barendregt, H.P.: Functional programming and lambda calculus. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: Formal Models and Semantics, ch. 7, vol.\u00a0B, pp. 321\u2013363. Elsevier, Amsterdam (1990)"},{"key":"10_CR5","volume-title":"Introduction to Functional Programming using Haskell","author":"R. Bird","year":"1998","unstructured":"Bird, R.: Introduction to Functional Programming using Haskell. Prentice Hall, Englewood Cliffs (1998)"},{"doi-asserted-by":"crossref","unstructured":"Burstall, R., MacQueen, D., Sanella, D.T.: Hope: an experimental applicative language. In: Proc. LISP Conference, pp. 136\u2013143 (1980)","key":"10_CR6","DOI":"10.1145\/800087.802799"},{"key":"10_CR7","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"},{"key":"10_CR8","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":"Baader, F., Siekmann, J.: Unification theory. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 41\u2013125. Oxford University Press, Oxford (1994)"},{"unstructured":"Clark, J., DeRose, S. (eds.): XML Path Language (XPath) Version 1.0. W3C, November 16 (1999), http:\/\/www.w3.org\/TR\/1999\/REC-xpath-19991116","key":"10_CR9"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/BFb0028013","volume-title":"Computer Science Logic","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Higher-order matching and tree automata. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol.\u00a01414, pp. 157\u2013176. Springer, Heidelberg (1998)"},{"issue":"4","key":"10_CR11","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. of Symbolic Computation\u00a025(4), 397\u2013419 (1998)","journal-title":"J. of Symbolic Computation"},{"issue":"4","key":"10_CR12","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1006\/jsco.1997.0186","volume":"25","author":"H. Comon","year":"1998","unstructured":"Comon, H.: Completion of rewrite systems with membership constraints. Part II: Constraint solving. J. of Symbolic Computation\u00a025(4), 421\u2013453 (1998)","journal-title":"J. of Symbolic Computation"},{"unstructured":"Contejean, E.: Unification under distributivity, Unification workshop, Dagstuhl, Germany (1992)","key":"10_CR13"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1006\/jsco.1993.1060","volume":"16","author":"E. Contejean","year":"1993","unstructured":"Contejean, E.: Solving *-problems modulo distributivity by a reduction to AC1-unification. J. of Symbolic Computation\u00a016, 493\u2013521 (1993)","journal-title":"J. of Symbolic Computation"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/10721975_9","volume-title":"Rewriting Techniques and Applications","author":"P. Groote de","year":"2000","unstructured":"de Groote, P.: Linear higher-order matching is NP-complete. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 127\u2013140. Springer, Heidelberg (2000)"},{"key":"10_CR16","series-title":"ch. 6","first-page":"243","volume-title":"Handbook of Theoretical Computer Science: Formal Models and Semantics","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science: Formal Models and Semantics, ch. 6, vol.\u00a0B, pp. 243\u2013320. Elsevier, Amsterdam (1990)"},{"doi-asserted-by":"crossref","unstructured":"Dowek, G.: Third order matching is decidable. In: Proceedings of the 7th Annual IEEE Symposium on Logic in Computer Science, pp. 2\u201310 (1992)","key":"10_CR17","DOI":"10.1109\/LICS.1992.185514"},{"key":"10_CR18","series-title":"ch. 16","doi-asserted-by":"publisher","first-page":"1009","DOI":"10.1016\/B978-044450813-3\/50018-7","volume-title":"Handbook of Automated Reasoning","author":"G. Dowek","year":"2001","unstructured":"Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 16, vol.\u00a02, pp. 1009\u20131062. North-Holland, Amsterdam (2001)"},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/10721975_8","volume-title":"Rewriting Techniques and Applications","author":"K. Erk","year":"2000","unstructured":"Erk, K., Niehren, J.: Parallelism constraints. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 110\u2013126. Springer, Heidelberg (2000)"},{"key":"10_CR20","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0168-0072(88)90015-2","volume":"39","author":"W.A. Farmer","year":"1988","unstructured":"Farmer, W.A.: A unification algorithm for second order monadic terms. Annals of Pure and Applied Logic\u00a039, 131\u2013174 (1988)","journal-title":"Annals of Pure and Applied Logic"},{"key":"10_CR21","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/S0304-3975(06)80003-4","volume":"87","author":"W.A. Farmer","year":"1991","unstructured":"Farmer, W.A.: Simple second-order languages for which unification is un-decidable. J. Theoretical Computer Science\u00a087, 173\u2013214 (1991)","journal-title":"J. Theoretical Computer Science"},{"key":"10_CR22","series-title":"Applied Logic Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-011-3981-6","volume-title":"Proof Theory and Automated Deduction","author":"J. Goubault-Larrecq","year":"1997","unstructured":"Goubault-Larrecq, J., Mackie, I.: Proof Theory and Automated Deduction. Applied Logic Series, vol.\u00a06. Kluwer, Dordrecht (1997) ISBN 0-7923-4593-2"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science\u00a013, 225\u2013230 (1981)","journal-title":"Theoretical Computer Science"},{"key":"10_CR24","first-page":"112","volume-title":"Proceedings FOCS 1998","author":"C. Gutierrez","year":"1998","unstructured":"Gutierrez, C.: Satisfiability of word equations with constants is in exponential space. In: Proceedings FOCS 1998, Palo Alto, California, pp. 112\u2013119. IEEE Computer Society Press, Los Alamitos (1998)"},{"unstructured":"Hanus, M., Kuchen, H., Moreno-Navarro, J.J.: Curry: A truly functional logic language. In: Proc. ILPS 1995 Workshop on Visions for the Future of Logic Programming, pp. 95\u2013107 (1995)","key":"10_CR25"},{"key":"10_CR26","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"Huet, G., Lang, B.: Proving and applying program transformations expressed with second-order patterns. Acta Informatica\u00a011, 31\u201355 (1978)","journal-title":"Acta Informatica"},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G. Huet","year":"1973","unstructured":"Huet, G.: Undecidability of unification in third-order logic. Information and Control\u00a022, 257\u2013267 (1973)","journal-title":"Information and Control"},{"key":"10_CR28","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science\u00a01, 27\u201357 (1975)","journal-title":"Theoretical Computer Science"},{"unstructured":"Huet, G.: R\u00e9solution d\u2019\u00e9quations dans des langages d\u2019ordre 1,2,. w. Th\u00e8se de doctorat d\u2018etat, Universit\u00e9 Paris VII (1976) (in French)","key":"10_CR29"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/3-540-48686-0_43","volume-title":"Computing and Combinatorics","author":"K. Hirata","year":"1999","unstructured":"Hirata, K., Yamada, K., Harao, M.: Tractable and intractable second-order matching problems. In: Asano, T., Imai, H., Lee, D.T., Nakano, S.-i., Tokuyama, T. (eds.) COCOON 1999. LNCS, vol.\u00a01627, pp. 432\u2013441. Springer, Heidelberg (1999)"},{"issue":"2","key":"10_CR31","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(76)90021-9","volume":"3","author":"D. Jensen","year":"1976","unstructured":"Jensen, D., Pietrzykowski, T.: Meachanizing \u03c9-order type theory through unification. Theoretical Computer Science\u00a03(2), 123\u2013171 (1976)","journal-title":"Theoretical Computer Science"},{"key":"10_CR32","first-page":"2","volume-title":"Handbook of Logic in Computer Science","author":"J.W. Klop","year":"1992","unstructured":"Klop, J.W.: Term rewriting systems. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol.\u00a02, pp. 2\u2013116. Oxford University Press, Oxford (1992)"},{"key":"10_CR33","doi-asserted-by":"crossref","first-page":"670","DOI":"10.1145\/234533.234543","volume":"43","author":"A. Ko\u015bcielski","year":"1996","unstructured":"Ko\u015bcielski, A., Pacholski, L.: Complexity of Makanin\u2019s algorithms. Journal of the Association for Computing Machinery\u00a043, 670\u2013684 (1996)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a01103, pp. 332\u2013346. Springer, Heidelberg (1996)"},{"key":"10_CR35","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.\u00a01379, pp. 47\u201360. Springer, Heidelberg (1998)"},{"unstructured":"Loader, R.: Higher-order \u03b2 matching is undecidable (2001) draft","key":"10_CR36"},{"key":"10_CR37","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1006\/inco.2000.2877","volume":"159","author":"J. Levy","year":"2000","unstructured":"Levy, J., Veanes, M.: On the undecidability of second-order unification. Information and Computation\u00a0159, 125\u2013150 (2000)","journal-title":"Information and Computation"},{"issue":"2","key":"10_CR38","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"G.S. Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Math. USSR Sbornik\u00a032(2), 129\u2013198 (1977)","journal-title":"Math. USSR Sbornik"},{"issue":"4","key":"10_CR39","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables and simple unification. J. of Logic and Computation\u00a01(4), 497\u2013536 (1991)","journal-title":"J. of Logic and Computation"},{"issue":"2","key":"10_CR40","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1979","unstructured":"Martelli, A., Montanari, U.: An efficient unification algorithm. ACM TOPLAS\u00a04(2), 258\u2013282 (1979)","journal-title":"ACM TOPLAS"},{"unstructured":"Narendran, P.: Some remarks on second order unification. Technical report, Inst. of Programming and Logics, Department of Computer Science, Univ. of NY at Albany (1990)","key":"10_CR41"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Higher-order critical pairs. In: Proc. 6th IEEE Symp. LICS, pp. 342\u2013349 (1991)","key":"10_CR42","DOI":"10.1109\/LICS.1991.151658"},{"key":"10_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/3-540-63104-6_4","volume-title":"Automated Deduction - CADE-14","author":"J. Niehren","year":"1997","unstructured":"Niehren, J., Pinkal, M., Ruhrberg, P.: On equality up-to constraints over finite trees, context unification, and one-step rewriting. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 34\u201348. Springer, Heidelberg (1997)"},{"doi-asserted-by":"crossref","unstructured":"Niehren, J., Pinkal, M., Ruhrberg, P.: A uniform approach to underspecification and parallelism. In: Proceedings of the 35th Annual Meeting of the Association of Computational Linguistics (ACL), Madrid, Spain, pp. 410\u2013417 (1997)","key":"10_CR44","DOI":"10.3115\/976909.979670"},{"key":"10_CR45","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0020-0190(00)00036-3","volume":"74","author":"J. Niehren","year":"2000","unstructured":"Niehren, J., Tison, S., Treinen, R.: On rewrite constraints and context unification. Information Processing Letters\u00a074, 35\u201340 (2000)","journal-title":"Information Processing Letters"},{"key":"10_CR46","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","author":"V. Padovani","year":"1996","unstructured":"Padovani, V.: Decidability of all minimal models. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158. Springer, Heidelberg (1996)"},{"issue":"3","key":"10_CR47","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1017\/S0960129500003108","volume":"10","author":"V. Padovani","year":"2000","unstructured":"Padovani, V.: Decidability of fourth-order matching. Mathematical Structures in Computer Science\u00a010(3), 361\u2013372 (2000)","journal-title":"Mathematical Structures in Computer Science"},{"key":"10_CR48","volume-title":"ML for the working programmer","author":"L.C. Paulson","year":"1991","unstructured":"Paulson, L.C.: ML for the working programmer. Cambridge University Press, Cambridge (1991)"},{"key":"10_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"10_CR50","series-title":"ch. 17","doi-asserted-by":"publisher","first-page":"1063","DOI":"10.1016\/B978-044450813-3\/50019-9","volume-title":"Handbook of Automated Reasoning","author":"F. Pfenning","year":"2001","unstructured":"Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 17, vol.\u00a02, pp. 1063\u20131147. North-Holland, Amsterdam (2001)"},{"key":"10_CR51","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/321752.321764","volume":"20","author":"T. Pietrzykowski","year":"1973","unstructured":"Pietrzykowski, T.: A complete mechanization of second-order type theory. J. ACM\u00a020, 333\u2013364 (1973)","journal-title":"J. ACM"},{"key":"10_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/BFb0049431","volume-title":"Algorithms - ESA \u201994","author":"W. Plandowski","year":"1994","unstructured":"Plandowski, W.: Testing equivalence of morphisms in context-free languages. In: van Leeuwen, J. (ed.) ESA 1994. LNCS, vol.\u00a0855, pp. 460\u2013470. Springer, Heidelberg (1994)"},{"doi-asserted-by":"crossref","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. In: FOCS 1999, pp. 495\u2013500 (1999)","key":"10_CR53","DOI":"10.1109\/SFFCS.1999.814622"},{"key":"10_CR54","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"Plotkin, G.: Building in equational theories. Machine Intelligence\u00a07, 73\u201390 (1972)","journal-title":"Machine Intelligence"},{"unstructured":"Prehofer, C.: Solving Higher-order Equations: From Logic to Programming. Ph.D. thesis, Technische Universitat Munchen (1995) (in German)","key":"10_CR55"},{"issue":"2","key":"10_CR56","first-page":"158","volume":"16","author":"M.S. Paterson","year":"1978","unstructured":"Paterson, M.S., Wegman, M.N.: Linear unification. JCSS\u00a016(2), 158\u2013167 (1978)","journal-title":"JCSS"},{"issue":"1","key":"10_CR57","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine oriented logic based on the resolution principle. J. of the ACM\u00a012(1), 23\u201341 (1965)","journal-title":"J. of the ACM"},{"unstructured":"Siekmann, J.H.: String-unification. internal report Memo CSM-7, Essex university (1975)","key":"10_CR58"},{"key":"10_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0047111","volume-title":"7th International Conference on Automated Deduction","author":"J.H. Siekmann","year":"1984","unstructured":"Siekmann, J.H.: Universal unification. In: Shostak, R.E. (ed.) CADE 1984. LNCS, vol.\u00a0170, pp. 1\u201342. Springer, Heidelberg (1984)"},{"issue":"3,4","key":"10_CR60","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J.H. Siekmann","year":"1989","unstructured":"Siekmann, J.H.: Unification theory: A survey. J. Symbolic Computation\u00a07(3,4), 207\u2013274 (1989)","journal-title":"J. Symbolic Computation"},{"unstructured":"Schmidt-Schau\u00df, M.: Some results for unification in distributive equational theories. Internal Report 7\/92, Fachbereich Informatik, J.W. Goethe-Universit\u00e4t Frankfurt, Frankfurt, Germany (1992)","key":"10_CR61"},{"unstructured":"Schmidt-Schau\u00df, M.: An algorithm for distributive unification. Internal Report 13\/94, Fachbereich Informatik, J.W. Goethe-Universit\u00e4t Frankfurt, Frankfurt, Germany (1994)","key":"10_CR62"},{"key":"10_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-61464-8_60","volume-title":"Rewriting Techniques and Applications","author":"M. Schmidt-Schau\u00df","year":"1996","unstructured":"Schmidt-Schau\u00df, M.: An algorithm for distributive unification. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol.\u00a01103, pp. 287\u2013301. Springer, Heidelberg (1996)"},{"key":"10_CR64","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/S0304-3975(98)00081-4","volume":"208","author":"M. Schmidt-Schau\u00df","year":"1998","unstructured":"Schmidt-Schau\u00df, M.: A decision algorithm for distributive unification. Theoretical Computer Science\u00a0208, 111\u2013148 (1998)","journal-title":"Theoretical Computer Science"},{"unstructured":"Schmidt-Schau\u00df, M.: Decidability of bounded second order unification. Technical Report Frank-report-11, FB Informatik, J.W. Goethe-Universit\u00e4t Frankfurt am Main (1999)","key":"10_CR65"},{"doi-asserted-by":"crossref","unstructured":"Schmidt-Schau\u00df, M.: Decidability of bounded second order unification (2001) (submitted for publication)","key":"10_CR66","DOI":"10.1007\/3-540-45793-3_35"},{"doi-asserted-by":"crossref","unstructured":"Schmidt-Schau\u00df, M.: A decision algorithm for stratified context unification. Journal of Logic and Computation (2001) (accepted for publication)","key":"10_CR67","DOI":"10.1007\/3-540-44802-0_35"},{"key":"10_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1007\/3-540-44802-0_35","volume-title":"Computer Science Logic","author":"M. Schmidt-Schau\u00df","year":"2001","unstructured":"Schmidt-Schau\u00df, M.: Stratified context unification is in PSPACE. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, p. 498. Springer, Heidelberg (2001) (to appear)"},{"key":"10_CR69","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.\u00a01379, pp. 61\u201375. Springer, Heidelberg (1998)"},{"doi-asserted-by":"crossref","unstructured":"Schmidt-Schau\u00df, M., Schulz, K.U.: Solvability of context equations with two context variables is decidable. Journal of Symbolic Computation (2000) (accepted for publication)","key":"10_CR70","DOI":"10.1007\/3-540-48660-7_5"},{"doi-asserted-by":"crossref","unstructured":"Schmidt-Schau\u00df, M., Schulz, K.U.: Decidability of bounded higher order unification. Frank report 15, Institut f\u00fcr Informatik (2001)","key":"10_CR71","DOI":"10.1007\/3-540-45793-3_35"},{"unstructured":"Schmidt-Schau\u00df, M., Stuber, J.: On the complexity of linear and stratified context matching problems. Frank-Report 14, Fachbere-ich Informatik, J.W. Goethe-Universit\u00e4t Frankfurt, Frankfurt, Germany (2001), available at http:\/\/www.ki.informatik.uni-frankfurt.de\/papers\/articles.html","key":"10_CR72"},{"key":"10_CR73","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R. Statman","year":"1979","unstructured":"Statman, R.: The typed \u03bb-calculus is not elementary recursive. Theoretical Computer Science\u00a09, 73\u201381 (1979)","journal-title":"Theoretical Computer Science"},{"unstructured":"Szab\u00f3, P.: Unifikationstheorie Erster Ordnung. Ph.D. thesis, Universit\u00e4t Karlsruhe (1982) (in German)","key":"10_CR74"},{"key":"10_CR75","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Functional Programming Languages and Computer Architecture","author":"D.A. Turner","year":"1985","unstructured":"Turner, D.A.: Miranda: A non-strict functional language with polymorphic types. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol.\u00a0201, pp. 1\u201316. Springer, Heidelberg (1985)"},{"key":"10_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"597","DOI":"10.1007\/BFb0055810","volume-title":"Mathematical Foundations of Computer Science 1998","author":"S. Vorobyov","year":"1998","unstructured":"Vorobyov, S.: \u2200\u2009\u2203\u2009\u2009\u2217\u2009-equational theory of context unification is $\\Pi_1^0$ -hard. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol.\u00a01450, pp. 597\u2013606. Springer, Heidelberg (1998)"},{"key":"10_CR77","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-48660-7_6","volume-title":"Automated Deduction - CADE-16","author":"T. Wierzbicki","year":"1999","unstructured":"Wierzbicki, T.: Complexity of the higher-order matching. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 82\u201396. Springer, Heidelberg (1999)"},{"key":"10_CR78","series-title":"Cambridge tracts in theoretical computer science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569906","volume-title":"The clausal theories of types","author":"D.A. Wolfram","year":"1993","unstructured":"Wolfram, D.A.: The clausal theories of types. Cambridge tracts in theoretical computer science, vol.\u00a021. Cambridge University Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Mechanizing Mathematical Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32254-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,27]],"date-time":"2024-03-27T19:19:27Z","timestamp":1711567167000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32254-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540250517","9783540322542"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32254-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}