{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T14:13:34Z","timestamp":1648995214283},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540643012","type":"print"},{"value":"9783540697213","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0052370","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T05:31:11Z","timestamp":1149658271000},"page":"181-195","source":"Crossref","is-referenced-by-count":8,"title":["The decidability of simultaneous rigid E-unification with one variable"],"prefix":"10.1007","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[]},{"given":"Yuri","family":"Gurevich","sequence":"additional","affiliation":[]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[]},{"given":"Margus","family":"Veanes","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,18]]},"reference":[{"issue":"2","key":"15_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"P.B. Andrews. Theorem proving via generell matings. Journal of the Association for Computing Machinery, 28(2):193\u2013214, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"15_CR2","unstructured":"W. Bibel. Deduction. Automated Logic. Academic Press, 1993."},{"key":"15_CR3","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/S0019-9958(69)90065-5","volume":"14","author":"W.S. Brainerd","year":"1969","unstructured":"W.S. Brainerd. Tree generating regular systems. Information and Control, 14:217\u2013231, 1969.","journal-title":"Information and Control"},{"key":"15_CR4","volume-title":"Model Theory","author":"C.C. Chang","year":"1990","unstructured":"C.C. Chang and H.J. Keisler. Model Theory. North-Holland, Amsterdam, third edition, 1990.","edition":"third edition"},{"key":"15_CR5","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":"15_CR6","doi-asserted-by":"crossref","unstructured":"B. Courcelle. On recognizable sets and tree automata. In M. Nivat and H. AitKaci, editors, Resolution of Equations in Algebraic Structures. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046370-1.50009-7"},{"key":"15_CR7","first-page":"95","volume-title":"Term Rewriting (French Spring School of Theoretical Computer Science), volume 909 of Lecture Notes in 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":"15_CR8","first-page":"17","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods, number 918 in Lecture Notes in Artificial Intelligence","author":"E. Kogel De","year":"1995","unstructured":"E. De Kogel. Rigid E-unification simplified. In P. Baumgartner, R. H\u00e4hnle, and J. Posegga, editors, Theorem Proving with Analytic Tableaux and Related Methods, number 918 in Lecture Notes in Artificial Intelligence, pages 17\u201330, Schlo\u00df Rheinfels, St. Goar, Germany, May 1995."},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"A. Degtyarev, Yu. Gurevich, P. Narendran, M. Veanes, and A. Voronkov. The decidability of simultaneous rigid E-unification with one variable. UPMAIL Technical Report 139, Uppsala University, Computing Science Department, March 1997.","DOI":"10.1007\/BFb0052370"},{"key":"15_CR10","unstructured":"A. Degtyarev, Yu. Gurevich, and A. Voronkov. Herbrand's theorem and equational reasoning: Problems and solutions. In Bulletin of the European Association for Theoretical Computer Science, volume 60. October 1996. The \u201cLogic in Computer Science\u201d column."},{"key":"15_CR11","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":"15_CR12","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1109\/LICS.1996.561467","volume-title":"Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96)","author":"A. Degtyarev","year":"1996","unstructured":"A. Degtyarev and A. Voronkov. Decidability problems for the prenex fragment of intuitionistic logic. In Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96), pages 503\u2013512, New Brunswick, NJ, July 1996. IEEE Computer Society Press."},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. Simultaneous rigid E-unification is undecidable. In H. Kleine B\u00fcning, editor, Computer Science Logic. 9th International Workshop, CSL'95, volume 1092 of Lecture Notes in Computer Science, pages 178\u2013190, Paderborn, Germany, September 1995, 1996.","DOI":"10.1007\/3-540-61377-3_38"},{"issue":"1\u20132","key":"15_CR14","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(96)00092-8","volume":"166","author":"A. Degtyarev","year":"1996","unstructured":"A. Degtyarev and A. Voronkov. The undecidability of simultaneous rigid E- unification. Theoretical Computer Science, 166(1\u20132):291\u2013300, 1996.","journal-title":"Theoretical Computer Science"},{"key":"15_CR15","first-page":"243","volume-title":"Handbook of Theoretical Computer Science, volume B: Formal Methods and Semantics","author":"N. Dershowitz","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":"15_CR16","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":"15_CR17","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF00244394","volume":"4","author":"M. Fitting","year":"1988","unstructured":"M. Fitting. First-order modal tableaux. Journal of Automated Reasoning, 4:191\u2013213, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"15_CR18","unstructured":"T. Fr\u00fchwirth, E. Shapiro, M. Vardi, and E. Yardeni. Logic programs as types of logic programs. In Proc. 6th Symposium on Logics in Computer Science (LICS), pages 300\u2013309, 1991."},{"key":"15_CR19","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":"15_CR20","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":"15_CR21","volume-title":"Tree Automata","author":"F. G\u00e9cseg","year":"1984","unstructured":"F. G\u00e9cseg and M. Steinby. Tree Automata. Akad\u00e9miai Kiod\u00f3, Budapest, 1984."},{"key":"15_CR22","unstructured":"J. Goubault. Rigid E-unifiability is DEXPTIME-complete. In Proc. IEEE Conference on Logic in Computer Science (LICS). IEEE Computer Society Press, 1994. 23. R. Greenlaw, H.J. Hoover, and W.L. Ruzzo. Limits to Parallel Computation: P-Completeness Theory. Oxford University Press, 1995."},{"key":"15_CR23","unstructured":"Y. Gurevich and M. Veanes. Some undecidable problems related to the Herbrand theorem. UPMAIL Technical Report 138, Uppsala University, Computing Science Department, March 1997."},{"key":"15_CR24","unstructured":"Y. Gurevich and A. Voronkov. The monadic case of simultaneous rigid E- unification. UPMAIL Technical Report 137, Uppsala University, Computing Science Department, 1997. To appear in Proc. of ICALP'97."},{"key":"15_CR25","volume-title":"Technical Report TR 76-294","author":"D. Kozen","year":"1976","unstructured":"D. Kozen. Complexity of finitely presented algebras. Technical Report TR 76-294, Cornell University, Ithaca, N.Y., 1976."},{"key":"15_CR26","first-page":"164","volume-title":"Proc. of the 9th Annual Symposium on Theory of Computing","author":"D. Kozen","year":"1977","unstructured":"D. Kozen. Complexity of finitely presented algebras. In Proc. of the 9th Annual Symposium on Theory of Computing, pages 164\u2013177, New York, 1977. ACM."},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"D. Kozen. Lower bounds for natural proof systems. In Proc. 18th IEEE Symposium on Foundations of Computer Science (FOCS), pages 254\u2013266, 1977.","DOI":"10.1109\/SFCS.1977.16"},{"key":"15_CR28","volume-title":"Technical report","author":"D.S. Lankford","year":"1975","unstructured":"D.S. Lankford. Canonical inference. Technical report, Department of Mathematics, South-Western University, Georgetown, Texas, 1975."},{"key":"15_CR29","first-page":"78","volume":"4","author":"V. Lifschitz","year":"1967","unstructured":"V. Lifschitz. Problem of decidability for some constructive theories of equalities (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4:78\u201385, 1967. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, p.29\u201331.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"15_CR30","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"D.W. Loveland. Mechanical theorem proving by model elimination. Journal of the Association for Computing Machinery, 15:236\u2013251, 1968.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"15_CR31","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0019-9958(67)90353-1","volume":"11","author":"J. Mezei","year":"1967","unstructured":"J. Mezei and J.B. Wright. Algebraic automata and context-free sets. Information and Control, 11:3\u201329, 1967.","journal-title":"Information and Control"},{"key":"15_CR32","first-page":"78","volume":"4","author":"G.E. Mints","year":"1967","unstructured":"G.E. Mints. Choice of terms in quantifier rules of constructive predicate calculus (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4:78\u201385, 1967. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, p.43\u201346.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"issue":"3","key":"15_CR33","first-page":"581","volume":"163","author":"V.P. Orevkov","year":"1965","unstructured":"V.P. Orevkov. Unsolvability in the constructive predicate calculus of the class of the formulas of the type \u2223\u2223\u2200\u2203 (in Russian). Soviet Mathematical Doklady, 163(3):581\u2013583, 1965.","journal-title":"Soviet Mathematical Doklady"},{"key":"15_CR34","first-page":"109","volume":"60","author":"V.P. Orevkov","year":"1976","unstructured":"V.P. Orevkov. Solvable classes of pseudo-prenex formulas (in Russian). Zapiski Nauchnyh Seminarov LOMI, 60:109\u2013170, 1976. English translation in: Journal of Soviet Mathematics.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"issue":"2","key":"15_CR35","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0020-0190(94)00130-8","volume":"52","author":"H. Seidl","year":"1994","unstructured":"H. Seidl. Haskell overloading is DEXPTIME-complete. Information Processing Letters, 52(2):57\u201360, 1994.","journal-title":"Information Processing Letters"},{"key":"15_CR36","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R. Shostak","year":"1978","unstructured":"R. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21:583\u2013585, July 1978.","journal-title":"Communications of the ACM"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"W. Snyder. Efficient ground completion: An O(nlogn) algorithm for generating reduced sets of ground rewrite rules equivalent to a set of ground equations E. In G. Goos and J. Hartmanis, editors, Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science, pages 419\u2013433. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51081-8_123"},{"issue":"1","key":"15_CR38","first-page":"104","volume":"75","author":"R. Statman","year":"1979","unstructured":"R. Statman. Lower bounds on Herbrand's theorem. Proc. American Mathematical Society, 75(1):104\u2013107, 1979.","journal-title":"Proc. American Mathematical Society"},{"issue":"1","key":"15_CR39","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":"15_CR40","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":"15_CR41","doi-asserted-by":"crossref","unstructured":"M. Veanes. The undecidability of simultaneous rigid E-unification with two variables. To appear in Proc. Kurt G\u00f6del Colloquium KGC'97, 1997.","DOI":"10.1007\/3-540-63385-5_52"},{"key":"15_CR42","doi-asserted-by":"crossref","unstructured":"A. Voronkov. Proof search in intuitionistic logic based on constraint satisfaction. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods. 5th International Workshop, TABLEAUX '96, volume 1071 of Lecture Notes in Artificial Intelligence, pages 312\u2013329, Terrasini, Palermo Italy, May 1996.","DOI":"10.1007\/3-540-61208-4_20"},{"key":"15_CR43","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 and J.K. Slaney, editors, Automated Deduction \u2014CADE-13, volume 1104 of Lecture Notes in Computer Science, pages 32\u201346, New Brunswick, NJ, USA, 1996.","DOI":"10.1007\/3-540-61511-3_67"}],"container-title":["Rewriting Techniques and Applications","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0052370","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T06:34:04Z","timestamp":1555655644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0052370"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643012","9783540697213"],"references-count":43,"URL":"http:\/\/dx.doi.org\/10.1007\/bfb0052370","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1998]]}}}