{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:28Z","timestamp":1725494308097},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_5","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T15:53:07Z","timestamp":1194623587000},"page":"67-81","source":"Crossref","is-referenced-by-count":11,"title":["Solvability of Context Equations with Two Context Variables Is Decidable"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus U.","family":"Schulz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"key":"5_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. to appear in JSC."},{"key":"5_CR2","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/S0304-3975(06)80003-4","volume":"87","author":"W. Farmer","year":"1991","unstructured":"W. Farmer. Simple second-order languages for which unification is undecidable. Theoretical Computer Science, 87:173\u2013214, 1991.","journal-title":"Theoretical Computer Science"},{"key":"5_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-49366-2_2","volume-title":"Advances in Computing Science-ASIAN\u201998","author":"H. Ganzinger","year":"1998","unstructured":"H. Ganzinger, F. Jacquemard, and M. Veanes. Rigid reachability. In J. Hsiang and A. Ohori, editors, Advances in Computing Science-ASIAN\u201998, Springer LNCS 1538, pages 4\u201321, 1998."},{"key":"5_CR4","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. Goldfarb","year":"1981","unstructured":"W. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13:225\u2013230, 1981.","journal-title":"Theoretical Computer Science"},{"key":"5_CR5","doi-asserted-by":"crossref","first-page":"670","DOI":"10.1145\/234533.234543","volume":"43","author":"A. Ko\u015bcielski","year":"1996","unstructured":"A. Ko\u015bcielski and L. Pacholski. Complexity of Makanin\u2019s algorithms. Journal of the Association for Computing Machinery, 43:670\u2013684, 1996.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"5_CR6","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 Int. Conf. on Rewriting Techniques and Applications","author":"J. Levy","year":"1996","unstructured":"J. Levy. Linear second order unification. In Proc. of the 7th Int. Conf. on Rewriting Techniques and Applications, Springer LNCS 1103, pages 332\u2013346, 1996."},{"key":"5_CR7","unstructured":"J. Levy and M. Veanes. On the undecidability of second-order unification. Submitted to Information and Computation, 1999."},{"issue":"2","key":"5_CR8","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"G. Makanin","year":"1977","unstructured":"G. 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":"5_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/3-540-62950-5_75","volume-title":"International Conference on Rewriting Techniques and Applications","author":"J. Marcinkowski","year":"1997","unstructured":"J. Marcinkowski. Undecidability of the first order theory of one-step right ground rewriting. In H. Comon, editor, International Conference on Rewriting Techniques and Applications, Springer LNCS 1232, pages 241\u2013253, 1997."},{"key":"5_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/3-540-63104-6_4","volume-title":"Proc. of the Int. Conf. on Automated Deduction","author":"J. Niehren","year":"1997","unstructured":"J. Niehren, M. Pinkal, and P. Ruhrberg. On equality up-to constraints over finite trees, context unification, and one-step rewriting. In Proc. of the Int. Conf. on Automated Deduction, Springer LNCS 1249, pages 34\u201348, 1997."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"J. Niehren, M. Pinkal, and P. Ruhrberg. A uniform approach to underspecification and parallelism. Technical Report, 1997.","DOI":"10.3115\/979617.979670"},{"key":"5_CR12","unstructured":"J. Niehren, S. Tison, and R. Treinen. On stratified context unification and rewriting constraints. Talk at CCL\u201998 Workshop, 1998."},{"key":"5_CR13","series-title":"Internal Report","volume-title":"Fachb. Informatik","author":"M. Schmidt-Schau\u00df","year":"1994","unstructured":"M. Schmidt-Schau\u00df. Unification of stratified second-order terms. Internal Report 12\/94, Fachb. Informatik, J.W. Goethe-Universit\u00e4t Frankfurt, Germany, 1994."},{"key":"5_CR14","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":"M. Schmidt-Schau\u00df. An algorithm for distributive unification. Theoretical Computer Science, 208:111\u2013148, 1998.","journal-title":"Theoretical Computer Science"},{"key":"5_CR15","volume-title":"Draft, Fachbereich Informatik","author":"M. Schmidt-Schau\u00df","year":"1998","unstructured":"M. Schmidt-Schau\u00df. Decidability of bounded second order unification. Draft, Fachbereich Informatik, J.W. Goethe-Universit\u00e4t Frankfurt, Germany, 1998."},{"key":"5_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/BFb0052361","volume-title":"Rewriting Techniques and Applications, Proc. RTA\u201998","author":"M. Schmidt-Schau\u00df","year":"1998","unstructured":"M. Schmidt-Schau\u00df and K. U. Schulz. On the exponent of periodicity of minimal solutions of context equations. In Rewriting Techniques and Applications, Proc. RTA\u201998, volume 1379 of LNCS, pages 61\u201375. Springer-Verlag, 1998."},{"key":"5_CR17","series-title":"CIS-Report","volume-title":"Solvability of context equations with two context variables is decidable","author":"M. Schmidt-Schau\u00df","year":"1999","unstructured":"M. Schmidt-Schau\u00df and K. U. Schulz. Solvability of context equations with two context variables is decidable. CIS-Report 98-114, CIS, University of Munich, Germany, 1999. available under ftp:\/\/ftp.cis.uni-muenchen.de\/pub\/cis-berichte\/CIS-Bericht-98-114.ps ."},{"key":"5_CR18","series-title":"Lect Notes Comput Sci","first-page":"85","volume-title":"Proc. of IWWERT 1990","author":"K. U. Schulz","year":"1990","unstructured":"K. U. Schulz. Makanin\u2019s algorithm-two improvements and a generalization. In Proc. of IWWERT 1990, Springer LNCS 572, pages 85\u2013150, 1990."},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"K. U. Schulz. Word unification and transformation of generalized equations. J. Automated Reasoning, pages 149\u2013184, 1993.","DOI":"10.1007\/BF00881904"},{"key":"5_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/3-540-61464-8_59","volume-title":"7th International Conference on Rewriting Techniques and Applications","author":"R. Treinen","year":"1996","unstructured":"R. Treinen. The first-order theory of one-step rewriting is undecidable. In H. Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, Springer LNCS 1103, pages 276\u2013286,Rutgers University, NJ, USA, 1996."},{"key":"5_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"254","DOI":"10.1007\/3-540-62950-5_76","volume-title":"International Conference on Rewriting Techniques and Applications","author":"S. Vorobyov","year":"1997","unstructured":"S. Vorobyov. The first-order theory of one step rewriting in linear noetherian systems is undecidable. In H. Comon, editor, International Conference on Rewriting Techniques and Applications, Springer LNCS 1232, pages 254\u2013268, 1997."},{"key":"5_CR22","unstructured":"S. Vorobyov. The 898-equational theory of context unification is co-recursively enumerable hard. Talk at CCL\u201998 Workshop, 1998."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T04:56:24Z","timestamp":1556945784000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_5","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}