{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T08:49:12Z","timestamp":1768898952489,"version":"3.49.0"},"reference-count":7,"publisher":"Cambridge University Press (CUP)","issue":"5","license":[{"start":{"date-parts":[[2016,5,3]],"date-time":"2016-05-03T00:00:00Z","timestamp":1462233600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,6]]},"abstract":"<jats:p>There has been an increased interest in the decision problems for linear logic and its fragments. Here, we give a fully self-contained, easy-to-follow, but <jats:italic>fully detailed<\/jats:italic>, direct and constructive proof of the undecidability of a very simple Horn-like fragment of linear logic, which is accessible to a wide range of people. Namely, we show that there is <jats:italic>a direct correspondence<\/jats:italic> between terminated computations of a Minsky machine <jats:italic>M<\/jats:italic> and cut-free linear logic derivations for a Horn-like sequent of the form\n<jats:disp-formula><jats:alternatives><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S0960129516000049_eqnU1\"\/><jats:tex-math>\n\\begin{equation*}\n\\bang{\\Phi_M},\\ l_1 \\vdash l_0,\n\\end{equation*}\n<\/jats:tex-math><\/jats:alternatives><\/jats:disp-formula>\nwhere \u03a6<jats:italic><jats:sub>M<\/jats:sub><\/jats:italic> consists only of Horn-like implications of the following simple forms\n<jats:disp-formula><jats:alternatives><jats:graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" orientation=\"portrait\" mime-subtype=\"gif\" mimetype=\"image\" position=\"float\" xlink:type=\"simple\" xlink:href=\"S0960129516000049_eqnU2\"\/><jats:tex-math>\n\\begin{equation*}\n(l \\llto l'),\\ \\ ((l\\otimes r) \\llto l'),\\ \\ (l\\llto (r\\otimes l')),\\ \\ and \\ \\ (l\\llto (l'\\oplus l'')),\n\\end{equation*}\n<\/jats:tex-math><\/jats:alternatives><\/jats:disp-formula>\nwhere <jats:italic>l<\/jats:italic><jats:sub>1<\/jats:sub>, <jats:italic>l<\/jats:italic><jats:sub>0<\/jats:sub>, <jats:italic>l<\/jats:italic>, <jats:italic>l<\/jats:italic>\u2032, <jats:italic>l<\/jats:italic>\u2033 and <jats:italic>r<\/jats:italic> stand for literals.<\/jats:p><jats:p>Neither negation, nor &amp;, nor constants, nor embedded implications\/bangs are used here.<\/jats:p><jats:p>Furthermore, our particular correspondence constructed above provides decidability for each of the Horn-like fragments whenever we confine ourselves to any two forms of the above Horn-like implications, along with the complexity bounds that come from the proof.<\/jats:p>","DOI":"10.1017\/s0960129516000049","type":"journal-article","created":{"date-parts":[[2016,5,3]],"date-time":"2016-05-03T06:40:11Z","timestamp":1462257611000},"page":"719-744","source":"Crossref","is-referenced-by-count":3,"title":["The undecidability theorem for the Horn-like fragment of linear logic (Revisited)"],"prefix":"10.1017","volume":"26","author":[{"given":"MAX","family":"KANOVICH","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,5,3]]},"reference":[{"key":"S0960129516000049_ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(92)90075-B"},{"key":"S0960129516000049_ref2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150"},{"key":"S0960129516000049_ref6","doi-asserted-by":"publisher","DOI":"10.1137\/0213029"},{"key":"S0960129516000049_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0960129516000049_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150.007"},{"key":"S0960129516000049_ref4","unstructured":"Kosaraju R.S. (1982). Decidability of reachability in vector addition systems. In: Proceedings of the 14th Annual Symposium on Theory of Computing 267\u2013281. Preliminary Version."},{"key":"S0960129516000049_ref7","doi-asserted-by":"publisher","DOI":"10.2307\/1970290"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129516000049","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,18]],"date-time":"2019-04-18T23:04:41Z","timestamp":1555628681000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129516000049\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,5,3]]},"references-count":7,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["S0960129516000049"],"URL":"https:\/\/doi.org\/10.1017\/s0960129516000049","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,5,3]]}}}