{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:05:31Z","timestamp":1749125131684},"reference-count":31,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1996,10,1]],"date-time":"1996-10-01T00:00:00Z","timestamp":844128000000},"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":6133,"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":[[1996,10]]},"DOI":"10.1016\/0304-3975(96)00092-8","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T00:48:18Z","timestamp":1027644498000},"page":"291-300","source":"Crossref","is-referenced-by-count":30,"title":["The undecidability of simultaneous rigid E-unification"],"prefix":"10.1016","volume":"166","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":"78","reference":[{"key":"10.1016\/0304-3975(96)00092-8_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":"Jo. Assoc. Comput. Machinery"},{"key":"10.1016\/0304-3975(96)00092-8_BIB2","series-title":"Arithmetic, Proof Theory and Computation Complexity","first-page":"20","article-title":"Note on the existence of most general semi-unifiers","volume":"Vol. 23","author":"Baaz","year":"1993"},{"key":"10.1016\/0304-3975(96)00092-8_BIB3","series-title":"Logic Programming and Automated Reasoning (LPAR'92)","first-page":"119","article-title":"An ordered theory resolution calculus","volume":"Vol. 624","author":"Baumgartner","year":"1992"},{"key":"10.1016\/0304-3975(96)00092-8_BIB4","series-title":"KI-94: Advances in Artificial Intelligence. 18th German Annual Conference on Artificial Intelligence","first-page":"319","article-title":"Rigid unification by completion and rigid paramodulation","volume":"Vol. 861","author":"Becher","year":"1994"},{"key":"10.1016\/0304-3975(96)00092-8_BIB5","series-title":"Automated Deduction \u2014 CADE-12. 12th Internat. Conf. on Automated Deduction","first-page":"678","article-title":"A completion-based method for mixed universal and rigid E-unification","volume":"Vol. 814","author":"Beckert","year":"1994"},{"key":"10.1016\/0304-3975(96)00092-8_BIB6","series-title":"11th Internat. Conf. on Automated Deduction (CADE)","first-page":"678","article-title":"An improved method for adding equality to free variable semantic tableaux","volume":"Vol. 607","author":"Beckert","year":"1992"},{"key":"10.1016\/0304-3975(96)00092-8_BIB7","series-title":"Deduction. Automated Logic","author":"Bibel","year":"1993"},{"key":"10.1016\/0304-3975(96)00092-8_BIB8","series-title":"Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS'96)","first-page":"494","article-title":"Simultaneous rigid E-unification and related algorithmic problems","author":"Degtyarev","year":"1996"},{"key":"10.1016\/0304-3975(96)00092-8_BIB9","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-61377-3_38","article-title":"Simultaneous rigid E-unification is undecidable","author":"Degtyarev","year":"1995"},{"key":"10.1016\/0304-3975(96)00092-8_BIB10","article-title":"Reduction of second-order unification to simultaneous rigid E-unification","author":"Degtyarev","year":"1995"},{"key":"10.1016\/0304-3975(96)00092-8_BIB11","series-title":"Second World Conf. on the Fundamentals of Artificial Intelligence (WOCFAI-95)","first-page":"109","article-title":"General connections via equality elimination","author":"Degtyarev","year":"1995"},{"key":"10.1016\/0304-3975(96)00092-8_BIB12","first-page":"342","article-title":"Equality elimination for the inverse method and extension procedures","volume":"Vol. 1","author":"Degtyarev","year":"1995"},{"key":"10.1016\/0304-3975(96)00092-8_BIB13","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. Automated Reasoning"},{"key":"10.1016\/0304-3975(96)00092-8_BIB14","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1145\/128749.128754","article-title":"Theorem proving using equational matings and rigid E-unification","volume":"39","author":"Gallier","year":"1992","journal-title":"J. Assoc. Comput. Machinery"},{"key":"10.1016\/0304-3975(96)00092-8_BIB15","series-title":"Logic in Computer Science (LICS'88)","first-page":"338","article-title":"Rigid E-unification is NP-complete","author":"Gallier","year":"1988"},{"key":"10.1016\/0304-3975(96)00092-8_BIB16","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. and Comput."},{"key":"10.1016\/0304-3975(96)00092-8_BIB17","series-title":"Logic in Computer Science (LICS'87)","first-page":"338","article-title":"Theorem proving using rigid E-unification: equational matings","author":"Gallier","year":"1987"},{"key":"10.1016\/0304-3975(96)00092-8_BIB18","first-page":"126","article-title":"Rigid E-unification and its applications to equational matings","volume":"Vol. 1","author":"Gallier","year":"1989"},{"key":"10.1016\/0304-3975(96)00092-8_BIB19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(96)00092-8_BIB20","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(96)00092-8_BIB21","series-title":"Logic in Computer Science (LICS'94)","article-title":"Rigid E-unifiability is DEXPTIME-complete","author":"Goubault","year":"1994"},{"key":"10.1016\/0304-3975(96)00092-8_BIB22","first-page":"364","article-title":"A simplified proof method for elementary logic","volume":"Vol. 1","author":"Kanger","year":"1983"},{"key":"10.1016\/0304-3975(96)00092-8_BIB23","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. Develop."},{"key":"10.1016\/0304-3975(96)00092-8_BIB24","first-page":"78","article-title":"The decidability problem for some constructive theories of equality","volume":"4","author":"Lifschitz","year":"1967"},{"key":"10.1016\/0304-3975(96)00092-8_BIB25","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. Machinery"},{"key":"10.1016\/0304-3975(96)00092-8_BIB26","first-page":"78","article-title":"Collecting terms in the quantifier rules of the constructive predicate calculus","volume":"4","author":"Mints","year":"1967"},{"key":"10.1016\/0304-3975(96)00092-8_BIB27","first-page":"581","article-title":"The undecidability in the constructive predicate calculus of the class of formulas of the form \u00ac\u00ac\u2200\u2203","volume":"163","author":"Orevkov","year":"1965","journal-title":"Sov. Math. Doklady"},{"key":"10.1016\/0304-3975(96)00092-8_BIB28","first-page":"109","article-title":"Solvable classes of pseudo-prenex formulas","volume":"60","author":"Orevkov","year":"1976"},{"key":"10.1016\/0304-3975(96)00092-8_BIB29","series-title":"JELIA'94","first-page":"152","article-title":"A complete connection calculus with rigid E-unification","volume":"Vol. 838","author":"Petermann","year":"1994"},{"key":"10.1016\/0304-3975(96)00092-8_BIB30","first-page":"162","article-title":"An improved proof procedure","volume":"vol. 1","author":"Prawitz","year":"1983"},{"key":"10.1016\/0304-3975(96)00092-8_BIB31","series-title":"Automated Deduction\u2014CADE-13","first-page":"32","article-title":"Proof-search in intuitionistic logic with equality, or back to simultaneous rigid E-Unification","volume":"Vol. 1104","author":"Voronkov","year":"1996"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397596000928?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0304397596000928?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T12:55:13Z","timestamp":1555419313000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0304397596000928"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,10]]},"references-count":31,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1996,10]]}},"alternative-id":["0304397596000928"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(96)00092-8","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1996,10]]}}}