{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,22]],"date-time":"2026-08-22T08:03:46Z","timestamp":1787385826150,"version":"build-2736575974"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425540","type":"print"},{"value":"9783540448020","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_35","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T04:15:38Z","timestamp":1180671338000},"page":"498-513","source":"Crossref","is-referenced-by-count":4,"title":["Stratified Context Unification Is in PSPACE"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"35_CR1","unstructured":"H. Comon. Completion of rewrite systems with membership constraints, part I: Deduction rules and part II: Constraint solving. Technical report, CNRS and LRI, Universit\u00e9 de Paris Sud, 1993."},{"issue":"4","key":"35_CR2","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1006\/jsco.1997.0185","volume":"25","author":"H. Comon","year":"1998","unstructured":"H. Comon. Completion of rewrite systems with membership constraints. Part I: Deduction rules. J. Symbolic Computation, 25(4):397\u2013419, 1998.","journal-title":"J. Symbolic Computation"},{"issue":"4","key":"35_CR3","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1006\/jsco.1997.0186","volume":"25","author":"H. Comon","year":"1998","unstructured":"H. Comon. Completion of rewrite systems with membership constraints. Part II: Constraint solving. J. Symbolic Computation, 25(4):421\u2013453, 1998.","journal-title":"J. Symbolic Computation"},{"key":"35_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/10721975_8","volume-title":"Proc. of the 11th RTA","author":"K. Erk","year":"2000","unstructured":"Katrin Erk and Joachim Niehren. Parallelism constraints. In Proc. of the 11th RTA, volume 1833 of LNCS, pages 110\u2013126, 2000."},{"key":"35_CR5","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/S0304-3975(06)80003-4","volume":"87","author":"W.A. Farmer","year":"1991","unstructured":"W.A. Farmer. Simple second-order languages for which unification is unde-cidable. J. Theoretical Computer Science, 87:173\u2013214, 1991.","journal-title":"J. Theoretical Computer Science"},{"key":"35_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":"35_CR7","doi-asserted-by":"crossref","unstructured":"C. Gutierrez. Satisfiability of word equations with constants is in exponential space. In Proc. FOCS\u201998, pages 112\u2013119, Palo Alto, California, 1998. IEEE Computer Society Press.","DOI":"10.1109\/SFCS.1998.743434"},{"key":"35_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Gerard Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"35_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-61464-8_63","volume-title":"Proc. of the 7th RTA","author":"J. Levy","year":"1996","unstructured":"Jordi Levy. Linear second order unification. In Proc. of the 7th RTA, volume 1103 of LNCS, pages 332\u2013346, 1996."},{"key":"35_CR10","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1006\/inco.2000.2877","volume":"159","author":"J. Levy","year":"2000","unstructured":"Jordi Levy and Margus Veanes. On the undecidability of second-order unification. Information and Computation, 159:125\u2013150, 2000.","journal-title":"Information and Computation"},{"key":"35_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/10721975_11","volume-title":"Proc. of the 11th RTA","author":"J. Levy","year":"2000","unstructured":"Jordi Levy and Mateu Villaret. Linear second-order unification and context unification with tree-regular constraints. In Proc. of the 11th RTA, volume 1833 of LNCS, pages 156\u2013171, 2000."},{"issue":"2","key":"35_CR12","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"},{"key":"35_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/3-540-63104-6_4","volume-title":"CADE\u2019 97","author":"J. Niehren","year":"1997","unstructured":"Joachim Niehren, Manfred Pinkal, and P. Ruhrberg. On equality up-to constraints over finite trees, context unification, and one-step rewriting. In CADE\u2019 97, volume 1249 of LNCS, pages 34\u201348, 1997."},{"key":"35_CR14","doi-asserted-by":"crossref","unstructured":"Joachim Niehren, Manfred Pinkal, and Peter Ruhrberg. A uniform approach to underspecification and parallelism. In Proc. of the 35th Annual Meeting of the Ass. of Computational Linguistics, pages 410\u2013417, Madrid, Spain, 1997.","DOI":"10.3115\/976909.979670"},{"key":"35_CR15","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0020-0190(00)00036-3","volume":"74","author":"J. Niehren","year":"2000","unstructured":"Joachim Niehren, Sophie Tison, and Ralf Treinen. On rewrite constraints and context unification. Information Processing Letters, 74:35\u201340, 2000.","journal-title":"Information Processing Letters"},{"key":"35_CR16","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 type theory. J. ACM, 20:333\u2013364, 1973.","journal-title":"J. ACM"},{"key":"35_CR17","doi-asserted-by":"crossref","unstructured":"W. Plandowski. Satisfiability of word equations with constants is in NEX-PTIME. In T. Leighton, editor, Proc. STOC\u201999, pages 721\u2013725, Atlanta, Georgia, 1999. ACM Press.","DOI":"10.1145\/301250.301443"},{"key":"35_CR18","doi-asserted-by":"crossref","unstructured":"W. Plandowski. Satisfiability of word equations with constants is in PSPACE. In FOCS 99, pages 495\u2013500, 1999.","DOI":"10.1145\/301250.301443"},{"key":"35_CR19","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0747-7171(89)80023-9","volume":"8","author":"W. Snyder","year":"1989","unstructured":"Wayne Snyder and Jean Gallier. Higher-order unification revisited: Complete sets of transformations. J. Symbolic Computation, 8:101\u2013140, 1989.","journal-title":"J. Symbolic Computation"},{"key":"35_CR20","volume-title":"Internal Report 12\/94","author":"M. Schmidt-Schau\u00df","year":"1994","unstructured":"Manfred Schmidt-Schau\u00df. Unification of stratified second-order terms. Internal Report 12\/94, Fachbereich Informatik, J.W. Goethe-Universit\u00e4t Frankfurt, Frankfurt, Germany, 1994."},{"key":"35_CR21","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":"Manfred Schmidt-Schau\u00df. A decision algorithm for distributive unification. TCS, 208:111\u2013148, 1998.","journal-title":"TCS"},{"key":"35_CR22","unstructured":"Manfred Schmidt-Schau\u00df. Decidability of bounded second order unification. Technical Report Frank-report-11, FB Informatik, J.W. Goethe-Universit\u00e4t Frankfurt am Main, 1999. submitted for publication."},{"key":"35_CR23","volume-title":"Frank-Report 12","author":"M. Schmidt-Schau\u00df","year":"1999","unstructured":"Manfred Schmidt-Schau\u00df. A decision algorithm for stratified context unification. Frank-Report 12, Fachbereich Informatik, J.W. Goethe-Universit\u00e4t Frankfurt, Frankfurt, Germany, 1999. accepted for publication in Journal of Logic and Computation, preliminary version available at http:\/\/www.ki.informatik.uni-frankfurt.de\/papers\/articles.html."},{"key":"35_CR24","unstructured":"Manfred Schmidt-Schau\u00df. An optimized decision algorithm for stratified context unification. Technical Report Frank-report-13, FB Informatik, J.W. Goethe-Universit\u00e4t Frankfurt am Main, 1999."},{"key":"35_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BFb0052361","volume-title":"Proc. of the 9th RTA","author":"M. Schmidt-Schau\u00df","year":"1998","unstructured":"Manfred Schmidt-Schau\u00df and Klaus U. Schulz. On the exponent of periodicity of minimal solutions of context equations. In Proc. of the 9th RTA, volume 1379 of LNCS, pages 61\u201375, 1998."},{"key":"35_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-48660-7_5","volume-title":"Proc. of the Int. Conf. on Automated Deduction","author":"M. Schmidt-Schau\u00df","year":"1999","unstructured":"Manfred Schmidt-Schau\u00df and Klaus U. Schulz. Solvability of context equations with two context variables is decidable. In Proc. of the Int. Conf. on Automated Deduction, volume 1632 of LNCS, pages 67\u201381, 1999."},{"key":"35_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1007\/BFb0055810","volume-title":"MFCS 1998","author":"S. Vorobyov","year":"1998","unstructured":"Sergei Vorobyov. V3*-equational theory of context unification is \u03c0\u21341-hard. In MFCS 1998, volume 1450 of LNCS, pages 597\u2013606. Springer-Verlag, 1998."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:02:24Z","timestamp":1737061344000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_35","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}