{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,16]],"date-time":"2024-09-16T21:29:38Z","timestamp":1726522178919},"reference-count":56,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2000,7,1]],"date-time":"2000-07-01T00:00:00Z","timestamp":962409600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4764,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2000,7]]},"DOI":"10.1016\/s0304-3975(98)00185-6","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T16:43:06Z","timestamp":1027615386000},"page":"167-184","source":"Crossref","is-referenced-by-count":6,"title":["Decidability and complexity of simultaneous rigid E-unification with one variable and related results"],"prefix":"10.1016","volume":"243","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuri","family":"Gurevich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"2","key":"10.1016\/S0304-3975(98)00185-6_BIB1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","article-title":"Theorem proving via general matings","volume":"28","author":"Andrews","year":"1981","journal-title":"J. Assoc. Comput. Mach."},{"year":"1993","series-title":"Deduction. Automated Logic","author":"Bibel","key":"10.1016\/S0304-3975(98)00185-6_BIB2"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB3","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/S0019-9958(69)90065-5","article-title":"Tree generating regular systems","volume":"14","author":"Brainerd","year":"1969","journal-title":"Inform. Control"},{"year":"1990","series-title":"Model Theory","author":"Chang","key":"10.1016\/S0304-3975(98)00185-6_BIB4"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB5","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/0304-3975(94)90101-5","article-title":"Bottom-up tree pushdown automata: classification and connection with rewrite systems","volume":"127","author":"Coquid\u00e9","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB6","series-title":"Resolution of Equations in Algebraic Structures","article-title":"On recognizable sets and tree automata","author":"Courcelle","year":"1989"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB7","article-title":"Rewriting and tree automata","volume":"vol. 909","author":"Dauchet","year":"1993"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB8","unstructured":"M. Dauchet, T. Heuillard, P. Lescanne, S. Tison, Decidability of the confluence of ground term rewriting systems, Proc. IEEE Conf. on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, 1987, pp. 353\u2013360."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB9","doi-asserted-by":"crossref","unstructured":"M. Dauchet, S. Tison, Tree automata and decidability in ground term rewriting systems, Proc. FCT\u201985, Lecture Notes in Computer Science, vol. 199, 1985, pp. 80\u201384.","DOI":"10.1007\/BFb0028794"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB10","doi-asserted-by":"crossref","unstructured":"M. Dauchet, S. Tison, The theory of ground rewrite systems is decidable, Proc. IEEE Conf. on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, 1990, pp. 242\u2013248.","DOI":"10.1109\/LICS.1990.113750"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB11","article-title":"Rigid E-unification simplified","volume":"vol. 918","author":"De Kogel","year":"1995"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB12","unstructured":"A. Degtyarev, Yu. Gurevich, A. Voronkov, Herbrand's theorem and equational reasoning: problems and solutions, Bulletin of the European Association for Theoretical Computer Science, vol. 60, The Logic in Computer Science column, October 1996."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB13","unstructured":"A. Degtyarev, Yu. Matiyasevich, A. Voronkov, Simultaneous rigid E-unification is not so simple, UPMAIL Technical Report 104, Uppsala University, Computing Science Department, April 1995."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB14","doi-asserted-by":"crossref","unstructured":"A. Degtyarev, Yu. Matiyasevich, A. Voronkov, Simultaneous rigid E-unification and related algorithmic problems, 11th Ann. IEEE Symp. on Logic in Computer Science (LICS\u201996), New Brunswick, NJ, July, IEEE Computer Society Press, Silver Spring, MD, 1996, pp. 494\u2013502.","DOI":"10.1109\/LICS.1996.561466"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB15","doi-asserted-by":"crossref","unstructured":"A. Degtyarev, 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":"10.1016\/S0304-3975(98)00185-6_BIB16","doi-asserted-by":"crossref","unstructured":"A. Degtyarev, A. Voronkov, Decidability problems for the prenex fragment of intuitionistic logic, 11th Ann. IEEE Symp. on Logic in Computer Science (LICS\u201996), New Brunswick, NJ, July, IEEE Computer Society Press, Silver Spring, MD, 1996, pp. 503\u2013512.","DOI":"10.1109\/LICS.1996.561467"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB17","doi-asserted-by":"crossref","unstructured":"A. Degtyarev, A. Voronkov, Simultaneous rigid E-unification is undecidable, in: H. Kleine B\u00fcning, (Ed.), Computer Science Logic. 9th Int. Workshop, CSL\u201995, Lecture Notes in Computer Science, vol. 1092, Paderborn, Germany, September 1995, 1996, pp. 178\u2013190.","DOI":"10.1007\/3-540-61377-3_38"},{"issue":"1\u20132","key":"10.1016\/S0304-3975(98)00185-6_BIB18","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","article-title":"The undecidability of simultaneous rigid E-unification","volume":"166","author":"Degtyarev","year":"1996","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB19","series-title":"Handbook of Theoretical Computer Science, vol. B: Formal Methods and Semantics, ch. 6","first-page":"243","article-title":"Rewrite systems","author":"Dershowitz","year":"1990"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB20","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1016\/S0022-0000(70)80041-1","article-title":"Tree acceptors and some of their applications","volume":"4","author":"Doner","year":"1970","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB21","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF00244394","article-title":"First-order modal tableaux","volume":"4","author":"Fitting","year":"1988","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB22","doi-asserted-by":"crossref","unstructured":"T. Fr\u00fchwirth, E. Shapiro, M. Vardi, E. Yardeni, Logic programs as types of logic programs, Proc. 6th Symp. on Logics in Computer Science (LICS), 1991, pp. 300\u2013309.","DOI":"10.1109\/LICS.1991.151654"},{"issue":"1\/2","key":"10.1016\/S0304-3975(98)00185-6_BIB23","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0890-5401(90)90061-L","article-title":"Rigid E-unification: NP-completeness and applications to equational matings","volume":"87","author":"Gallier","year":"1990","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB24","doi-asserted-by":"crossref","unstructured":"J.H. Gallier, P. Narendran, D. Plaisted, W. Snyder, Rigid E-unification is NP-complete, Proc. IEEE Conf. on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, July 1988, pp. 338\u2013346.","DOI":"10.1109\/LICS.1988.5121"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB25","unstructured":"J.H. Gallier, S. Raatz, W. Snyder, Theorem proving using rigid E-unification: equational matings, Proc. IEEE Conf. on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, 1987, pp. 338\u2013346."},{"year":"1984","series-title":"Tree Automata","author":"G\u00e9cseg","key":"10.1016\/S0304-3975(98)00185-6_BIB26"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB27","unstructured":"J. Goubault, Rigid E-unifiability is DEXPTIME-complete, Proc. IEEE Conf. on Logic in Computer Science (LICS), IEEE Computer Society Press, Silver Spring, MD, 1994."},{"year":"1995","series-title":"Limits to Parallel Computation: P-Completeness Theory","author":"Greenlaw","key":"10.1016\/S0304-3975(98)00185-6_BIB28"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB29","unstructured":"Y. Gurevich, M. Veanes, Some undecidable problems related to the Herbrand theorem, UPMAIL Technical Report 138, Uppsala University, Computing Science Department, March 1997, Inform. Comput. submitted."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB30","first-page":"154","article-title":"Monadic simultaneous rigid E-unification and related problems","volume":"vol. 1256","author":"Gurevich","year":"1997"},{"year":"1976","series-title":"Complexity of finitely presented algebras, Technical Report TR 76-294","author":"Kozen","key":"10.1016\/S0304-3975(98)00185-6_BIB31"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB32","doi-asserted-by":"crossref","unstructured":"D. Kozen, Complexity of finitely presented algebras, Proc. 9th Ann. Symp. on Theory of Computing, ACM, New York, 1977, pp. 164\u2013177.","DOI":"10.1145\/800105.803406"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB33","doi-asserted-by":"crossref","unstructured":"D. Kozen, Lower bounds for natural proof systems, Proc. 18th IEEE Symp. on Foundations of Computer Science (FOCS), 1977, pp. 254\u2013266.","DOI":"10.1109\/SFCS.1977.16"},{"issue":"4","key":"10.1016\/S0304-3975(98)00185-6_BIB34","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1147\/rd.254.0327","article-title":"Positive first-order logic is NP-complete","volume":"25","author":"Kozen","year":"1981","journal-title":"IBM J. Res. Dev."},{"year":"1975","series-title":"Canonical inference, Technical Report","author":"Lankford","key":"10.1016\/S0304-3975(98)00185-6_BIB35"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB36","doi-asserted-by":"crossref","unstructured":"V. Lifschitz, Problem of decidability for some constructive theories of equalities (in Russian), Zapiski Nauchnyh Seminarov LOMI 4 (1967) 78\u201385. (English Trans. Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, pp. 29\u201331).","DOI":"10.1007\/978-1-4684-8968-2_8"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB37","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","article-title":"Mechanical theorem proving by model elimination","volume":"15","author":"Loveland","year":"1968","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB38","doi-asserted-by":"crossref","unstructured":"G.S. Makanin, The problem of solvability of equations in free semigroups, Mat. Sbornik (in Russian) 103(2) (1977) 147\u2013236. (English Trans. Amer. Math. Soc. Trans. 117 (2) (1981)).","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB39","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0019-9958(67)90353-1","article-title":"Algebraic automata and context-free sets","volume":"11","author":"Mezei","year":"1967","journal-title":"Inform. Control"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB40","doi-asserted-by":"crossref","unstructured":"G.E. Mints, Choice of terms in quantifier rules of constructive predicate calculus (in Russian), Zapiski Nauchnyh Seminarov LOMI 4 (1967) 78\u201385. (English Trans. Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, pp. 43\u201346).","DOI":"10.1007\/978-1-4684-8968-2_11"},{"issue":"3","key":"10.1016\/S0304-3975(98)00185-6_BIB41","first-page":"581","article-title":"Unsolvability in the constructive predicate calculus of the class of the formulas of the type \u00ac\u00ac\u2200\u2203 (in Russian)","volume":"163","author":"Orevkov","year":"1965","journal-title":"Soviet Math. Dokl."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB42","unstructured":"V.P. Orevkov, Solvable classes of pseudo-prenex formulas (in Russian), Zapiski Nauchnyh Seminarov LOMI 60 (1976) 109\u2013170 (English Trans. J. Soviet Math.)"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB43","unstructured":"D.A. Plaisted, Special cases and substitutes for rigid E-unification, Technical Report MPI-I-95-2-010, Max-Planck-Institut f\u00fcr Informatik, November 1995."},{"issue":"2","key":"10.1016\/S0304-3975(98)00185-6_BIB44","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0020-0190(94)00130-8","article-title":"Haskell overloading is DEXPTIME-complete","volume":"52","author":"Seidl","year":"1994","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB45","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1145\/359545.359570","article-title":"An algorithm for reasoning about equality","volume":"21","author":"Shostak","year":"1978","journal-title":"Commun. ACM"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB46","first-page":"419","article-title":"Efficient ground completion","volume":"vol. 355","author":"Snyder","year":"1989"},{"issue":"1","key":"10.1016\/S0304-3975(98)00185-6_BIB47","first-page":"104","article-title":"Lower bounds on Herbrand's theorem","volume":"75","author":"Statman","year":"1979","journal-title":"Proc. Amer. Math. Soc."},{"issue":"1","key":"10.1016\/S0304-3975(98)00185-6_BIB48","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/BF01691346","article-title":"Generalized finite automata theory with an application to a decision problem of second-order logic","volume":"2","author":"Thatcher","year":"1968","journal-title":"Math. Systems Theory"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB49","unstructured":"W. Thomas, Languages, automata and logic, Technical Report 9607, Institut f\u00fcr Informatik und Praktische Mathematik der Christian-Albrechts-Universit\u00e4t zu Kiel, 1996, in: G. Rozenberg, A. Salomaa (Eds.), A modified version appears as a chapter of the Handbook of Formal Language Theory, Springer, Berlin."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB50","unstructured":"M. Veanes, On computational complexity of basic decision problems of finite tree automata, UPMAIL Technical Report 133, Uppsala University, Computing Science Department, January 1997."},{"key":"10.1016\/S0304-3975(98)00185-6_BIB51","doi-asserted-by":"crossref","unstructured":"M. Veanes, The undecidability of simultaneous rigid E-unification with two variables, Proc. Kurt G\u00f6del Colloquium KGC\u201997, Lecture Notes in Computer Science, vol. 1289, Springer, Berlin, 1997, pp. 305\u2013318.","DOI":"10.1007\/3-540-63385-5_52"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB52","doi-asserted-by":"crossref","unstructured":"M. Veanes, The relation between second-order unification and simultaneous rigid E-unification, Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS\u201998), IEEE Computer Society Press, 1998, pp. 264\u2013275.","DOI":"10.1109\/LICS.1998.705663"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB53","doi-asserted-by":"crossref","unstructured":"A. Voronkov, Proof search in intuitionistic logic based on constraint satisfaction, in: P. Miglioli, U. Moscato, D. Mundici, M. Ornaghi (Eds.), Theorem Proving with Analytic Tableaux and Related Methods. 5th Int. Workshop, TABLEAUX \u201996, Lecture Notes in Artificial Intelligence, vol. 1071, Terrasini, Palermo Italy, May 1996, pp. 312\u2013329.","DOI":"10.1007\/3-540-61208-4_20"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB54","doi-asserted-by":"crossref","unstructured":"A. Voronkov, Proof search in intuitionistic logic with equality, or back to simultaneous rigid E-unification, in: M.A. McRobbie, J.K. Slaney (Eds.), Automated Deduction \u2013 CADE-13, Lecture Notes in Computer Science, vol. 1104, New Brunswick, NJ, USA, 1996, pp. 32\u201346.","DOI":"10.1007\/3-540-61511-3_67"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB55","doi-asserted-by":"crossref","unstructured":"A. Voronkov, Herbrand's theorem, automated reasoning and semantic tableaux, Proc. Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS\u201998), IEEE Computer Society Press, 1998, pp. 252\u2013263.","DOI":"10.1109\/LICS.1998.705662"},{"key":"10.1016\/S0304-3975(98)00185-6_BIB56","unstructured":"A. Voronkov, Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem, UPMAIL Technical Report 152, Uppsala University, Computing Science Department, February 1998, Theoret. Comput. Sci., submitted."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397598001856?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397598001856?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,16]],"date-time":"2020-01-16T16:35:50Z","timestamp":1579192550000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397598001856"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,7]]},"references-count":56,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2000,7]]}},"alternative-id":["S0304397598001856"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(98)00185-6","relation":{},"ISSN":["0304-3975"],"issn-type":[{"type":"print","value":"0304-3975"}],"subject":[],"published":{"date-parts":[[2000,7]]}}}