{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T11:40:12Z","timestamp":1737632412844,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540653882"},{"type":"electronic","value":"9783540493662"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49366-2_2","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T18:48:47Z","timestamp":1194979727000},"page":"4-21","source":"Crossref","is-referenced-by-count":0,"title":["Rigid Reachability"],"prefix":"10.1007","author":[{"given":"Harald","family":"Ganzinger","sequence":"first","affiliation":[]},{"given":"Florent","family":"Jacquemard","sequence":"additional","affiliation":[]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1998,11,30]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"2_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/3-540-53414-8_34","volume-title":"Proc. of the 6th International Meeting of Young Computer Scientists","author":"J.-L. Coquid\u00e9","year":"1990","unstructured":"J.-L. Coquid\u00e9 and R. Gilleron. Proofs and reachability problem for ground rewrite systems. In Proc. of the 6th International Meeting of Young Computer Scientists, volume 464 of LNCS, pages 120\u2013129, 1990."},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)90101-5","volume":"127","author":"J.L. Coquid\u00e9","year":"1994","unstructured":"J.L. Coquid\u00e9, M. Dauchet, R. Gilleron, and S. V\u00e1gv\u00f6lgyi. Bottom-up tree pushdown automata: classification and connection with rewrite systems. Theoretical Computer Science, 127:69\u201398, 1994.","journal-title":"Theoretical Computer Science"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"V. Cortier. PSPACE-completeness of monadic simultaneous rigid reachability. Unpublished manuscript, july 1998.","DOI":"10.1007\/3-540-48523-6_22"},{"key":"2_CR5","series-title":"Lect Notes Comput Sci","first-page":"95","volume-title":"Term Rewriting (French Spring School of Theoretical Computer Science)","author":"M. Dauchet","year":"1993","unstructured":"M. Dauchet. Rewriting and tree automata. In H. Comon and J.P. Jouannaud, editors, Term Rewriting (French Spring School of Theoretical Computer Science), volume 909 of Lecture Notes in Computer Science, pages 95\u2013113. Springer Verlag, Font Romeux, France, 1993."},{"key":"2_CR6","unstructured":"Max Dauchet, Thierry Heuillard, Pierre Lescanne, and Sophie Tison. The confluence of ground term rewriting systems is decidable. In Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, 1988."},{"key":"2_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/BFb0052370","volume-title":"Rewriting Techniques and Applications","author":"A. Degtyarev","year":"1998","unstructured":"A. Degtyarev, Yu. Gurevich, P. Narendran, M. Veanes, and A. Voronkov. The decidability of simultaneous rigid E-unification with one variable. In T. Nipkow, editor, Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 181\u2013195. Springer Verlag, 1998."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. UPMAIL Technical Report 105, Uppsala University, Computing Science Department, May 1995.","DOI":"10.1007\/3-540-61377-3_38"},{"key":"2_CR9","series-title":"Formal Methods and Semantics","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"D. N","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics, chapter 6, pages 243\u2013309. North Holland, Amsterdam, 1990."},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1016\/S0022-0000(70)80041-1","volume":"4","author":"J. Doner","year":"1970","unstructured":"J. Doner. Tree acceptors and some of their applications. Journal of Computer and System Sciences, 4:406\u2013451, 1970.","journal-title":"Journal of Computer and System Sciences"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/S0304-3975(06)80003-4","volume":"87","author":"W.M. Farmer","year":"1991","unstructured":"W.M. Farmer. Simple second-order languages for which unification is undecidable. Theoretical Computer Science, 87:25\u201341, 1991.","journal-title":"Theoretical Computer Science"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Thom Fr\u00fchwirth, Ehud Shapiro, Moshe Y.Vardi, and Eyal Yardemi. Logic programs as types for logic programs. In 6th IEEE Symp. Logic In Computer Science, pages 300\u2013309, 1991.","DOI":"10.1109\/LICS.1991.151654"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"J.H. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification is NP-complete. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 338\u2013346. IEEE Computer Society Press, July 1988.","DOI":"10.1109\/LICS.1988.5121"},{"key":"2_CR14","unstructured":"J.H. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification: Equational matings. In Proc. IEEE Conference on Logic in Computer Science (LICS), pages 338\u2013346. IEEE Computer Society Press, 1987."},{"key":"2_CR15","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":"2_CR16","doi-asserted-by":"crossref","unstructured":"Y. Gurevich and M. Veanes. Partisan corroboration, and shifted pairing. Research Report MPI-I-98-2-014, Max-Planck-Institut f\u00fcr Informatik, September 1998.","DOI":"10.1006\/inco.1999.2797"},{"key":"2_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/3-540-63165-8_173","volume-title":"Automata, Languages and Programming, 24th International Colloquium, ICALP\u201997","author":"Y. Gurevich","year":"1997","unstructured":"Y. Gurevich and A. Voronkov. Monadic simultaneous rigid E-unification and related problems. In P. Degano, R. Corrieri, and A. Marchetti-Spaccamella, editors, Automata, Languages and Programming, 24th International Colloquium, ICALP\u201997, volume 1256 of Lecture Notes in Computer Science, pages 154\u2013165. Springer Verlag, 1997."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"D. Kozen. Complexity of finitely presented algebras. In Proc. 9th STOC, pages 164\u2013177, 1977.","DOI":"10.1145\/800105.803406"},{"key":"2_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/BFb0052360","volume-title":"Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March\/April 1998, Proceedings","author":"J. Levy","year":"1998","unstructured":"J. Levy. Decidable and undecidable second-order unification problems. In T. Nipkow, editor, Rewriting Techniques and Applications, 9th International Conference, RTA-98, Tsukuba, Japan, March\/April 1998, Proceedings, volume 1379 of Lecture Notes in Computer Science, pages 47\u201360. Springer Verlag, 1998."},{"key":"2_CR20","unstructured":"J. Levy and M. Veanes. On the undecidability of second-order unification. Submitted to Information and Computation, 1998."},{"key":"2_CR21","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0020-0190(94)00130-8","volume":"52","author":"H. Seidl","year":"1994","unstructured":"Helmut Seidl. Haskell overloading is dexptime-complete. Inf. Process. Letters, 52:57\u201360, 1994.","journal-title":"Inf. Process. Letters"},{"issue":"1","key":"2_CR22","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/BF01691346","volume":"2","author":"J.W. Thatcher","year":"1968","unstructured":"J.W. Thatcher and J.B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1):57\u201381, 1968.","journal-title":"Mathematical Systems Theory"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"M. Veanes. The relation between second-order unification and simultaneous rigid E-unification. In Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science, June 21\u201324, 1998, Indianapolis, Indiana (LICS\u201998), pages 264\u2013275. IEEE Computer Society Press, 1998.","DOI":"10.1109\/LICS.1998.705663"},{"key":"2_CR24","unstructured":"Margus Veanes. On computational complexity of basic decision problems of finite tree automata. Technical Report 133, Computing Science Department, Uppsala University, 1997."}],"container-title":["Lecture Notes in Computer Science","Advances in Computing Science ASIAN 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49366-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,22]],"date-time":"2025-01-22T08:02:24Z","timestamp":1737532944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49366-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540653882","9783540493662"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-49366-2_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}