{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T06:40:04Z","timestamp":1736577604190,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814771_8","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"82-96","source":"Crossref","is-referenced-by-count":5,"title":["Stratified Context Unification Is NP-Complete"],"prefix":"10.1007","author":[{"given":"Jordi","family":"Levy","sequence":"first","affiliation":[]},{"given":"Manfred","family":"Schmidt-Schau\u00df","sequence":"additional","affiliation":[]},{"given":"Mateu","family":"Villaret","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","volume-title":"An introduction to mathematical logic and type theory: to truth through proof","author":"P. Andrews","year":"1986","unstructured":"Andrews, P.: An introduction to mathematical logic and type theory: to truth through proof. Academic Press, London (1986)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/11601524_13","volume-title":"Database Programming Languages","author":"G. Busatto","year":"2005","unstructured":"Busatto, G., Lohrey, M., Maneth, S.: Efficient memory representation of XML documents. In: Bierman, G., Koch, C. (eds.) DBPL 2005. LNCS, vol.\u00a03774, pp. 199\u2013216. Springer, Heidelberg (2005)"},{"key":"8_CR3","unstructured":"Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (1997) (release, October 1, 2002), available on http:\/\/www.grappa.univ-lille3.fr\/tata"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"1009","DOI":"10.1016\/B978-044450813-3\/50018-7","volume-title":"Handbook of Automated Reasoning, ch. 16","author":"G. Dowek","year":"2001","unstructured":"Dowek, G.: Higher-order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 16, vol.\u00a0II, pp. 1009\u20131062. Elsevier Science, Amsterdam (2001)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/10721975_8","volume-title":"Rewriting Techniques and Applications","author":"K. Erk","year":"2000","unstructured":"Erk, K., Niehren, J.: Parallelism constraints. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol.\u00a01833, pp. 110\u2013126. Springer, Heidelberg (2000)"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/S0304-3975(06)80003-4","volume":"87","author":"W.M. Farmer","year":"1991","unstructured":"Farmer, W.M.: Simple second-order languages for wich unification is undecidable. Theoretical Computer Science\u00a087, 173\u2013214 (1991)","journal-title":"Theoretical Computer Science"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W.D. Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theoretical Computer Science\u00a013, 225\u2013230 (1981)","journal-title":"Theoretical Computer Science"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science\u00a01, 27\u201357 (1975)","journal-title":"Theoretical Computer Science"},{"key":"8_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/3-540-45738-0_7","volume-title":"Logical Aspects of Computational Linguistics","author":"A. Koller","year":"2001","unstructured":"Koller, A., Niehren, J., Treinen, R.: Dominance constraints: Algorithms and complexity. In: Moortgat, M. (ed.) LACL 1998. LNCS (LNAI), vol.\u00a02014, pp. 106\u2013125. Springer, Heidelberg (2001)"},{"issue":"4","key":"8_CR10","doi-asserted-by":"publisher","first-page":"670","DOI":"10.1145\/234533.234543","volume":"43","author":"A. Ko\u015bcielski","year":"1996","unstructured":"Ko\u015bcielski, A., Pacholski, L.: Complexity of Makanin\u2019s algorithm. Journal of the ACM\u00a043(4), 670\u2013684 (1996)","journal-title":"Journal of the ACM"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"8_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/11532231_11","volume-title":"Automated Deduction \u2013 CADE-20","author":"J. Levy","year":"2005","unstructured":"Levy, J., Niehren, J., Villaret, M.: Well-nested context unification. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 149\u2013163. Springer, Heidelberg (2005)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-540-25979-4_4","volume-title":"Rewriting Techniques and Applications","author":"J. Levy","year":"2004","unstructured":"Levy, J., Schmidt-Schau\u00df, M., Villaret, M.: Monadic second-order unification is NP-complete. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol.\u00a03091, pp. 55\u201369. Springer, Heidelberg (2004)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11805618_30","volume-title":"Term Rewriting and Applications","author":"J. Levy","year":"2006","unstructured":"Levy, J., Schmidt-Schau\u00df, M., Villaret, M.: Bounded second-order unification is NP-complete. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol.\u00a04098, Springer, Heidelberg (2006)"},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1006\/inco.2000.2877","volume":"159","author":"J. Levy","year":"2000","unstructured":"Levy, J., Veanes, M.: On the undecidability of second-order unification. Information and Computation\u00a0159, 125\u2013150 (2000)","journal-title":"Information and Computation"},{"key":"8_CR16","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":"2","key":"8_CR17","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1070\/SM1977v032n02ABEH002376","volume":"32","author":"G.S. Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Math. USSR Sbornik\u00a032(2), 129\u2013198 (1977)","journal-title":"Math. USSR Sbornik"},{"key":"8_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/3-540-45738-0_12","volume-title":"Logical Aspects of Computational Linguistics","author":"J. Niehren","year":"2001","unstructured":"Niehren, J., Koller, A.: Dominance constraints in context unification. In: Moortgat, M. (ed.) LACL 1998. LNCS (LNAI), vol.\u00a02014, pp. 199\u2013218. Springer, Heidelberg (2001)"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/3-540-63104-6_4","volume-title":"Automated Deduction - CADE-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.\u00a01249, pp. 34\u201348. Springer, Heidelberg (1997)"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Niehren, J., Pinkal, M., Ruhrberg, P.: A uniform approach to underspecification and parallelism. In: 35th ACL 1997, Madrid, pp. 410\u2013417 (1997)","DOI":"10.3115\/976909.979670"},{"key":"8_CR21","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/S0020-0190(00)00036-3","volume":"74","author":"J. Niehren","year":"2000","unstructured":"Niehren, J., Tison, S., Treinen, R.: On rewrite constraints and context unification. Information Processing Letters\u00a074, 35\u201340 (2000)","journal-title":"Information Processing Letters"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/BFb0049431","volume-title":"Algorithms - ESA \u201994","author":"W. Plandowski","year":"1994","unstructured":"Plandowski, W.: Testing equivalence of morphisms in context-free languages. In: van Leeuwen, J. (ed.) ESA 1994. LNCS, vol.\u00a0855, pp. 460\u2013470. Springer, Heidelberg (1994)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Plandowski, W.: The Complexity of the Morphism Equivalence Problem for Context-Free Languages. PhD thesis, Dept. of Mathematics, Informatics and Mechanics, Warsaw University (1995)","DOI":"10.1007\/BFb0049431"},{"issue":"3","key":"8_CR25","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. Journal of the ACM\u00a051(3), 483\u2013496 (2004)","journal-title":"Journal of the ACM"},{"key":"8_CR26","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"8_CR27","unstructured":"http:\/\/www.satlive.org\/ (2006)"},{"key":"8_CR28","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. TCS\u00a0208, 111\u2013148 (1998)","journal-title":"TCS"},{"issue":"6","key":"8_CR29","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. Journal of Logic and Computation\u00a012(6), 929\u2013953 (2002)","journal-title":"Journal of Logic and Computation"},{"key":"8_CR30","unstructured":"Schmidt-Schau\u00df, M.: Polynomial equality testing for terms with shared substructures. Frank report\u00a021, Institut f\u00fcr Informatik. FB Informatik und Mathematik. J. W. Goethe-Universit\u00e4t Frankfurt am Main (November 2005)"},{"key":"8_CR31","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)"},{"key":"8_CR32","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1007\/s00224-004-1151-9","volume":"37","author":"M. Schmidt-Schau\u00df","year":"2004","unstructured":"Schmidt-Schau\u00df, M., Stuber, J.: On the complexity of linear and stratified context matching problems. Theory of Computing Systems\u00a037, 717\u2013740 (2004)","journal-title":"Theory of Computing Systems"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T06:08:57Z","timestamp":1736575737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/11814771_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}