{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:57:10Z","timestamp":1726037830850},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030248857"},{"type":"electronic","value":"9783030248864"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-24886-4_2","type":"book-chapter","created":{"date-parts":[[2019,7,23]],"date-time":"2019-07-23T19:02:56Z","timestamp":1563908576000},"page":"18-40","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Deciding Context Unification (with Regular Constraints)"],"prefix":"10.1007","author":[{"given":"Artur","family":"Je\u017c","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,10]]},"reference":[{"issue":"4","key":"2_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. 25(4), 397\u2013419 (1998). \n                      https:\/\/doi.org\/10.1006\/jsco.1997.0185","journal-title":"J. Symb. Comput."},{"issue":"4","key":"2_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. 25(4), 421\u2013453 (1998). \n                      https:\/\/doi.org\/10.1006\/jsco.1997.0186","journal-title":"J. Symb. Comput."},{"issue":"2","key":"2_CR3","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.ic.2005.04.002","volume":"202","author":"V Diekert","year":"2005","unstructured":"Diekert, V., Guti\u00e9rrez, C., Hagenah, C.: The existential theory of equations with rational constraints in free groups is PSPACE-complete. Inf. Comput. 202(2), 105\u2013140 (2005). \n                      https:\/\/doi.org\/10.1016\/j.ic.2005.04.002","journal-title":"Inf. Comput."},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1016\/j.ic.2016.09.009","volume":"251","author":"V Diekert","year":"2016","unstructured":"Diekert, V., Je\u017c, A., Plandowski, W.: Finding all solutions of equations in free groups and monoids with involution. Inf. Comput. 251, 263\u2013286 (2016). \n                      https:\/\/doi.org\/10.1016\/j.ic.2016.09.009","journal-title":"Inf. Comput."},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Fr\u00fchwirth, T.W., Shapiro, E.Y., Vardi, M.Y., Yardeni, E.: Logic programs as types for logic programs. In: LICS, pp. 300\u2013309. IEEE Computer Society (1991). \n                      https:\/\/doi.org\/10.1109\/LICS.1991.151654","DOI":"10.1109\/LICS.1991.151654"},{"issue":"2","key":"2_CR6","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. 45(2), 173\u2013193 (2010). \n                      https:\/\/doi.org\/10.1016\/j.jsc.2008.10.005","journal-title":"J. Symb. Comput."},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Gasc\u00f3n, A., Schmidt-Schau\u00df, M., Tiwari, A.: Two-restricted one context unification is in polynomial time. In: Kreutzer, S. (ed.) CSL. LIPIcs, vol. 41, pp. 405\u2013422. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik (2015). \n                      https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2015.405","DOI":"10.4230\/LIPIcs.CSL.2015.405"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Gasc\u00f3n, A., Tiwari, A., Schmidt-Schau\u00df, M.: One context unification problems solvable in polynomial time. In: LICS, pp. 499\u2013510. IEEE (2015). \n                      https:\/\/doi.org\/10.1109\/LICS.2015.53","DOI":"10.1109\/LICS.2015.53"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"WD Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13, 225\u2013230 (1981). \n                      https:\/\/doi.org\/10.1016\/0304-3975(81)90040-2","journal-title":"Theor. Comput. Sci."},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-662-43951-7_21","volume-title":"Automata, Languages, and Programming","author":"A Je\u017c","year":"2014","unstructured":"Je\u017c, A.: Context unification is in PSPACE. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014. LNCS, vol. 8573, pp. 244\u2013255. Springer, Heidelberg (2014). \n                      https:\/\/doi.org\/10.1007\/978-3-662-43951-7_21\n                      \n                    . Full version \n                      http:\/\/arxiv.org\/abs\/1310.4367"},{"issue":"1","key":"2_CR11","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/2743014","volume":"63","author":"A Je\u017c","year":"2016","unstructured":"Je\u017c, A.: Recompression: a simple and powerful technique for word equations. J. ACM 63(1), 4:1 (2016). \n                      https:\/\/doi.org\/10.1145\/2743014","journal-title":"J. ACM"},{"key":"2_CR12","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. 1103, pp. 332\u2013346. Springer, Heidelberg (1996). \n                      https:\/\/doi.org\/10.1007\/3-540-61464-8_63"},{"issue":"3","key":"2_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1006\/jsco.1996.0053","volume":"22","author":"J Levy","year":"1996","unstructured":"Levy, J., Agust\u00ed-Cullell, J.: Bi-rewrite systems. J. Symb. Comput. 22(3), 279\u2013314 (1996). \n                      https:\/\/doi.org\/10.1006\/jsco.1996.0053","journal-title":"J. Symb. Comput."},{"issue":"3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"1113","DOI":"10.1137\/050645403","volume":"38","author":"J Levy","year":"2008","unstructured":"Levy, J., Schmidt-Schau\u00df, M., Villaret, M.: The complexity of monadic second-order unification. SIAM J. Comput. 38(3), 1113\u20131140 (2008). \n                      https:\/\/doi.org\/10.1137\/050645403","journal-title":"SIAM J. Comput."},{"issue":"6","key":"2_CR15","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. Log. J. IGPL 19(6), 763\u2013789 (2011). \n                      https:\/\/doi.org\/10.1093\/jigpal\/jzq010","journal-title":"Log. J. IGPL"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/10721975_11","volume-title":"Rewriting Techniques and Applications","author":"J Levy","year":"2000","unstructured":"Levy, J., Villaret, M.: Linear second-order unification and context unification with tree-regular constraints. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833, pp. 156\u2013171. Springer, Heidelberg (2000). \n                      https:\/\/doi.org\/10.1007\/10721975_11"},{"key":"2_CR17","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. 2378, pp. 326\u2013339. Springer, Heidelberg (2002). \n                      https:\/\/doi.org\/10.1007\/3-540-45610-4_23"},{"issue":"103","key":"2_CR18","first-page":"147","volume":"2","author":"G Makanin","year":"1977","unstructured":"Makanin, G.: The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik 2(103), 147\u2013236 (1977). (in Russian)","journal-title":"Matematicheskii Sbornik"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/3-540-62950-5_75","volume-title":"Rewriting Techniques and Applications","author":"J Marcinkowski","year":"1997","unstructured":"Marcinkowski, J.: Undecidability of the first order theory of one-step right ground rewriting. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 241\u2013253. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/3-540-62950-5_75"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/3-540-63104-6_4","volume-title":"Automated Deduction\u2014CADE-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. 1249, pp. 34\u201348. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/3-540-63104-6_4"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Niehren, J., Pinkal, M., Ruhrberg, P.: A uniform approach to underspecification and parallelism. In: Cohen, P.R., Wahlster, W. (eds.) ACL, pp. 410\u2013417. Morgan Kaufmann Publishers\/ACL (1997). \n                      https:\/\/doi.org\/10.3115\/979617.979670","DOI":"10.3115\/979617.979670"},{"issue":"3","key":"2_CR22","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/990308.990312","volume":"51","author":"W Plandowski","year":"2004","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J. ACM 51(3), 483\u2013496 (2004). \n                      https:\/\/doi.org\/10.1145\/990308.990312","journal-title":"J. ACM"},{"key":"2_CR23","unstructured":"RTA Problem List: Problem 90 (1990). \n                      http:\/\/rtaloop.mancoosi.univ-paris-diderot.fr\/problems\/90.html"},{"key":"2_CR24","unstructured":"Schmidt-Schau\u00df, M.: Unification of stratified second-order terms. Internal Report 12\/94, Johann-Wolfgang-Goethe-Universit\u00e4t (1994)"},{"issue":"1\u20132","key":"2_CR25","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. Theor. Comput. Sci. 208(1\u20132), 111\u2013148 (1998). \n                      https:\/\/doi.org\/10.1016\/S0304-3975(98)00081-4","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"2_CR26","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. 12(6), 929\u2013953 (2002). \n                      https:\/\/doi.org\/10.1093\/logcom\/12.6.929","journal-title":"J. Log. Comput."},{"issue":"2","key":"2_CR27","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/j.ic.2003.08.002","volume":"188","author":"M Schmidt-Schau\u00df","year":"2004","unstructured":"Schmidt-Schau\u00df, M.: Decidability of bounded second order unification. Inf. Comput. 188(2), 143\u2013178 (2004). \n                      https:\/\/doi.org\/10.1016\/j.ic.2003.08.002","journal-title":"Inf. Comput."},{"key":"2_CR28","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. 1379, pp. 61\u201375. Springer, Heidelberg (1998). \n                      https:\/\/doi.org\/10.1007\/BFb0052361"},{"issue":"1","key":"2_CR29","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. 33(1), 77\u2013122 (2002). \n                      https:\/\/doi.org\/10.1006\/jsco.2001.0438","journal-title":"J. Symb. Comput."},{"issue":"2","key":"2_CR30","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. 40(2), 905\u2013954 (2005). \n                      https:\/\/doi.org\/10.1016\/j.jsc.2005.01.005","journal-title":"J. Symb. Comput."},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-55124-7_4","volume-title":"Word Equations and Related Topics","author":"KU Schulz","year":"1992","unstructured":"Schulz, K.U.: Makanin\u2019s algorithm for word equations-two improvements and a generalization. In: Schulz, K.U. (ed.) IWWERT 1990. LNCS, vol. 572, pp. 85\u2013150. Springer, Heidelberg (1992). \n                      https:\/\/doi.org\/10.1007\/3-540-55124-7_4"},{"issue":"1\u20132","key":"2_CR32","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/S0304-3975(98)00083-8","volume":"208","author":"R Treinen","year":"1998","unstructured":"Treinen, R.: The first-order theory of linear one-step rewriting is undecidable. Theor. Comput. Sci. 208(1\u20132), 179\u2013190 (1998). \n                      https:\/\/doi.org\/10.1016\/S0304-3975(98)00083-8","journal-title":"Theor. Comput. Sci."},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/3-540-62950-5_76","volume-title":"Rewriting Techniques and Applications","author":"S Vorobyov","year":"1997","unstructured":"Vorobyov, S.: The first-order theory of one step rewriting in linear Noetherian systems is undecidable. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 254\u2013268. Springer, Heidelberg (1997). \n                      https:\/\/doi.org\/10.1007\/3-540-62950-5_76"},{"key":"2_CR34","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.: \n                      \n                        \n                      \n                      $$\\forall \\exists $$\n                    *-Equational theory of context unification is \n                      \n                        \n                      \n                      $$\\varPi $$\n                    \n                      \n                        \n                      \n                      $${}_{1}^{0}$$\n                    -hard. In: Brim, L., Gruska, J., Zlatu\u0161ka, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 597\u2013606. Springer, Heidelberg (1998). \n                      https:\/\/doi.org\/10.1007\/BFb0055810"}],"container-title":["Lecture Notes in Computer Science","Developments in Language Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24886-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,23]],"date-time":"2019-07-23T19:03:34Z","timestamp":1563908614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24886-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030248857","9783030248864"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24886-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"10 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"DLT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Developments in Language Theory","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Warsaw","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"dlt2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/dlt2019.mimuw.edu.pl\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}