{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:23Z","timestamp":1749125183770,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":47,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540613770"},{"type":"electronic","value":"9783540685074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61377-3_38","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:35:43Z","timestamp":1330292143000},"page":"178-190","source":"Crossref","is-referenced-by-count":19,"title":["Simultaneous rigid E-unification is undecidable"],"prefix":"10.1007","author":[{"given":"Anatoli","family":"Degtyarev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"2","key":"11_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"P.B. Andrews. Theorem proving via general matings. Journal of the Association for Computing Machinery, 28(2):193\u2013214, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR2","unstructured":"M. Baaz. Note on the existence of most general semi-unifiers. In Arithmetic, Proof Theory and Computation Complexity, volume 23 of Oxford Logic Guides, pages 20\u201329. Oxford University Press, 1993."},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Peter Baumgartner. An ordered theory resolution calculus. In A. Voronkov, editor, Logic Programming and Automated Reasoning (LPAR'92), volume 624 of Lecture Notes in Computer Science, pages 119\u2013130, 1992.","DOI":"10.1007\/BFb0013054"},{"key":"11_CR4","series-title":"volume 861 of Lecture Notes in Artificial Intelligence","first-page":"319","volume-title":"Rigid unification by completion and rigid paramodulation","author":"G. Becher","year":"1994","unstructured":"G. Becher and U. Petermann. Rigid unification by completion and rigid paramodulation. In B. Nebel and L. Dreschler-Fischer, editors, KI-94: Advances in Artificial Intelligence. 18th German Annual Conference on Artificial Intelligence, volume 861 of Lecture Notes in Artificial Intelligence, pages 319\u2013330, Saarbr\u00fccken, Germany, September 1994. Springer Verlag."},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"B. Beckert. A completion-based method for mixed universal and rigid E-unification. In A. Bundy, editor, Automated Deduction \u2014 CADE-12. 12th International Conference on Automated Deduction., volume 814 of Lecture Notes in Artificial Intelligence, pages 678\u2013692, Nancy, France, June\/July 1994.","DOI":"10.1007\/3-540-58156-1_49"},{"key":"11_CR6","unstructured":"B. Beckert. Are minimal solutions to simultaneous rigid E-unification problems sufficient to adding equality to semantic tableaux. Privately circulated manuscript, 1995."},{"key":"11_CR7","first-page":"678","volume-title":"An improved method for adding equality to free variable semantic tableaux","author":"B. Beckert","year":"1992","unstructured":"B. Beckert and R. H\u00e4hnle. An improved method for adding equality to free variable semantic tableaux. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 678\u2013692, Saratoga Springs, NY, USA, June 1992. Springer Verlag."},{"key":"11_CR8","unstructured":"E.W. Beth. The Foundations of Mathematics. North Holland, 1959."},{"issue":"4","key":"11_CR9","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"W. Bibel. On matrices with connections. Journal of the Association for Computing Machinery, 28(4):633\u2013645, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR10","unstructured":"W. Bibel. Deduction. Automated Logic. Academic Press, 1993."},{"key":"11_CR11","unstructured":"A. Degtyarev, Yu, Matiyasevich, and A. Voronkov. Simultaneous rigid E-unification is not so simple. UPMAIL Technical Report 104, Uppsala University, Computing Science Department, April 1995."},{"key":"11_CR12","unstructured":"A. Degtyarev, Yu. Matiyasevich, and A. Voronkov. Simultaneous rigid E-unification and related algorithmic problems. To appear in LICS'96, 1996."},{"key":"11_CR13","unstructured":"A. Degtyarev and A. Voronkov. Equality elimination for semantic tableaux. UP MAIL Technical Report 90, Uppsala University, Computing Science Department, December 1994. Submitted to a conference."},{"key":"11_CR14","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":"11_CR15","unstructured":"A. Degtyarev and A. Voronkov. Reduction of second-order unification to simultaneous rigid E-unification. UPMAIL Technical Report 109, Uppsala University, Computing Science Department, June 1995."},{"key":"11_CR16","unstructured":"A. Degtyarev and A. Voronkov. Equality elimination for the inverse method and extension procedures. In C.S. Mellish, editor, Proc. International Joint Conference on Artificial Intelligence (IJCAI), volume 1, pages 342\u2013347, Montr\u00e9al, August 1995."},{"key":"11_CR17","first-page":"109","volume-title":"General connections via equality elimination","author":"A. Degtyarev","year":"1995","unstructured":"A. Degtyarev and A. Voronkov. General connections via equality elimination. In M. De Glas and Z. Pawlak, editors, Second World Conference on the Fundamentals of Artificial Intelligence (WOCFAI-95), pages 109\u2013120, Paris, July 1995. Angkor."},{"key":"11_CR18","unstructured":"A. Degtyarev and A. Voronkov, Skolemization and decidability problems for fragments of intuitionistic logic. To appear in LICS'96, 1996."},{"key":"11_CR19","unstructured":"A. Degtyarev and A. Voronkov. A complete proof procedure for first-order logic based on an incomplete procedure for rigid E-unification. Submitted to a conference, 1996."},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"A. Degtyarev and A. Voronkov. The undecidability of simultaneous rigid E-unification. To appear in Theoretical Computer Science, 10 pages, 1996.","DOI":"10.1007\/3-540-61377-3_38"},{"issue":"2","key":"11_CR21","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/128749.128754","volume":"39","author":"J. Gallier","year":"1992","unstructured":"J. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid E-unification. Journal of the Association for Computing Machinery, 39(2):377\u2013429, 1992.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR22","first-page":"338","volume-title":"Logic in Computer Science (LICS'88)","author":"J.H. Gallier","year":"1988","unstructured":"J.H. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification is NP-complete. In Logic in Computer Science (LICS'88) (Edinburgh, Scotland), pages 338\u2013346. IEEE Computer Society Press, July 1988."},{"issue":"1\/2","key":"11_CR23","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/0890-5401(90)90061-L","volume":"87","author":"J. Gallier","year":"1990","unstructured":"J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification: NP-completeness and applications to equational matings. Information and Computation, 87(1\/2):129\u2013195, 1990.","journal-title":"Information and Computation"},{"key":"11_CR24","first-page":"338","volume-title":"Logic in Computer Science (LICS'87)","author":"J.H. Gallier","year":"1987","unstructured":"J.H. Gallier, S. Raatz, and W. Snyder. Theorem proving using rigid E-unification: Equational matings. In Logic in Computer Science (LICS'87) (Ithaca, N. Y.), pages 338\u2013346. IEEE Computer Society Press, 1987."},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"J.H. Gallier, S. Raatz, and W. Snyder. Rigid E-unification and its applications to equational matings. In H. A\u00eft Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 1, pages 151\u2013216. Academic Press, 1989.","DOI":"10.1016\/B978-0-12-046370-1.50011-5"},{"issue":"1","key":"11_CR26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"J.-Y. Girard. Linear logic. Theoretical Computer Science, 50(1):1\u2013101, 1987.","journal-title":"Theoretical Computer Science"},{"key":"11_CR27","unstructured":"C.A. Goad. Computational uses of the manipulation of formal proofs. Technical Report TR no. STAN-CS-80-819, Stanford Univ. Department of Computer Science, 1980."},{"key":"11_CR28","doi-asserted-by":"crossref","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":"11_CR29","unstructured":"J. Goubault. Rigid E-unifiability is DEXPTIME-complete. In Logic in Computer Science (LICS'94). IEEE Computer Society Press, 1994."},{"key":"11_CR30","doi-asserted-by":"crossref","unstructured":"S. Kanger. A simplified proof method for elementary logic. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning. Classical Papers on Computational Logic, volume 1, pages 364\u2013371. Springer Verlag, 1983. Originally appeared in 1963.","DOI":"10.1007\/978-3-642-81952-0_23"},{"issue":"4","key":"11_CR31","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1147\/rd.254.0327","volume":"25","author":"D. Kozen","year":"1981","unstructured":"D. Kozen. Positive first-order logic is NP-complete. IBM J. of Research and Development, 25(4):327\u2013332, 1981.","journal-title":"IBM J. of Research and Development"},{"key":"11_CR32","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":"11_CR33","doi-asserted-by":"crossref","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":"11_CR34","first-page":"96","volume":"4","author":"S. Maslov","year":"1967","unstructured":"S.Yu. Maslov. Invertible sequential variant of constructive predicate calculus (in Russian). Zapiski Nauchnyh Seminarov LOMI, 4:96\u2013111, 1967. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 4, Consultants Bureau, NY-London, 1969, p. 36\u201342.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"issue":"2","key":"11_CR35","first-page":"354","volume":"11","author":"Y.V. Matiyasevi\u010d","year":"1970","unstructured":"Y.V. Matiyasevi\u010d. Enumerable sets are Diophantine. Soviet Mathematical Doklady, 11(2):354\u2013358, 1970.","journal-title":"Soviet Mathematical Doklady"},{"key":"11_CR36","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"},{"key":"11_CR37","volume-title":"Technical Report AR-95-11","author":"M. Moser","year":"1995","unstructured":"M. Moser, C. Lynch, and J. Steinbach. Model elimination with basic ordered paramodulation. Technical Report AR-95-11, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, 1995."},{"issue":"3","key":"11_CR38","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-\u2200\u2203 (in Russian). Soviet Mathematical Doklady, 163(3):581\u2013583, 1965.","journal-title":"Soviet Mathematical Doklady"},{"key":"11_CR39","first-page":"152","volume":"16","author":"V.P. Orevkov","year":"1969","unstructured":"V.P. Orevkov. On nonlengthening applications of equality rules (in Russian). Zapiski Nauchnyh Seminarov LOMI, 16:152\u2013156, 1969. English Translation in: Seminars in Mathematics: Steklov Math. Inst. 16, Consultants Bureau, NY-London, 1971, p.77\u201379.","journal-title":"Zapiski Nauchnyh Seminarov LOMI"},{"key":"11_CR40","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"},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"U. Petermann. A complete connection calculus with rigid E-unification. In JELIA'94, volume 838 of Lecture Notes in Computer Science, pages 152\u2013166, 1994.","DOI":"10.1007\/BFb0021970"},{"key":"11_CR42","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."},{"key":"11_CR43","doi-asserted-by":"crossref","unstructured":"D. Prawitz. An improved proof procedure. In J. Siekmann and G. Wrightson, editors, Automation of Reasoning. Classical Papers on Computational Logic, volume 1, pages 162\u2013201. Springer Verlag, 1983. Originally appeared in 1960.","DOI":"10.1007\/978-3-642-81952-0_12"},{"key":"11_CR44","doi-asserted-by":"crossref","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":"11_CR45","doi-asserted-by":"crossref","unstructured":"M. Veanes. Undecidability proofs of simultaneous rigid E-unification. Upmail technical report, Uppsala University, Computing Science Department, 1996. To appear.","DOI":"10.1007\/3-540-63385-5_52"},{"key":"11_CR46","unstructured":"P.J. Voda and J. Komara. On Herbrand skeletons. Technical report, Institute of Informatics, Comenius University Bratislava, July 1995."},{"key":"11_CR47","doi-asserted-by":"crossref","unstructured":"A. Voronkov. On proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-Unification. UPMAIL Technical Report 121, Uppsala University, Computing Science Department, January 1996. To appear in CADE'96, 15 pages, 1996.","DOI":"10.1007\/3-540-61511-3_67"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61377-3_38.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:18:40Z","timestamp":1742599120000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61377-3_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540613770","9783540685074"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/3-540-61377-3_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}