{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T07:40:39Z","timestamp":1707032439224},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":9050,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1989,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We show that the D<jats:sub>A<\/jats:sub>-uniflcation problem is undecidable. That is, given two binary function symbols \u2295 and \u2297, variables and constants, it is undecidable if two terms built from these symbols can be unified provided the following D<jats:sub>A<\/jats:sub>-axioms hold:<\/jats:p><jats:p><jats:disp-formula><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S0022481200027055_eqnU1\" \/><\/jats:disp-formula><\/jats:p><jats:p>Two terms are D<jats:sub>A<\/jats:sub>-unifiable (i.e. an equation is solvable in D<jats:sub>A<\/jats:sub>) if there exist terms to be substituted for their variables such that the resulting terms are equal in the equational theory D<jats:sub>A<\/jats:sub>.<\/jats:p><jats:p>This is the smallest currently known axiomatic subset of Hilbert's tenth problem for which an undecidability result has been obtained.<\/jats:p>","DOI":"10.2307\/2274856","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T22:30:21Z","timestamp":1146954621000},"page":"402-414","source":"Crossref","is-referenced-by-count":8,"title":["The undecidability of the D<sub>A<\/sub>-unification problem"],"prefix":"10.1017","volume":"54","author":[{"given":"J.","family":"Siekmann","sequence":"first","affiliation":[]},{"given":"P.","family":"Szab\u00f3","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200027055_ref024","volume-title":"Stringunification","author":"Siekmann","year":"1975"},{"key":"S0022481200027055_ref016","article-title":"Special issue on unification theory","author":"Kirchner","journal-title":"Journal of Symbolic Computation"},{"key":"S0022481200027055_ref023","volume-title":"Unification theory","author":"Siekmann","year":"1986"},{"key":"S0022481200027055_ref019","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16780-3_114"},{"key":"S0022481200027055_ref015","first-page":"263","volume-title":"Computational problems in abstract algebra (proceedings, Oxford, 1967","author":"Knuth","year":"1970"},{"key":"S0022481200027055_ref006","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90175-1"},{"key":"S0022481200027055_ref005","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.1973.11993265"},{"key":"S0022481200027055_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90040-2"},{"key":"S0022481200027055_ref002","doi-asserted-by":"publisher","DOI":"10.1007\/BF02575010"},{"key":"S0022481200027055_ref004","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8130-3"},{"key":"S0022481200027055_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15976-2_1"},{"key":"S0022481200027055_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-15976-2_20"},{"key":"S0022481200027055_ref009","first-page":"253","volume-title":"Nachrichten von der K\u00f6nigl. Gesellschaft der Wissenschaften zu G\u00f6ttingen, Mathematisch-physikalische Klasse","author":"Hilbert","year":"1900"},{"key":"S0022481200027055_ref013","first-page":"349","volume-title":"Formal language theory (proceedings, Santa Barbara, California, 1979","author":"Huet","year":"1980"},{"key":"S0022481200027055_ref012","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"S0022481200027055_ref008","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-77487-9","volume-title":"Universal algebra","author":"Gr\u00e4tzer","year":"1979"},{"key":"S0022481200027055_ref014","volume-title":"Minimal and complete word unification","author":"Jaffar","year":"1985"},{"key":"S0022481200027055_ref011","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(73)90301-X"},{"key":"S0022481200027055_ref025","unstructured":"Szab\u00f3 P. , Theory of first order unification, Thesis, University of Karlsruhe, Karlsruhe, 1982. (in German)"},{"key":"S0022481200027055_ref026","doi-asserted-by":"publisher","DOI":"10.1145\/321420.321429"},{"key":"S0022481200027055_ref017","first-page":"287","article-title":"The problem of solvability of equations in a free semigroup","volume":"233","author":"Makanin","year":"1977","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0022481200027055_ref018","first-page":"279","article-title":"Enumerable sets are Diophantine","volume":"191","author":"Matiyasevich","year":"1970","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0022481200027055_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/BF02328450"},{"key":"S0022481200027055_ref020","first-page":"73","volume-title":"Machine intelligence","volume":"7","author":"Plotkin","year":"1972"},{"key":"S0022481200027055_ref010","first-page":"749","article-title":"The solution of certain systems of word equations","volume":"156","author":"Hmelevskij","year":"1964","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0022481200027055_ref021","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200027055","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,4]],"date-time":"2024-02-04T07:26:29Z","timestamp":1707031589000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200027055\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,6]]},"references-count":26,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1989,6]]}},"alternative-id":["S0022481200027055"],"URL":"https:\/\/doi.org\/10.2307\/2274856","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1989,6]]}}}