{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:19Z","timestamp":1760202679403},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662439500"},{"type":"electronic","value":"9783662439517"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43951-7_21","type":"book-chapter","created":{"date-parts":[[2014,6,11]],"date-time":"2014-06-11T08:37:49Z","timestamp":1402475869000},"page":"244-255","source":"Crossref","is-referenced-by-count":9,"title":["Context Unification is in PSPACE"],"prefix":"10.1007","author":[{"given":"Artur","family":"Je\u017c","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"21_CR1","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.\u00a025(4), 397\u2013419 (1998)","journal-title":"J. Symb. Comput."},{"issue":"4","key":"21_CR2","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. Symb. Comput.\u00a025(4), 421\u2013453 (1998)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"21_CR3","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/j.jsc.2008.10.005","volume":"45","author":"A. Gasc\u00f3n","year":"2010","unstructured":"Gasc\u00f3n, A., Godoy, G., Schmidt-Schau\u00df, M., Tiwari, A.: Context unification with one context variable. J. Symb. Comput.\u00a045(2), 173\u2013193 (2010)","journal-title":"J. Symb. Comput."},{"key":"21_CR4","series-title":"LIPIcs","first-page":"233","volume-title":"STACS","author":"A. Je\u017c","year":"2013","unstructured":"Je\u017c, A.: Recompression: a simple and powerful technique for word equations. In: Portier, N., Wilke, T. (eds.) STACS. LIPIcs, vol.\u00a020, pp. 233\u2013244. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl (2013)"},{"key":"21_CR5","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.\u00a01103, pp. 332\u2013346. Springer, Heidelberg (1996)"},{"issue":"6","key":"21_CR6","doi-asserted-by":"publisher","first-page":"763","DOI":"10.1093\/jigpal\/jzq010","volume":"19","author":"J. Levy","year":"2011","unstructured":"Levy, J., Schmidt-Schau\u00df, M., Villaret, M.: On the complexity of bounded second-order unification and stratified context unification. Logic Journal of the IGPL\u00a019(6), 763\u2013789 (2011)","journal-title":"Logic Journal of the IGPL"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/3-540-45610-4_23","volume-title":"Rewriting Techniques and Applications","author":"J. Levy","year":"2002","unstructured":"Levy, J., Villaret, M.: Currying second-order unification problems. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 326\u2013339. Springer, Heidelberg (2002)"},{"issue":"3","key":"21_CR8","first-page":"483","volume":"51","author":"W. Plandowski","year":"2004","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J.\u00a0ACM\u00a051(3), 483\u2013496 (2004)","journal-title":"J.\u00a0ACM"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"731","DOI":"10.1007\/BFb0055097","volume-title":"Automata, Languages and Programming","author":"W. Plandowski","year":"1998","unstructured":"Plandowski, W., Rytter, W.: Application of lempel-ziv encodings to the solution of word equations. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 731\u2013742. Springer, Heidelberg (1998)"},{"key":"21_CR10","unstructured":"Schmidt-Schau\u00df, M.: Unification of stratified second-order terms, internal Report 12\/94, Johann-Wolfgang-Goethe-Universit\u00e4t (1994)"},{"issue":"6","key":"21_CR11","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.\u00a012(6), 929\u2013953 (2002)","journal-title":"J. Log. Comput."},{"key":"21_CR12","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)"},{"issue":"1","key":"21_CR13","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.\u00a033(1), 77\u2013122 (2002)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"21_CR14","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.\u00a040(2), 905\u2013954 (2005)","journal-title":"J. Symb. Comput."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43951-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T02:32:41Z","timestamp":1558924361000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43951-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662439500","9783662439517"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43951-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}